0

I have done meta-proofs of the consistency of FOL (Studied about 40 years ago), but have not done any for PA and have not looked at (and maybe now could not follow) Gentzen or the other proofs of PA. In looking at some characterizations of his proof, they seemed to assert that part of the proof actually showed that transfinite induction was unprovable, which seems to invoke inconsistency, but some of these talked about using a weaker 9th axiom.

Hence my question. Was PA consistent as originally stated or consistent only with a weaker 9th axiom?

Lee Hester
  • 1

1 Answers1

1

As mentioned in Mauro's comment, Gentzen's result was carried out in the theory of primitive recursive arithmetic along with the assumption that $\varepsilon_0$ is well-ordered. Gentzen proved this by proving the Hauptsatz, or cut-elimination theorem, and then the consistency of PA is a corollary of this.

However as far as I'm aware of how the proof was carried out, the Hauptsatz doesn't hold for PA alone, so to prove the consistency of PA this way, Gentzen instead proved the Hauptsatz for a theory $\mathsf{PA}_\omega$ of which PA is a subset. Cut elimination holds for $\mathsf{PA}_\omega$, so the empty sequent isn't deducible in $\mathsf{PA}_\omega$. Since all $\mathsf{PA}$-deductions are also $\mathsf{PA}_\omega$-deductions (but not vice versa), if the empty sequent were deducible in $\mathsf{PA}$ it would also be deducible in $\mathsf{PA}_\omega$, but we now know this is impossible. So we have shown PA must be consistent. Rathjen gives a nice, more detailed overview of Gentzen's workflow in "Proof theory: From arithmetic to set theory", in which $\mathsf{PA}_\omega$ is introduced on p.3.

C7X
  • 1,187