[FOM] Convincing Edward Nelson that PA is consistent

[Alasdair Urquhart]

Pavel Pudlak has some good results in this area.  His paper
"Improved bounds to the length of proofs of finitistic consistency
statements" has a lower bound of n/(log n)^2 for proofs of
Con_T(n), which says "There is no proof of 0=1 of length <=n in T".
This paper appeared in Contemporary Mathematics Volume 65, 1987.


On Tue, 19 Jun 2018, Timothy Y. Chow wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>