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?