[FOM] Consistency of PA, again

[freund at mathematik.tu-darmstadt.de]

> Assertion A.  There exists a Turing machine M that, for every i>0, outputs
> a notation M(i) for an ordinal below epsilon_0, and such that M(i)>M(i+1)
> for all i.
>
> Question 1.  Is Assertion A disprovable in PRA?
>
> Question 2.  Is it provable in PRA that "PA is inconsistent" implies
> Assertion A?

The answer to Question 2 is yes. As a consequence, the answer to Question
1 is no. The following book explains how this follows from Gentzen's
investigation (see Lemma 12.79):

Gaisi Takeuti: "Proof Theory", Studies in Logic and the Foundations of
Mathematics vol. 81 (1975).

It can also be helpful to look at reformulations of Gentzen's work in
terms of infinite proof trees. The following papers use this approach to
answer your Question 2 (see Theorem 4.6 and Theorem 4.5, respectively):

Wilfried Buchholz: "Notation systems for infinitary derivations", Archive
for Mathematical Logic 30 (1991) 277-296.

Harvey Friedman and Michael Sheard: "Elementary descent recursion and
proof theory", Annals of Pure and Applied Logic 71 (1995) 1-45.

The connection between infinite proof trees and Gentzen's original
approach is explained in the following paper:

Wilfried Buchholz: "Explaining Gentzen's Consistency Proof within
Infinitary Proof Theory". In: "Computational Logic and Proof Theory. Fifth
Kurt G"odel Colloquium, KGC '97", ed. by G. Gottlob, A. Leitsch, D.
Mundici, Lecture Notes in Computer Science vol. 1289 (1997) pp. 4-17.

There are even more natural/mathematical statements connected to the
well-foundedness of epsilon_0. An example related to Kruskal's theorem can
be found in Theorem 12.75 of Takeuti's book (the result is due to Harvey
Friedman).

Anton