[FOM] Gentzen's consistency proof

[WILLIAM TAIT]

Sorry to be so slow responding, Tim.

For a suitable system of notation for the ordinals < \epsilon_0: 

Call a cut-free deduction of a sequent in PA without math induction but with the \omega-rule *annotated* if each step has an ordinal < \epsilon_0 attached to it so that ordinals decrease going from conclusion to premise in each inference. 

Gentzen (essentially) defined, uniformly primitive recursive in a given deduction in PA of a sequent \Gamma |- A, a function f such that f(n) codes the n-th approximation of an annotated deduction of \Gamma |- A.  (Because of the omega-rule, `n-th approximation’ is in width as well as in height.) Will this help?

Best,
Bill 

> On May 16, 2018, at 8:43 PM, tchow <tchow at alum.mit.edu> wrote:
> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom