[FOM] Convincing Edward Nelson that PA is consistent

[katzmik at macs.biu.ac.il]

It may be worth clarifying that, as far as I know, Nelson accepted that there
was a gap in his argument for inconsistency as shown by Tao.  So comments to
the effect that Nelson "rejected" this or that system, or suggestions that he
might have thought such systems "inconsistent", merely mean that he did not
have full confidence in such systems philosophically speaking (rather than he
believed in the existence of a specific inconsistency).  MK

On Tue, June 19, 2018 18:04, 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
>