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:13Questions 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. 


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). 


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. 

