From: Aatu Koskensilta on 29 Jun 2010 08:28 George Greene <greeneg(a)email.unc.edu> writes: > I really don't think that the model existence theorem is going to leap > out at him here. Pretty much any elementary text contains an account of the set theoretic construction of the various number systems. It's a trivial exercise to verify the axioms of PA hold in the structure of naturals. Combined with the soundness of first-order logic this immediately yields the consistency of PA. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 29 Jun 2010 08:29 Charlie-Boo <shymathguy(a)gmail.com> writes: > No no no. You have to prove it using ZFC's axioms and rules only. No no no. You have to prove it to Charlie-Boo's satisfaction, with broccoli sticking out of your ears, drunk on too much cheap whiskey. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 29 Jun 2010 08:34 Transfer Principle <lwalke3(a)lausd.net> writes: > 1. Is there a proof in ZF-Inf+~Inf that every set is finite? It appears I once posted a proof. It relies, in an essential way, if I recall correctly, on the axiom of replacement. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 29 Jun 2010 08:58 Charlie-Boo <shymathguy(a)gmail.com> writes: > How about when you said that Gentzen proved PA consistent using ZFC? No one ever proves anything using ZFC in the sense of producing formal derivations. Rather, they prove mathematical theorems using mathematical principles formalized in ZFC. By certain elementary considerations we know the formalizations of such theorems are formally derivable in ZFC. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 29 Jun 2010 09:11
Frederick Williams <frederick.williams2(a)tesco.net> writes: > Yes, you can: take Gentzen's proof (or Ackermann's etc) and formalize > it in ZFC. This is a pretty silly way of proving the consistency of PA in set theory. That PA is consistent is a triviality. The interest in Gentzen's proof lies elsewhere. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus |