Formal Proof in ZFC that {Cmpr, Pair} $\vdash$ Pair#

Question

Comprehension and Pair come from ZFC and Pair# is a proposed alternate axiom to Pair. We want to show that {Cmpr, Pair} $\vdash$ Pair# in ZFC.

Cmpr $$ \forall x \forall w_1 \ldots \forall w_n \exists y \forall z (z \in y \leftrightarrow (z \in x \wedge \phi(z, w_1, \ldots, w_n)))$$

Pair $$\forall x \forall y \exists z (x \in z \wedge y \in z).$$

Pair# $$\forall x \forall y \exists p \forall u (u \in p \leftrightarrow (u = x \vee u = y)).$$

Here is my informal proof.

Let $x$ and $y$ be sets. By Pair, $\forall x \forall y \exists z (x \in z \wedge y \in z),$ meaning that there exists a set $z$ which has $x$ and $y$ as members (and possibly more other members). Let $\phi$ be the set property that $\{u \in z : u = x \vee u = y\}$. By Comprehension, given the set $z$ and the property $\phi$, there is a set $p$ whose elements are precisely those elements of $z$ which satisfy $\phi$. Thus, we have that $p = \{x, y\}$, showing that Pair# is satisfied.

First, is my description for $\phi$ a valid way to specify a "property of sets"? I am not entirely sure what this means.

Second, how do I translate this into a formal proof? I suspect this will involve a lot of coming up with tautologies and using MP, but I honestly don't even know where to get started. Any help is greatly appreciated.

Answer 1

Given any unary predicate $\phi(u)$, comprehension implies $\exists p\forall u (u\in p\iff u\in z\land\phi(u))$, with $z$ defined as per your usage of pair. For this inference to coincide with pair#, it suffices by modus ponens to take $\phi(u)$ to be $u=x\lor u=y$. Of course, any $\phi$ that suffices could be replaced with $u\in z\land\phi(u)$, but this is an unnecessary complication. This is what I imagine you intended when you wrote, "Let $\phi$ be the set property that $\{u\in z:u=x\lor u=y\}$" (i.e. I think you were defining $\phi(u)$ as $u\in z\land (u=x\lor u=y)$).

Answer 2

As noted in comments, your $\phi$ is not a property of sets -- it's a class. You're correct when you say that Comp says that given a set, there is a subset of that set whose elements all satisfy some property. What's the property we want? "Being identical to x or being identical to y" (for some given $x$ and $y$). We can write this as a formula with one free variable, $u$, as follows: $u = x \lor u = y$. We call this formula $\varphi$. If $\varphi$ holds of $u$, then $u$ is identical to $x$ or to $y$, meaning $u$ has the property we want. Now it does indeed follow from Cmpr that when we're given a set, there's a subset of that set whose elements all satisfy the property. For the following formula is an instance of Cmpr: $$\forall x \forall w_1 \forall w_2 \exists y \forall z(z \in y \leftrightarrow (z \in x \land (u = w_1 \lor u = w_2)))$$ (Note we replaced $\phi$ in Comp not by our $\varphi$ but by a variation on it, in which $w_1$ and $w_2$ are also free.) And, given this, we can derive $$\forall u \exists y \forall z(z \in y \leftrightarrow (z \in u \land (z = x \lor z = y))) \tag{1}$$ which tells us that for any set $u$ there is a $y \subset u$ such that all elements of $y$ satisfy $\varphi$.

Now your informal proof is basically "Given (1), I can turn the set that Pair gives me into the set Pair# asserts exists". It's a fine informal proof. You ask how to turn it into a formal one. I'll walk you through my own thought process and, at the end, note what generalizes particularly well.

First, we try and write down the central idea. Saying we can turn the set Pair gives us into the set whose existence Pair# asserts is saying that we can turn any set containing $x$ and $y$ into a set containing only $x$ and $y$. It is to say that $$\forall p(x \in p \land y \in p \rightarrow \exists p' \forall u(u \in p' \leftrightarrow (u = x \lor u = y))) \tag{2}$$Let's imagine we have a proof of (2). Then we can use the statement $$\forall p (\varphi \to \psi) \leftrightarrow (\exists p \varphi \to \psi) \tag{3}$$ which holds whenever $p$ is not free in $\psi$, and throw some quantifiers at the formula we get, to ultimately arrive at $$\forall x \forall y \exists p(x \in p \land y \in p) \to \forall x \forall y \exists p \forall u(u \in p \leftrightarrow (u = x \lor u = y))$$or in other words "Pair $\to$ Pair#". So if we can prove (2), we're done. How do we prove (2)? In the informal proof you got it from (1), which we know we can get from Cmpr. We can also get it from (1) in a formal proof. For, using the statement $$\forall x \psi \rightarrow \forall x(\varphi \to \psi) \tag{4}$$ we can from (1) arrive at $$\forall p(x \in p \land y \in p \rightarrow \exists y \forall z(z \in y \leftrightarrow z \in p \land (z = x \lor z = y))) \tag{5}$$and from (5), we can arrive at (2). I leave this part (and writing down the full proof, which will probably involve proving (3) and (4)) to you. (It might help you to note that in axiomatic systems the best way to prove $\exists x \varphi \to \exists x \psi$ is usually to prove $\forall x \neg \psi \rightarrow \forall x \neg \varphi$ and contrapose, and that in general formal proofs use contraposition all the time.)

What in this thought process is generally applicable? Write down the statements your informal proof uses; write down your axioms; use statements like (3) and (4) which hold generally to connect the latter to the former. At the end of this process, you have the skeleton of a proof, and you just need to fill in the blanks.