[FOM] Convincing Edward Nelson that PA is consistent

[Timothy Y. Chow]

I wrote:

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

Harvey Friedman pointed out to me that there is relevant word by him and 
(later) Pudlak.  For a recent survey, see

Incompleteness in the finite domain, by Pavel Pudlak.
https://arxiv.org/pdf/1601.01487.pdf

Here's a brief summary of the results that are most relevant to my 
question.  Let Con(T,n) be the statement that there is no proof of a 
contradiction from the axioms of T whose length is shorter than n.  For a 
large family of T, including PA, Friedman established an n^epsilon lower 
bound on the length of a proof of Con(T,n) from T itself, and Pudlak 
established a poly(n) upper bound.

The poly(n) upper bound is exponentially better than naively exhausting 
over all proofs, but is perhaps philosophically not so interesting, since 
if you find proofs from T convincing then presumably you already accept 
Con(T).  What is more relevant for the question I asked originally is the 
length of a proof of Con(T,n) in S where S is weaker than T.  Here the 
situation is unfortunately less satisfactory because we bump up against 
standard conjectures in complexity theory that we have no idea how to 
prove.  Conjecturally, though, if T proves Con(S) then there is a 
superpolynomial (in n) bound on the length of a proof of Con(T,n) in S.

If the conjecture is true then that means there's no hope of showing 
someone like Nelson a proof of Con(PA, 2^1000) or even Con(PA, 2^100) that 
he "believes," because he only believes systems weaker than PRA, and any 
such "Nelson-believable" proof is going to be infeasibly large.

Tim