[FOM] Gentzen's consistency proof

[WILLIAM TAIT]

Dear Tim,

Since there are no proofs of 0=1(I hope!), maybe you need to  formulate your question.

Bill

> On May 10, 2018, at 10:14 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> 
> I'm trying to understand Gentzen's consistency proof of PA.  There is something that I think follows as a corollary of the proof but I'm wondering if I'm missing something.
> 
> Suppose I write down explicitly a Turing machine M that represents epsilon_0.  That is, M takes a pair of natural numbers (a,b) as input and outputs either 0 or 1, and I can prove (using ZF or whatever) that if I interpret an output of 1 as "a < b" then I get a total ordering on the natural numbers that is order isomorphic to epsilon_0.
> 
> Does Gentzen's proof give an effective procedure for taking a PA-proof of 0=1 and producing a Turing machine M' that outputs an infinite sequence of natural numbers a_1, a_2, a_3, ... such that a_i > a_{i+1} for all i, where ">" denotes the aforementioned epsilon_0 ordering computed by M?
> 
> I think that the answer is yes but I'm a little concerned that ineffectivity might creep in somewhere.
> 
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom