[FOM] Polynomial Consistency Proofs
freund at mathematik.tu-darmstadt.de
freund at mathematik.tu-darmstadt.de
Thu Jun 21 04:06:11 EDT 2018
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
More information about the FOM
mailing list