[FOM] Gentzen's consistency proof

[tchow]

On 2018-05-14 10:28, WILLIAM TAIT wrote:
> Since there are no proofs of 0=1(I hope!), maybe you need to
> formulate your question.

Here is an attempt to be more precise.

I've been focusing on Gentzen's first proof, that uses game-theoretic 
concepts and trees.  As I understand it, to every true statement of 
arithmetic one can associate a "reduction," which is an effective 
strategy for winning a certain syntactic game.  A skeptic who is queasy 
about infinite sets and the concept of a "true statement of arithmetic" 
can nevertheless accept that Gentzen has a way of explicitly 
constructing reductions (which can be represented explicitly as Turing 
machines that implementing the winning strategy) for the "base case" 
and, for each deductive rule in PA, effectively producing a reduction 
for the result of the deduction.  (I'm being intentionally vague here 
about the specific implementation of PA since I believe it doesn't 
really matter for my question.)

The most obvious avenue for the skeptic that I can see is that the 
skeptic might not believe that Gentzen's algorithm for producing new 
reductions (Turing machines) always produces Turing machines that 
*halt*, when we track through a PA-proof.  The skeptic can therefore 
imagine a PA-proof of 0=1, and imagine running Gentzen's algorithm to 
produce a corresponding sequence of reductions.  But it seems to me that 
the skeptic is going to say that the alleged reduction of 0=1 doesn't 
halt.  To me as a non-skeptic, this would seem to be a claim that a 
particular ordinal < epsilon_0 admits an infinite decreasing 
subsequence.

So I guess what I'm wondering if this line of reasoning can be 
formalized in, say, PRA, as a proof of an assertion that the procedure 
I've described above does indeed effectively produce a non-halting 
Turing machine (that is traversing a decreasing subsequence in some 
ordinal < epsilon_0) from a PA-proof of 0=1.

Tim