Question about the use of quantifiers

[lastever-article]

Suppose we have four integer variables w,x,y,z and a quantifier-free integer formula fml over them.
Consider four quantified formulas f1, f2, f3 below

        from z3 import *
        w, x, y, z = Ints("w x y z")
        fml = .... 
        f1 = Exists([w, x], fml)
        f2 = ForAll([y, z], fml)
        f3 = Exists([w, x], (ForAll([y, z], fml)))

Can we say that f2 must be equivalent to f3? Perhaps f2 and f3 are equi-satisfiable, but not necessarily equivalent?

Thanks!

NOTE: I use the following code to check for equivalence.

def is_equivalent(a, b):
    s = Solver()
    s.add(a != b)
    res = s.check()
    if res == sat:
        return False
    return True

[NikolajBjorner]

f2 != f3 is the same
as

ForAll([y, z], fml) != Exists([w, x], (ForAll([y, z], fml)))

w, x are free in left side. The free variables are existentially force at the top level

In other words, it checks sat of the formula:

Exists([w,x], (ForAll([y, z], fml) != Exists([w, x], (ForAll([y, z], fml)))))

This formula is different from

Exists([w,x], ForAll([y, z], fml)) != Exists([w, x], (ForAll([y, z], fml)))

[lastever-article]

Did you mean that f2 and f3 are indeed equivalent, but my function is_equivalent is inappropriate for checking the property? Do you have other suggestions for the checking? Thanks!

[NikolajBjorner]

I meant to say that f2 and f3 are not equivalent.

[lastever-article]

Should we say that f2 and f3 are equi-satisfiable, but not necessarily equivalent?

To my understanding, we may assume that the logic admits QE (quantifier elimination).
We may denote G(w,x) the formula obtained by performing QE on f2, i.e., f2 = G(w, x)
We then have f3 = Exists([w, x], G(w,x)).

Therefore, we know that Exists([w, x], G(w,x)) and G(w,x) are not equivalent, but equi-satisfiable.
Because in the second formula, the bound variable w,x are replaced by fresh constants w,x?
Is my previous understanding correct? Thanks!

[NikolajBjorner]

Not sure how to explain it further. This will have to be my last attempt. If that doesn't work,
there have to be textbooks that can explain it or someone else with better expository skills.
The question is not specific to z3.

You appear to be conflating equi-satisfiability with equivalence.
When you write s.add(f2 != f3) and expecting unsat you are checking for equivalence not equi-satisfiability.
What you are implying is that you expect to check for equi-satisfiability. Because f2 and f3 are equi-satisfiable (f2 is satisfiable if and only if f3 is satisfiable).

[lastever-article]

Thanks! I knew the difference between equivalence and equi-satisfiabiltiy (e.g., after Tseitin transformation, the CNF formula is only equi-satisfiable with the original formula).
In the beginning, I expected to check for equivalence. But later I was aware that f2 and f3 are only equi-satisfiable, as illustrated by f2 = G(w,x) and f3 = Exists([w, x], G(w,x)) above (assuming that G(w,x) is a quantifier-free formula equivalent to f2.)