# Why wouldn't someone accept Gentzen's consistency proof?

The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, relying either on intuition or the acceptance of a consistency proof such as Gentzen's proof.

If Gentzen's proof shows the consistency of PA, then what is there to "accept"? Is the point that some mathematicians might not accept that Gentzen's proof shows the consistency of PA because we don't know whether the system Gentzen uses in his proof is consistent?

• You can see also Gentzen's consistency proof with Kleene's comment, and also Annika Siders, Gentzen’s Consistency Proofs for Arithmetic : "It should be noted that the theory, in which the proof is formalizable, is incomparable to Peano arithmetic. The theory is not stronger than Peano arithmeic, since complete induction cannot be proved for all formulas. But on the other hand, neither is the theory weaker, since it proves the consistency of Peano arithmetic." Oct 16, 2014 at 7:37
• If PA are inconsistent, then all sets must be Dedekind-finite. Oct 17, 2014 at 2:48

Essentially due to Gödel's Incompleteness Theorems, proofs of the consistency of $\mathsf{PA}$ must involve methods that transcend $\mathsf{PA}$ itself. If one has any doubts about the consistency of $\mathsf{PA}$, those doubts are likely only to be amplified concerning the methods used to prove the consistency of $\mathsf{PA}$. (For example, from $\mathsf{ZF}$, then you can easily construct a model of $\mathsf{PA}$, but the consistency of $\mathsf{ZF}$ is "more debatable" than that of $\mathsf{PA}$, so you haven't really gained anything.)
Gentzen's proof relies on infinitary processes (in particular, induction up to $\varepsilon_0$; see Wikipedia), and may not have been accepted by the Hilbert school (who sought purely finitary proofs of consistency). The ordinal $\varepsilon_0$ is important here because (assuming its consistency) $\mathsf{PA}$ cannot prove that it is well-founded, and it is basically this move that transcends $\mathsf{PA}$.
• @Dennis: It might be worth adding that Gentzen used the transfinite induction as the main tool here, but as far as $\sf PA$ goes, he used only a small fragment of it. Oct 16, 2014 at 12:40