From: Aatu Koskensilta on
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
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
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
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
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