[FOM] Gentzen's consistency proof

[tchow]

On 2018-05-14 19:04, I wrote:
> 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.

As I talk through this, I feel that I'm pinpointing my 
question/confusion
better with each iteration.  Here's another attempt to be more precise.

Let us focus on models of PRA + "PA is inconsistent."  Since PA is 
really
consistent, such models must be nonstandard, and the "proofs" of 0=1 
must
have nonstandard length.  What I think we can get out of Gentzen's proof
is a way to associate a "Turing machine" (representing a reduction) to
each step of the PA-proof of 0=1; in our nonstandard model, these Turing
machines may be nonstandard.  In a standard model, these Turing machines
will traverse a (finite) decreasing sequence in some ordinal < 
epsilon_0.
In a model of PRA + "PA is inconsistent," what I think happens (and this
is the part I'm least sure about) is that we get a nonstandard Turing
machine associated with "0=1" that doesn't halt, even nonstandardly.  Is
this right?

Tim Chow