[FOM] Consistency of PA, again

[WILLIAM TAIT]

Tim, 

Assertion A makes no sense. It says that there is a TM that generates an infinite descending sequence from  \epsilon_0. Also kit makes no reference to deduction in PA. I expect you meant something else.

One remark about this and your earlier posts. The TM does not generate a simple sequence of sequents together with ordinals, but rather, at the i-th step  it yields the i-th approximation of a tree. At each node of the tree is a sequent together with an ordinal, such that the ordinals descend along each branch. The tree that is generates has unary, binary and \omega branchings—corresponding to acting on A v B, \exists x A(x) for one branching, A&B for two and \forall x A(x) for \omega branching.  What in fact the TM generates is a cut-free deduction of the initial sequent. 

As you suggested, the TM can be thought of as playing a winning strategy in a two-person game—the winning strategy being the cut-free deduction. 

Bill

 
> On Jun 4, 2018, at 9:35 PM, Timothy Y. Chow <tchow at princeton.edu> wrote:
> 
> 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.
> 
> Question 1.  Is Assertion A disprovable in PRA?
> 
> I'm guessing that the answer is no, but I'm not sure.  If the answer to Question 1 is no, then my followup question is this:
> 
> Question 2.  Is it provable in PRA that "PA is inconsistent" implies Assertion A?
> 
> I'd like the answer to Question 2 to be yes, but somehow I suspect that the answer is no.  It doesn't seem to me that any of Gentzen's proofs actually constructs such an M from a PA-proof of 1=2.  But this might be because I still don't understand Gentzen's proofs well enough.
> 
> If the answer to Question 2 is no, then is there any PRA-consequence of "PA is inconsistent" that at all resembles Assertion A?  What I'm trying to get at is whether there is any (false) consequence of "PA is inconsistent" that is more "concrete" than the mere failure of induction up to epsilon_0, where by "concrete" I mean some direct statement about ordinal notations.
> 
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom