[FOM] Consistency of PA, again
Timothy Y. Chow
tchow at princeton.edu
Mon Jun 4 22:35:30 EDT 2018
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
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
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
More information about the FOM