[FOM] Convincing Edward Nelson that PA is consistent

Timothy Y. Chow tchow at math.princeton.edu
Tue Jun 19 11:04:33 EDT 2018

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

(*) 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.


More information about the FOM mailing list