[FOM] Convincing Edward Nelson that PA is consistent

[Timothy Y. Chow]

After sending my last message, I realized that there are a couple of 
obvious additional comments that I should have made.  Consider the 
statement

(*) There is no PA proof of "0=S0" of length < 2^1000.

It would go a long way towards answering the questions I raised if one 
could get good bounds on the length of the shortest proof of (*) in 
various systems S.

Even for S = PA, it's not clear to me that (*) has a proof of length less 
than 2^1000, although I think it is plausible that there might be.  Note 
that naively exhausting all PA proofs is going to require something like 
c^(2^1000) steps for some constant c.

There's a pedestrian way to go about proving (*) in PA.  The tough part is 
proving that there's no infinite decreasing sequence of ordinals below 
epsilon_0.  Since we are given an upper bound of 2^1000, we don't have to 
go all the way up to epsilon_0; I think we can stop with w^w^...^w at 
worst, where the tower has height 2^1000.  Constructing a PA proof of this 
can be done by induction on height, but at first glance this might take us 
significantly over 2^1000.

For weaker systems S, say PRA or below, I would conjecture that there 
isn't any proof of (*) shorter than 2^1000.  It would be very interesting 
to me to see any kind of provable lower bound, even for S being very weak 
(say, bounded arithmetic).

Such results might show that this avenue towards "convincing Nelson that 
PA is consistent" is doomed, but even a negative result of this sort would 
be interesting in my opinion.  Note that Nelson has explicitly rejected 
PRA and has even said things that suggest he might reject EFA.

Tim