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.
closed as off topic by Timothy Chow, Qiaochu Yuan, Simon Thomas, Gjergji Zaimi, François G. Dorais♦ Dec 22 '10 at 20:13
Questions on MathOverflow are expected to relate to research level mathematics within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here. If this question can be reworded to fit the rules in the help center, please edit the question.

7$\begingroup$ 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? $\endgroup$ – Gabriel Ebner Dec 22 '10 at 16:52

4$\begingroup$ Is this a researchlevel question? $\endgroup$ – Andrej Bauer Dec 22 '10 at 18:23

3$\begingroup$ Vote to close since this is too elementary a question for MO. $\endgroup$ – Timothy Chow Dec 22 '10 at 18:36

$\begingroup$ 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...) $\endgroup$ – David E Speyer Dec 23 '10 at 13:45

$\begingroup$ 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) $\endgroup$ – David E Speyer Dec 23 '10 at 13:53
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).

$\begingroup$ @Steven : Small typo in the first line: The second ZFC should be PA. $\endgroup$ – Andrés E. Caicedo Dec 22 '10 at 17:04

$\begingroup$ Andres: Thanks. I went to edit this, but it looks like Terry Tao did it for me. $\endgroup$ – Steven Landsburg Dec 22 '10 at 20:01
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.