# Things around $(\forall x)(\Psi \Rightarrow \Phi) \Leftrightarrow ((\exists z)\Psi) \Rightarrow \Phi)$

Let $M,N$ be sets, $Q_M$ a set that depends on $M$ and $P(\cdot,\cdot)$ a property with two parameters (is it ok, to call these "parameters" or would "variables" have been better ?). Consider the following three statements:

i) $(\forall x\in M)(\forall y\in Q_M)[P(x,y)\Rightarrow x \in N]$

ii) $(\forall x\in M)[((\exists y\in Q_M)[P(x,y)])\Rightarrow x \in N]$

iii) $N=\{ x\in M \mid (\exists y\in Q_M)[P(x,y)]\}$

I would very much like to know the following:

1. I have been told that i) and ii) are equivalent, since they are an instance of a general scheme $$(\forall x)(\Psi \Rightarrow \Phi) \Leftrightarrow ((\exists z)\Psi) \Rightarrow \Phi),$$ which holds if $z$ is not mentioned in $\Phi$, as Carl Mummert I think explained a long time ago - I can't find the entry right now.
What are the "values" the $x,z,\Psi$ and $\Phi$ have to take, such that this scheme shows the equivalence of i) and ii) ?

2. What kind of setting do you need in which you can prove this general scheme ? Is it only predicate logic ? Or do you need ZFC to formalize this logic so you can you use set-theory to prove it ?

3. How to you prove it (or a corrected version of it, if the above is flawed; it seems to me that quantifiers are missing) ?

4. Is ii) equivalent to iii) ? How do you rigorously prove that ? Which ZFC axioms are needed for that proof ?

-
@MinimusHeximus Using lattice theory ? I can't imagine how that could work... Maybe you mean that there is a formal analogy between similar looking statements in lattice theory and these ones ? Also, what is ZDF ? –  temo May 29 '13 at 14:52

Hints:

1] Assuming that $x$ is not free in $\varphi$, here's a chain of equivalences:

(a) $\forall x(\psi(x) \to \varphi)$

(b) $\forall x(\neg\psi(x) \lor \varphi)$

(c) $\forall x\neg\psi(x) \lor \varphi$

(d) $\neg\forall x\neg\psi(x) \to \varphi$

(e) $\exists x\psi(x) \to \varphi$

The only step that might give you pause is the equivalence of (b) and (c): it might help to compare $(\neg\psi(a) \lor \varphi) \land (\neg\psi(b) \lor \varphi)$ and $(\neg\psi(a) \land \neg\psi(b)) \lor \varphi$. Note that equivalence of (a) and (e) is just a matter of first-order logic, and nothing to do with ZFC.

2] These are also equivalents:

(a') $(\forall x \in A)(\psi(x) \to \varphi)$

(b') $(\exists x \in A)\psi(x) \to \varphi$

by just the same kind of reasoning, and again just by appeal to first-order logic. You just need to unpack the abbreviations for restricted quantifiers.

3] To see your (i) implies (ii), instantiate (i) -- use a parameter to name an arbitrary object in $M$ -- apply an (a'/b')-type equivalence, and generalize to get (ii). You can then do the reverse equivalence.

-
I don't really understand 3]. What is an (a'/b')-type equivalence ? Also, wouldn't I need two objects $M_1,M_2$ to instantiate with, since I have two quantifiers ? Or did you mean to show the equivalence between (ii) and (iii) ? Since your numbering differs from mine, I'm somewhat confused what is proved where. (Could you please also answer my question 1. ?) –  temo May 29 '13 at 15:03
In case you really meant (i) and (ii) in 3], what is an "object" ? Since we are outside of set-theory I thought I would only have syntactic rules at my disposal that tell me how to manipulate first-order formulas... –  temo May 29 '13 at 15:03
An (a'/b')-type equivalence is an equivalence of the kind illustrated by the pair (a'), (b') above. I meant your (i) and (ii). You only need to instantiate the outermost quantifiers to expose a pair of wffs of the relevant (a'/b')-types. I've replaced "object" with "parameter naming an object" (which should help explain what was obviously meant in context). Hope that helps. –  Peter Smith May 29 '13 at 16:25