# 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
Commented May 29, 2013 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
Commented May 29, 2013 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
Commented May 29, 2013 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. Commented May 29, 2013 at 16:25