How to prove Con(PA) in ZFC? [closed]

PA doesn't prove Con(PA) but ZFC does. That means the extra axiom of infinity is of tantamount importance in the proof. Not seen such a proof, think it would be interesting. Heard of it.

-
ZFC proves that the natural numbers (which exist by the axiom of infinity) are a model of PA, and therefore by soundness that PA is consistent? – Gabriel Ebner Dec 22 2010 at 16:52
Is this a research-level question? – Andrej Bauer Dec 22 2010 at 18:23
Vote to close since this is too elementary a question for MO. – Timothy Chow Dec 22 2010 at 18:36
Wikipedia's article en.wikipedia.org/wiki/Axiom_of_infinity has a good explanation of how ZF proves that there is a set $\omega$ and an operation $S$ obeying the Peano axioms. In other words, ZF proves that there is a model of PA. (continued...) – David Speyer Dec 23 2010 at 13:45
This no doubt reveals my ignorance of set theory, but it seems to me to be a little tricky to finish from here. I would like a theorem of ZF saying "For any theory T, if T has a model then Con(T)". It's not clear to me that this claim can be expressed in ZF! Everytime I try, I wind up wanting a truth predicate planetmath.org/encyclopedia/… . (continued) – David Speyer Dec 23 2010 at 13:53

closed as off topic by Timothy Chow, Qiaochu Yuan, Simon Thomas, Gjergji Zaimi, François G. Dorais♦Dec 22 2010 at 20:13

You can also prove the consistency of PA with second order logic.

The key thing is that you need a higher order induction hypothesis. In first order logic + PA, the induction hypothesis are limited to first order expressions.

The strength of a logic is often determined by what you allow in the induction hypothesis.

-

Within ZFC you can formalize Tarski's definition of truth, then prove that the axioms of PA are all true and that the rules of inference preserve truth. This gives a formal proof of Con(PA).

This allows you to prove not just the consistency of PA, but the consistency of PA + Con(PA), or PA + Con(PA) + Con(PA+Con(PA)), etc. Nothing close to the full strength of ZFC is needed for any of this (though of course you need something beyond PA).

-
 @Steven : Small typo in the first line: The second ZFC should be PA. – Andres Caicedo Dec 22 2010 at 17:04 Andres: Thanks. I went to edit this, but it looks like Terry Tao did it for me. – Steven Landsburg Dec 22 2010 at 20:01