I'm trying to understand this example:
solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])
but after reading the explanation I still don't understand it.
How do you read this? what is the meaning of []?
My wrong interpretation of this is.
"Given the theorem y == x + 1. Does it hold for all y such that Implies(y <= 0, x < y)?"
With this interpretation if I use y = 0 and x = -1 every constraint (Implies(y <= 0, x < y) is true since y <= 0 and x < y) is respected, but If I run this I find out that it's not solvable.
Do you have any hits to how to understand this topic?
Looks like there're a couple of confusions here. Let's first sort out binding: In a quantifier context, the variable is independent, i.e., it can be renamed with no change to the semantics. So, your original:
from z3 import *
x, y = Ints('x y')
solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])
is exactly equivalent to:
from z3 import *
x, y, z = Ints('x y z')
solve([y == x + 1, ForAll([z], Implies(z <= 0, x < z))])
Note that we replaced the y in the "scope" of ForAll to z, but left the one in the first conjunct untouched. You can only rename within the scope of ForAll (or Exist), not outside of it.
And both of these equivalent expressions are unsatisfiable. Why? The first conjunct is easy to satisfy; just pick an arbitrary x, and set y to be x+1 and you're done. It's the second conjunct that's unsatisfiable. Because, no matter which x you choose to satisfy the first, you can always find a z that's less than that x (just pick min(0, x-1)), and the quantified formula becomes False for that assignment. And hence there are no solutions.
Now, let's consider the variant you had in your comments, with x > z:
from z3 import *
x, y, z = Ints('x y z')
solve([y == x + 1, ForAll([z], Implies(z <= 0, x > z))])
Again, the first conjunct is easy to satisfy. And this time, so is the second, because you can pick a positive x, and that will be greater than all z's so long as z <= 0, and thus the implication is always true. And that's exactly what z3 is telling you, when it gives you the satisfying assignment:
[x = 2, y = 3]
Note that there's nothing in this assignment regarding the variable z. You cannot really give a model for a universally quantified formula; by definition it is true for all values of z.
Hope this clears things up.