# [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
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
```