Does x=y ∧ y∈z ⟹ x∈z follow from ZFC axioms?

[yossell]

That's ok Fredrik - I quite enjoyed thinking about it. I haven't seen this system before, and it's interesting seeing how one can use it to prove things one is used to taking for granted.

 

[Fredrik]

I think I got it now, after studying parts of the next few pages of the book. It gets easier if we consider a couple of simpler problems first. First we prove

$$\{p,q\}\vdash p\land q$$

This is a special case of one of the theorems Kunen proves in the book. It's kind of funny that I couldn't figure out how to prove that p and q proves "p and q" without using the book. The proof is based on the observation that $p\rightarrow(q\rightarrow p\land q)$ is a tautology, which I see that you're already using in your pdf.

$$\begin{align*}1.\quad & p\hspace{8 cm} & \in\{p,q\}\\ 2.\quad & q & \in\{p,q\}\\ 3.\quad & p\rightarrow(q\rightarrow p\land q) & \text{tautology}\\ 4.\quad & q\rightarrow p\land q &\text{MP 1,3}\\5.\quad & p\land q & \text{MP 2,4}\end{align*}$$

Hm, the "align" environment behaves strangely here, but it looks good enough. Now consider the slightly more difficult problem

$$\{\forall x p(x),\forall x q(x)\}\vdash\forall x(p(x)\land q(x))$$

$$\begin{align*}1.\quad & \forall x p(x) & \in\{\forall x p(x),\forall x q(x)\}\\ 2.\quad & \forall x q(x) & \in\{\forall x p(x),\forall x q(x)\}\\ 3.\quad & \forall x( p(x)\rightarrow(q(x)\rightarrow p(x)\land q(x))) & \text{tautology}\\ 4.\quad & \forall x( p(x)\rightarrow(q(x)\rightarrow p(x)\land q(x))) \rightarrow (\forall x p(x)\rightarrow\forall x(q(x)\rightarrow p(x)\land q(x)) &\text{axiom 3}\\ 5.\quad & \forall x p(x)\rightarrow\forall x(q(x)\rightarrow p(x)\land q(x)) & \text{MP 3,4}\\ 6.\quad &\forall x(q(x)\rightarrow p(x)\land q(x)) & \text{MP 1,5}\\ 7.\quad & \forall x q(x)\rightarrow \forall x(p(x)\land q(x)) & \text{axiom 3}\\ 8.\quad & \forall x(p(x)\land q(x)) &\text{MP 2,7}<br /> \end{align*}$$

The claim we want to prove is

$$\emptyset\vdash\forall x(\forall y(x\in y\leftrightarrow x\in y)\ \land\ \forall y(y\in x\leftrightarrow y\in x))$$

Let's define p(x) and q(x) to be the $\forall y(\text{blah-blah})$ formulas above, so that what we want to prove takes the form

$$\emptyset\vdash\forall x(p(x)\land q(x))$$

With this notation, the proof is exactly identical to the proof of the second theorem above. Only the motivation for the first two lines will be different. This time, the text motivating the first two lines should say "tautology".

 

[Hurkyl]

It's kind of funny that I couldn't figure out how to prove that p and q proves "p and q" without using the book.

It's not too different than proving things like (-1)x = -x from the ring axioms. The basic calculus was presented with very reduced functionality, and so to use it, it takes some clever arguments to construct the simple things we take for granted.

 

[Fredrik]

It's not too different than proving things like (-1)x = -x from the ring axioms. The basic calculus was presented with very reduced functionality, and so to use it, it takes some clever arguments to construct the simple things we take for granted.

That's certainly true. I remember struggling with 0x=0 for vector spaces, and 1>0 for ordered fields. (The latter one quite recently actually ).