*This is a minor variation of a question originally [asked on MSE](https://math.stackexchange.com/questions/4349128/partial-consistency-of-peano-arithmetic) by user779130 and bountied by me, without success. Throughout, "length" refers to the number of symbols, not lines, in a proof.*


For $T$ an "appropriate" theory, let $p\_T(n)$ be the length of the shortest $T$-proof of "There is no proof of $0=1$ in $\mathsf{PA}$ of length $<n$." We always have an exponential upper bound on the length of $p\_T$ by brute-force-checking, and sufficiently strong $T$s have $p\_T=O(1)$. However, beyond this very little is clear to me:


* Is $p\_{\mathsf{PA}}$ sub-exponential?
* If so, is $p\_{\mathsf{PRA}}$ sub-exponential?


(When I first read the original version of this question, I thought I recalled a theorem that $p\_{\mathsf{PA}}$ is in fact exponential, but I was unable to track it down. In fact, I already can't rule out the seemingly-ridiculous possibility of $p\_\mathsf{PRA}$ having polynomial-bounded growth rate.)



Proving short consistency: can we do better than brute force search?
Since the concept involves two theories, but the notation in the question only indicates one of them, I will instead write $p\_{S,T}(n)$ for the shortest $S$-proof of $\DeclareMathOperator\con{Con}\con\_T(\def\ob{\overline}\ob n)$, expressing that there is no $T$-proof of contradiction of length $<n$.


Here, each of $T,S$ is a consistent theory extending a suitable base theory (say, the theory $\def\pv{\mathrm{PV}\_1}\pv$ of polynomial-time functions, which is a weak subtheory of $I\Delta\_0+\Omega\_1$) with a fixed polynomial-time enumeration of axioms. To avoid trivializing a part of the question, let $\ob n$ denote the binary numeral defined by $\ob 0=0$, $\ob{2n}=S(S(0))\cdot\ob n$, and $\ob{2n+1}=S(\ob{2n})$, so that the length of the sentence $\con\_T(\ob n)$ is $\Theta(\log n)$.


Consequently, there is a trivial lower bound
$$p\_{S,T}(n)=\Omega(\log n)\tag1\label{lb}$$
for all $S$ and $T$. On the other hand, there is a trivial upper bound
$$p\_{S,T}(n)=2^{O(n)},\tag2\label{ub}$$
as we can just enumerate all strings of length $n$, and check that none of them is a $T$-proof of a contradiction.


We can study $p\_{S,T}$ in three different regimes:


**1.** If $S$ is sufficiently stronger than $T$, that is: if $S$ proves $\con\_T=\forall x\,\con\_T(x)$, then
$$p\_{S,T}(n)=\Theta(\log n),$$
thus the lower bound $\eqref{lb}$ is tight. Indeed, we can prove $\con\_T(\ob n)$ by taking a fixed proof of $\con\_T$ and instantiating the universal quantifier to $\ob n$.


**2.** If $T=S$ (including the case $p\_{\def\pa{\mathrm{PA}}\pa}=p\_{\pa,\pa}$ in the question), the problem was answered by Pudlák [1], who proved



> 
> **Theorem 1:** For any $T$, there are constants $c>\epsilon>0$ such that
> $$n^\epsilon<p\_{T,T}<n^c$$
> for sufficiently large $n$.
> 
> 
> 


Notice that both the lower bound and the upper bound here are nontrivial.


To be precise, Pudlák proves the polynomial upper bound only for finitely axiomatized theories $T$, and more generally, for theories axiomatized by schemata of a certain restricted form, which applies e.g. to PA and ZFC. The bounds were improved (under some restrictions) in Pudlák [2].


**3.** If $S$ is weaker than $T$ (including the case $p\_{\def\pra{\mathrm{PRA}}\pra}=p\_{\pra,\pa}$ in the question), the growth rate of $p\_{S,T}$ becomes a difficult open problem. If $T\supseteq S$, then Theorem 1 implies the polynomial lower bound
$$p\_{S,T}(n)>n^\epsilon,$$
but that’s just about all we know for a fact.


We have every reason to expect that if $T$ is sufficiently stronger than $S$, then the trivial upper bound $\eqref{ub}$ cannot be significantly improved, i.e., $p\_{S,T}$ is exponential. It seems likely that this should hold already when $T\supseteq S+\con\_S$. However, we cannot even prove the much weaker statement



> 
> **Conjecture 2:** For every $S$, there is $T$ such that $p\_{S,T}$ is not polynomially bounded.
> 
> 
> 


In fact, Krajíček and Pudlák [3] proved that Conjecture 2 is equivalent to



> 
> **Conjecture 3:** There is no optimal propositional proof system.
> 
> 
> 


Here, a *propositional proof system* (pps) is a polynomial-time predicate $P(\pi,\phi)$ (meaning “$\pi$ is a $P$-proof of $\phi$”) such that
$$\phi\in\def\taut{\mathrm{TAUT}}\taut\iff\exists\pi\:P(\pi,\phi),$$
where $\taut$ is the set of all classical propositional tautologies.
A pps $P$ *simulates* a pps $Q$ if there exists a polynomial $p$ such that
$$Q(\pi\_Q,\phi)\implies\exists\pi\_P\:\bigl(|\pi\_P|\le p(|\pi\_Q|+|\phi|)\land P(\pi\_P,\phi)\bigr),$$
and a pps $P$ is *optimal* if it simulates any other pps. A pps $P$ is *polynomially bounded* if there is a polynomial $p$ such that
$$\phi\in\taut\implies\exists\pi\:\bigl(|\pi|\le p(|\phi|)\land P(\pi,\phi)\bigr).$$
Any polynomially bounded pps is clearly optimal, but the converse is not necessarily true.


It is generally assumed that *every* pps requires proofs of exponential size to prove some tautologies. However, we are far from proving this; the weaker statement that there are no polynomially bounded pps is equivalent to the famous $\mathrm{NP\ne coNP}$ problem. We can only prove unconditional superpolynomial (or even exponential) lower bounds on weak proof systems such as Resolution. No nontrivial lower bounds are known even for the *Frege* proof system (called Hilbert outside proof complexity), which is the textbook proof system using a finite set of axiom schemata and schematic rules (modus ponens).


The proof of the equivalence of Conjecture 2 and Conjecture 3 works roughly as follows. On the one hand, for any theory $S$, we can define a proof system $Q\_S$ by
$$Q\_S(\pi,\phi)\iff \pi\text{ is an $S$-proof of “$\phi\in\taut$”}$$
(this is called the *strong proof system of $S$* in Pudlák [4]) and we show that if $S$ violates Conjecture 2, then $Q\_S$ is optimal. On the other hand, if $P$ is an optimal pps, then the theory axiomatized by the reflection principle
$$S=\pv+\forall\pi,\phi\:(P(\pi,\phi)\to\phi\in\taut)$$
violates Conjecture 2.


As already mentioned, it is consistent with current knowledge that Frege is polynomially bounded, and therefore optimal. Since the reflection principle for Frege is provable already in the base theory $\pv$, it follows that we cannot at present even disprove the statement



> 
> $p\_{S,T}$ is polynomially bounded for all $S$ and $T$.
> 
> 
> 


Thus, for example, we cannot prove anything about $p\_{\pra,\pa}$ besides the $n^\epsilon$ lower bound.


See also [5] for a discussion of statements related to Conjectures 2 and 3.


**References:**


[1] Pavel Pudlák: [*On the length of proofs of finitistic consistency statements in first order theories*](http://math.cas.cz/%7Epudlak/fin-con.pdf), in: Logic Colloquium '84 (J. B. Paris, A. J. Wilkie, G. M. Wilmers, eds.), Studies in Logic and the Foundations of Mathematics vol. 120, 1986, pp. 165–196, doi [10.1016/S0049-237X(08)70462-2](https://doi.org/10.1016/S0049-237X(08)70462-2).


[2] Pavel Pudlák: [*Improved bounds to the length of proofs of finitistic consistency statements*](http://math.cas.cz/%7Epudlak/improved.pdf), in: Logic and Combinatorics (S. G. Simpson, ed.), Contemporary Mathematics vol. 65, AMS, 1987, pp. 309–331.


[3] Jan Krajíček, Pavel Pudlák: [*Propositional proof systems, the consistency of first order theories and the complexity of computations*](http://math.cas.cz/%7Epudlak/propositional.pdf), Journal of Symbolic Logic 54 (1989), no. 3, pp. 1063–1079, doi [10.2307/2274765](https://doi.org/10.2307/2274765), jstor [2274765](https://www.jstor.org/stable/2274765).


[4] Pavel Pudlák: *Reflection principles, propositional proof systems, and theories*, [arXiv:2007.14835](https://arxiv.org/abs/2007.14835) [math.LO].


[5] Pavel Pudlák: [*Incompleteness in the finite domain*](https://math.cas.cz/%7Epudlak/inco.pdf), Bulletin of Symbolic Logic 23 (2017), no. 4, pp. 405–441, doi [10.1017/bsl.2017.32](https://doi.org/10.1017/bsl.2017.32).


