[FOM] Polynomial Consistency Proofs

[freund at mathematik.tu-darmstadt.de]

In his post "Convincing Edward Nelson that PA is consistent" Timothy Chow
wrote:

> 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.

It is true that the big question remains wide open. However, there are
some interesting recent results: Pavel Hrubes has used Rosser-style
diagonalization to construct theories S and T such that

* T is a proper extension of S,
* S has polynomial in n proofs for the statements Con(T,n).

In fact, Hrubes' result is somewhat stronger. A precise statement can be
found in Theorem 3.4 of

Pavel Pudlak, Incompleteness in the finite domain, Bulletin of Symbolic
Logic 23(4) 2017, pp. 405-441.

A natural example (which does not rely on diagonalization) has also been
discovered: One can take S=PA and T=PA+Con*(PA), where Con*(PA) is the
slow consistency statement introduced by Sy David Friedman, Michael
Rathjen and Andreas Weiermann. The fact that PA has polynomial proofs for
Con(PA+Con*(PA),n) is proved in

Anton Freund and Fedor Pakhomov, Short Proofs for Slow Consistency, 2017.
Preprint available at https://arxiv.org/abs/1712.03251

Anton