Short proofs for slow consistency

Recursive functions and relations, subrecursive hierarchies (03D20) Recursive ordinals and ordinal notations (03F15) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)

Abstract: Let

o p e r a t o r n a m e C o n (m a t h b f T)! e s t r i c t i o n! x

denote the finite consistency statement "there are no proofs of contradiction in

m a t h b f T

with

l e q x

symbols". For a large class of natural theories

m a t h b f T

, Pudl'ak has shown that the lengths of the shortest proofs of

o p e r a t o r n a m e C o n (m a t h b f T)! e s t r i c t i o n! n

in the theory

m a t h b f T

itself are bounded by a polynomial in

n

. At the same time he conjectures that

m a t h b f T

does not have polynomial proofs of the finite consistency statements

o p e r a t o r n a m e C o n (m a t h b f T + o p e r a t o r n a m e C o n (m a t h b f T))! e s t r i c t i o n! n

. In contrast we show that Peano arithmetic (

m a t h b f P A

) has polynomial proofs of

o p e r a t o r n a m e C o n (m a t h b f P A + o p e r a t o r n a m e {C o n}^{*} (m a t h b f P A))! e s t r i c t i o n! n

, where

o p e r a t o r n a m e {C o n}^{*} (m a t h b f P A)

is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement

o p e r a t o r n a m e C o n (m a t h b f P A)

is equivalent to

v a r e p s i l o n_{0}

iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.

Review text

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.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Short proofs for slow consistency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2176406)