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 ?

  • $\begingroup$ @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 ? $\endgroup$ – temo May 29 '13 at 14:52


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.

  • $\begingroup$ 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. ?) $\endgroup$ – temo May 29 '13 at 15:03
  • $\begingroup$ 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... $\endgroup$ – temo May 29 '13 at 15:03
  • $\begingroup$ 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. $\endgroup$ – Peter Smith May 29 '13 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.