[FOM] Consistency of PA, again

[Timothy Y. Chow]

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