×

On the provability logic of bounded arithmetic. (English) Zbl 0803.03037

\(I\Delta_ 0+ \Omega_ 1\) is a weak fragment of Peano Arithmetic which has received much attention in recent years. Its weakness consists in the fact that it does not prove that exponentiation is a total function (\(I\Delta_ 0+\Omega_ 1\) has an axiom expressing the totality of the sub-exponential function \(x^{\log(x)}\) and the scheme of induction restricted to bounded formulas).
The authors study the provability logic of \(I\Delta_ 0+ \Omega_ 1\) in the spirit of a classical paper of R. M. Solovay [Isr. J. Math. 25, 287-304 (1976; Zbl 0352.02019)], which considers the corresponding problem for Peano Arithmetic. Solovay’s result is known to hold for every reasonable theory proving the totality of the exponential function, but is not known to be true for weak theories like \(I\Delta_ 0+ \Omega_ 1\).
The authors prove some containments of the form \(\text{L}\subseteq\text{PL}\Omega\subset\text{Th}({\mathcal C})\), where L is the provability logic of PA, \(\text{PL}\Omega\) is the provability logic of \(I\Delta_ 0+ \Omega_ 1\), and \(\mathcal C\) is a suitable class of Kripke frames. They also prove that it is unlikely that \(\text{PL}\Omega\) is the theory of a class of Kripke frames, unless \(\text{PL}\Omega=\text{L}\). More precisely if \(\text{PL}\Omega=\text{Th}({\mathcal C})\), then every binary tree can be homomorphically embedded into some frame of \(\mathcal C\). It remains open whether \(\text{PL}\Omega=\text{L}\).
The latter problem might depend on difficult questions of computational complexity. In fact if \(\text{PL}\Omega\neq \text{L}\), it would follow that \(I\Delta_ 0+ \Omega_ 1\) does not prove its completeness with respect to \(\Sigma^ 0_ 1\)-formulas, and a fortiori it does not prove the Matiyasevich-Robinson-Davis-Putnam theorem (every r.e. set is diophantine). On the other hand if \(I\Delta_ 0+ \Omega_ 1\) did prove its completeness with respect to \(\Sigma^ 0_ 1\)-formula, it would follow not only that \(\text{L}=\text{PL}\Omega\), but also that \(\text{NP}=\text{co-NP}\). The possibility remains that \(\text{L}= \text{PL}\Omega\) and that one could give a proof of this fact without making use of \(\Sigma^ 0_ 1\)-completeness. Such a project is not without challenge due to the ubiquity of \(\Sigma^ 0_ 1\)-completeness in the whole area of provability logic.
Reviewer: A.Berarducci

MSC:

03F30 First-order arithmetic and fragments
03B45 Modal logic (including the logic of norms)

Citations:

Zbl 0352.02019
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Buss, S., Bounded Arithmetic (1986), Bibliopolis: Bibliopolis Napoli, edizioni di filosofia e scienze · Zbl 0649.03042
[2] Berarducci, A.; Verbrugge, R., On the metamathematics of weak theories, ITLI Prepublication Series for Mathematical Logic and Foundations (1991), University of Amsterdam, ML-91-02
[3] Davis, M.; Putnam, H.; Robinson, J., The decision problem for exponential diophantine equations, Ann. of Math., 74, 425-436 (1961) · Zbl 0111.01003
[4] Guaspari, D.; Solovay, R. M., Rosser sentences, Ann. Math. Logic, 16, 81-99 (1979) · Zbl 0426.03062
[5] de Jongh, D.; Jumelet, M.; Montagna, F., On the proof of Solovay’s theorem, Studia Logica, 50 (1991) · Zbl 0744.03057
[6] Soviet Math. Dokl., 354-357 (1970), English translation
[7] Pudlák, P., On the length of proofs of finistic consistency statements in first order theories, (Paris, J. B.; Wilkie, A. J.; Wilmers, G. M., Logic Colloquium ’84 (1986), North-Holland: North-Holland Amsterdam)
[8] Pudlák, P., Cuts, consistency statements and interpretations, J. Symbolic Logic, 50, 2 (1985) · Zbl 0569.03024
[9] Solovay, R. M., Provability interpretations of modal logic, Israel J. Math., 25, 287-304 (1976) · Zbl 0352.02019
[10] Solovay, R. M., On interpretability in set theories, Manuscript (1976)
[11] S̆vejdar, V., Modal analysis of generalized Rosser sentences, J. Symbolic Logic, 48, 986-999 (1983) · Zbl 0543.03010
[12] Verbrugge, R., Does Solovay’s Completeness Theorem Extend to Bounded Arithmetic?, Master’s thesis (1988), University of Amsterdam
[13] Verbrugge, R., Σ-completeness and bounded arithmetic, ITLI Prepublication Series for Mathematical Logic and Foundations (1989), University of Amsterdam, ML-89-05
[14] Visser, A., On the \(Σ^0_1\)-conservativity of \(Σ^0_1\)-completeness, Notre Dame J. Formal Logic, 32, 554-561 (1991) · Zbl 0747.03026
[15] Wilkie, A. J.; Paris, J. B., On the scheme of induction for bounded arithmetic formulas, Ann. Pure Appl. Logic, 35, 261-302 (1987) · Zbl 0647.03046
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.