Simple ZFC question

  • Thread starter Fredrik
  • Start date
  • #26
yossell
Gold Member
365
16
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...
 
  • #27
yossell
Gold Member
365
16
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
  • #28
Fredrik
Staff Emeritus
Science Advisor
Gold Member
10,851
413
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.
 
  • #29
yossell
Gold Member
365
16
Oh - ok then
 
  • #30
Fredrik
Staff Emeritus
Science Advisor
Gold Member
10,851
413
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. :smile:
 
  • #31
yossell
Gold Member
365
16
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.
 
  • #32
Fredrik
Staff Emeritus
Science Advisor
Gold Member
10,851
413
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

[tex]\{p,q\}\vdash p\land q[/tex]

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. :smile: The proof is based on the observation that [itex]p\rightarrow(q\rightarrow p\land q)[/itex] is a tautology, which I see that you're already using in your pdf.

[tex]\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*}[/tex]

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

[tex]\{\forall x p(x),\forall x q(x)\}\vdash\forall x(p(x)\land q(x))[/tex]

[tex]\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*}[/tex]

The claim we want to prove is

[tex]\emptyset\vdash\forall x(\forall y(x\in y\leftrightarrow x\in y)\ \land\ \forall y(y\in x\leftrightarrow y\in x))[/tex]

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

[tex]\emptyset\vdash\forall x(p(x)\land q(x))[/tex]

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:
  • #33
Hurkyl
Staff Emeritus
Science Advisor
Gold Member
14,916
19
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. :smile:
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.
 
  • #34
Fredrik
Staff Emeritus
Science Advisor
Gold Member
10,851
413
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 :smile:).
 
Last edited:

Related Threads on Simple ZFC question

Replies
8
Views
3K
  • Last Post
Replies
2
Views
2K
  • Last Post
Replies
13
Views
7K
  • Last Post
Replies
1
Views
2K
  • Last Post
Replies
20
Views
5K
  • Last Post
Replies
10
Views
3K
Replies
4
Views
1K
  • Last Post
Replies
6
Views
4K
Replies
40
Views
1K
Top