I want to check validity of a formula with the following quantifier alternation: ∃∀.φ

1. Do I check validity of this formula if I solve Exists(exist_vars, ForAll(forall_vars, Phi)) in Z3Py? What is the difference between checking validity and satisfiability of this formula? How do I check both in Z3?

I mean I know that e.g., a ∃.ψ being unsat implies a ∀.¬ψ being valid, but I still do not understand what is the difference between validity and satisfiability. For instance, what is the meaning of a ∃.ψ being valid?

I want to really understand this because I have the following situation, going back to ∃∀.φ. It is the case that I am going to keep variables in the universal scope unchanged (i.e., have the part ∀.φ re-used over and over), whereas I will only modify the existentially quantified part. Thus, I decided to save some computation and "simplify" ∃∀.φ by performing quantifier elimination of ∀.φ, so I get φ'.

The problem is that we know that ∃φ' preserves equi-satisfiability with respect to ∃∀.φ... but what about validity? I guess that if I solve ∃φ', and get SAT, then I am not solving whether ∃∀.φ is valid (instead, that ∃∀.φ is satisfiable), am I right?

2. How can I perform validity of the original formula, but doing quantifier elimination in order to save some computation? Do I have to negate the formula in something like ¬∃¬φ'? How can I think of transformations from satisfiability to validity involving first-order theories and quantifier elimination?

Do I check validity of this formula if I solve Exists(exist_vars, ForAll(forall_vars, Phi)) in Z3Py? What is the difference between checking validity and satisfiability of this formula? How do I check both in Z3?

To be clear, z3 has a solve function. Are you talking about using that? Here's an example:

from z3 import *

x, y = BitVecs('x y', 16)
solve(Exists([x], ForAll([y], x <= y)))

This prints:

[]

The meaning of this is that the formula is satisfiable, though due to quantifiers there's no model to display. You can also use prove:

prove(Exists([x], ForAll([y], x <= y)))

This prints:

proved

So, to answer your question: To check validity use prove. To check satisfiability use solve.

Internally, solve creates a problem and asks if it's sat. (This is the basic function provided by z3.) On the other hand prove asks if the negation is satisfiable. You can do the same of course:

solve(Not(Exists([x], ForAll([y], x <= y))))

This prints:

no solution

which means it is not satisfiable; proving that ∃x∀y. x <= y is a valid formula when x and y are interpreted as 8-bit bit vectors.

All these techniques about quantifier-elimination etc. is more or less irrelevant. If you have the formula ∃∀.φ and you performed quantifier-elimination to get rid of the universal and found ∃φ' then you do the same thing: To prove, check the satisfiability of ¬∃φ'. If you get unsat, your original is formula is valid.

As usual, thinking about "concrete" examples helps understanding. If the above wasn't clear, I suggest you write down concrete examples and ask questions about concrete instances.

Skolemization and negation do not commute

It's important to note that if you want to check validity by checking if the negation is unsatisfiable (which is a valid proof method), then you have to be careful if you also want to skolemize. In particular, you have to first negate, and then skolemize. If you first skolemize and then negate, that would be unsound.

Here's a concrete example to demonstrate. Let's say we want to check the validity of the formula:

∃x∀y.y >= x

where x and y are interpreted over 8-bit bit-vectors. This is a valid formula. The value of 0 for x is a witness, as no (unsigned) bit vector is less than 0 by definition.

The typical way to prove this in z3 would be:

from z3 import *

s    = Solver()
x, y = BitVecs('x y', 8)

phi = Exists([x], ForAll([y], y >= x))

# Negate
phi1 = Not(phi)

# Check unsat to prove phi
s.add(phi1)
print(s.check())

And the above prints unsat, establishing validity.

Let's say we want to play the skolemization game. The correct way would be to NEGATE the formula first, and then skolemize, like this:

from z3 import *

s    = Solver()
x, y = BitVecs('x y', 8)

phi = Exists([x], ForAll([y], y >= x))

# Negate, then skolemize. This is OK.
F = Function('F', BitVecSort(8), BitVecSort(8))
phi1 = ForAll([x], F(x) < x)

# Check unsat to prove phi
s.add(phi1)
print(s.check())

(I manually negated and then skolemized, I'm sure you can follow the details there.) This also prints unsat; so we're good.

If, however, we make the mistake of skolemizing first and then negating, look what we get:

from z3 import *

s    = Solver()
x, y = BitVecs('x y', 8)

phi = Exists([x], ForAll([y], y >= x))

# Skolemize, then negate. NOTE THAT THIS IS UNSOUND!
phi1 = Not(ForAll([y], y >= x))

# Check unsat to prove phi
s.add(phi1)
print(s.check())
print(s.model())

And this prints:

sat
[x = 1]

which might lead you to think that the original formula is NOT valid; with x = 1 as the counter-example. But that's obviously not a valid conclusion. We made a mistake: We first skolemized and then negated; which is an unsound thing to do for proving validity via checking the satisfiability of the negation.

To sum up

You can always check validity of some formula φ by showing that ¬φ is unsatisfiable. But be careful: if you want to do skolemization for whatever reason, you have to skolemize ¬φ! You can't first skolemize φ, and then negate the remnant. That would be an unsound thing to do.