# Simple ZFC question

yossell
Gold Member
Yes - this system is not easy to work with.

But: Phi -> (Psi -> (Phi & Psi)) is a tautology, so all instances of it are axioms. So, if you can prove Phi, and you can prove Psi then, by this axiom and two instances of Modus Ponens, you can prove the conjunction.

But now we've got to try and work out how to get that final universal quantifier in place...damn this system...

yossell
Gold Member
Fredrik,

it's hard in this system to get the effect of universal introduction, but I think I see how it's done. But it's so fiddly I couldn't face writing it all out in latex - or even longhand. I've attached a document - errors tend to creep in, and the notation may not be clear and it may even not work - but maybe it will help and we can bat it around a bit.

#### Attachments

• proof.pdf
43.3 KB · Views: 147
Staff Emeritus
Gold Member
I don't really feel the need to work out every detail of this specific problem right now. If I ever study the next few pages in Kunen's book, I will probably understand his approach well enough to figure it out. It looks like he proves a few theorems that makes things easier. Right now I'm satisfied knowing that there isn't just one set of axioms that defines the one and only proof theory. Thanks everyone for helping out. I learned a lot from this thread.

yossell
Gold Member
Oh - ok then

Staff Emeritus
Gold Member
Yossell, I wouldn't have written that if I had seen your post. I didn't see it until now. I don't have time today, but I will examine what you wrote tomorrow. If we are close to working this out, I might as well make an effort. I didn't mean that I absolutely don't want to work on this. I just wanted to let you know that you don't need to break your back trying to help me with something that really isn't that urgent.

yossell
Gold Member
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.

Staff Emeritus
Gold Member
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} \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".

Last edited:
Hurkyl
Staff Emeritus
Gold Member
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.

Staff Emeritus