Short proofs for slow consistency (Q2176406)

For a consistent, polynomial-time axiomatized theory \(T\) containing some arithmetic, let \(\mathrm{Con}_x(T)\) be a natural formalization of the statement that there is no proof of contradiction in \(T\) containing at most \(x\) symbols. [\textit{P. Pudlák}, Stud. Logic Found. Math. 120, 165--196 (1986; Zbl 0619.03037)] showed that for any standard natural number \(n\), a theory \(T\) as above can prove \(\mathrm{Con}_n(T)\) by a proof of size polynomial in \(n\). In contrast, Pudlák [loc. cit.] has also conjectured that \(T\) will no longer have polynomial-size proofs of \(\mathrm{Con}_n(T + \mathrm{Con}(T))\). The conjecture has important implications for computational complexity, propositional proof complexity, and related fields. In this paper, the authors consider the problem whether PA has small proofs of \(\mathrm{Con}_n(\mathrm{PA} + \mathrm{Con}^*(\mathrm{PA}))\), where \(\mathrm{Con}^*(\mathrm{PA})\) is the ``slow consistency'' principle of [\textit{S.-D. Friedman} et al., Ann. Pure Appl. Logic 164, No. 3, 382--393 (2013; Zbl 1263.03055)]: ``for every \(x\) such that \(F_{\epsilon_0}(x)\) exists, \(\mathrm{Con}(\mathrm{I}\Sigma_x)\) holds''. Here, \(F_{\epsilon_0}\) is the \(\epsilon_0\)-th function in the Hardy hierarchy of fast-growing functions. \(\mathrm{PA}\) does not prove that \(F_{\epsilon_0}\) is a total function, and indeed \(\mathrm{PA} + \mathrm{Con}^*(\mathrm{PA})\) is strictly intermediate in strength between \(\mathrm{PA}\) and \(\mathrm{PA} + \mathrm{Con}(\mathrm{PA})\). The main theorem of the paper is that \(\mathrm{PA}\) can prove \(\mathrm{Con}_n(\mathrm{PA} + \mathrm{Con}^*(\mathrm{PA}))\) by proofs of size polynomial in \(n\). Moreover, the result still holds if \(\mathrm{Con}^*(\mathrm{PA})\) is strengthened to a ``slow uniform \(\Pi_2\) reflection'' principle, \(\mathrm{RFN}^*_{\Pi_2}(\mathrm{PA})\), which says ``for every \(x\) such that \(F_{\epsilon_0}(x)\) exists, no false \(\Pi_2\) statement can be derived from \(\mathrm{PA}\) by a proof containing at most \(x\) symbols''. The proof of the main theorem has two major ingredients. The first of these is showing that already \(\mathrm{I}\Sigma_1\) proves ``for every \(x\), if \(F_{\epsilon_0}(x)\) exists, then \(\mathrm{Con}_x(\mathrm{PA} + \mathrm{Con}^*(\mathrm{PA}))\) holds''. This is achieved by interpreting \(\mathrm{RFN}^*_{\Pi_2}(\mathrm{PA})\) as a sentence expressing the totality of a function that grows considerably slower than \(F_{\epsilon_0}\), and then analyzing that sentence in terms of an infinitary proof system due to \textit{W. Buchholz} and \textit{S. Wainer} [Contemp. Math. 65, 179--198 (1987; Zbl 0635.03056)]. Proving the main theorem then comes down to showing that for standard \(n\), \(\mathrm{PA}\) is able to prove the existence of the value \(F_{\epsilon_0}(n)\) by proofs of size polynomial in \(n\). Such proofs are obtained using the transfinite induction available in \(\mathrm{PA}\). Their construction is more or less as expected but with some technical wrinkles. Interestingly, the statement ``for every \(x\), if \(F_{\epsilon_0}(x)\) exists, then \(\mathrm{Con}_x(\mathrm{PA} + \mathrm{Con}(\mathrm{PA}))\) holds'' is unprovable even in \(\mathrm{PA}\). This may suggest that the main theorem of the paper says more about the weakness of \(\mathrm{Con}^*(\mathrm{PA})\) compared to \(\mathrm{Con}(\mathrm{PA})\) than about Pudlák's conjecture [loc. cit.] as such.