[FOM] Consistency of PA, again

[Dennis E. Hamilton]

-----Original Message-----
From: Timothy Y. Chow
Sent: Monday, June 4, 2018 19:36
Subject: [FOM] Consistency of PA, again

Recently, I posed some questions about Gentzen's consistency proof, but I
have so far been unable to answer them satisfactorily, even with Bill Tait's
suggestion.  So let me try a slightly different tack.  Consider the
following assertion.

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.

I believe that Assertion A is expressible in PRA.  Ordinal notations for
ordinals below epsilon_0, and the order relation, are primitive recursive.


[orcmid]

I have concerns about Assertion A.

First, are the i in M(i) to be taken as natural numbers encoded in some
manner or is by a Turing Machine M(i) is M meant as a schema for a
denumerable family of TMs?  And also, the ">" in M(i) > M(i+1) refers to the
strict ordering of the ordinals as encoded in the outputs of the machine(s)?

Secondly, however that is cleared up, is it not a matter of concern that,
number-theoretically, the condition M(i) > M(i+1) is beyond impredicative?
If that is the case, I suggest that there are no such (terminating) TMs,
since it is not clear how an M(1) result, and any of the others, are ever
produced, TMs being operationally-definable yet ordinals are not enumerable
from "above."   I daresay there is no such recursive function, and ">" being
primitive recursive is of no help.

 - Dennis