[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