# [FOM] Convincing Edward Nelson that PA is consistent

Timothy Y. Chow tchow at math.princeton.edu
Wed Jun 20 11:20:47 EDT 2018

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