# 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
– Martín-Blas Pérez Pinilla Jun 6 '14 at 8:48

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

Now, what happens if (Xenu forbid!) (that fragment of) ZFC is itself inconsistent? In that case since ZFC proves everything, the fact that it proves the consistency of PA is rather worthless. What we can glean from this is that the consistency of ZFC implies the consistency of PA; an example of a relative consistency result, but does not give the absolute consistency of PA.

-
There is a little thing I don't understand completely. Usually, when treating with models, we don't want the structure to be exactly a structure described in a formal way. So it is immaterial whether the natural number structure take place in ZFC or not. It is just a non-formal structure we can talk about without referring to ZFC, isn't it? – Oo3 Apr 6 '12 at 9:34
The issue is that you need the machinery of sets and functions to even define what a model is. So, although you may not need to speak about sets and relations when you exhibit a model, the proof that the existence of a model implies consistence is dependent on the consistency of the "expressive" theory (the one doing the expressing) – nomen Jun 4 '14 at 0:03

One reason for investigating other consistency proofs (related to that given by Arthur Fischer) is philosophical/foundational. As Arthur Fischer pointed out, we can only prove consistency relative to some other, stronger system. Proving the consistency of $PA$ in $ZFC$ is rather like using a bazooka to open a can of beans; $ZFC$ is much, much stronger than $PA$ and accordingly, you might think, much more likely to be inconsistent. So from a philosophical/foundational perspective, one might want a consistency proof relative to a weaker theory than $ZFC$. Using less to prove consistency ought to improve ones faith that the theory is consistent. In the case of $PA$, Goedel showed that theory equiconsistent with the theory $T$, an extension in finite types of $PRA$ (primitive recursive arithmetic) and thus is in a certain sense finitistically justified.

There is a slightly more technical consideration lurking in the background here. By examining exactly how much one needs to prove a theory consistent, one gets an idea of the precise strength of the theory. Proving $CON(ZFC) \rightarrow CON(PA)$ tells you $ZFC$ is stronger than $PA$, but not by how much. Gentzen's consistency proof for $PA$ using transfinite induction up to $\epsilon_0$ yields an "ordinal analysis" of $PA$ ($\epsilon_0$ being the least ordinal $PA$ cannot prove recursive), and a correspondingly more refined conception of the strength of that theory.

-