# Consistency of PA: why other proofs?

Completeness theorem affirms that a formal first order system is consistent iff it has a model. The FOL number theory(PA) or First Order Arithmetic has a model, which is the natural numbers structure. So PA is consistent. But then,

why one needs proofs of the consistency of PA such (such those by Gentzen, Ackermann etc... obviously not in PA)? Is it only for the sake of proving the result "syntactically" and not by using semantic tools such as models, or what else?

-
The mathematical principles needed to prove the completeness theorem are considerably stronger than PA itself, and according to some, stronger than what is really needed to do mathematics. So in a philosophical sense, there's no real meaning to such a proof of the consistency of PA. –  Zhen Lin Mar 14 '12 at 12:42
could you please cite a reference for these consistency proofs (by Gentzen, Ackermann, ect)? I am not sure I know what you are referring at –  magma Mar 14 '12 at 15:43
One reason is that the construction of the natural number structure (and the proof that it is a model of PA) actually takes place in a much stronger system: (a fragment of) ZFC. Since you are using ZFC to construct a model of PA, this amounts to "ZFC $\vdash$ PA is consistent."