On the provability logic of bounded arithmetic
\(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 \textit{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 \textit{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.
- An inside view of EXP; or, The closed fragment of the provability logic of IΔ0 + Ω1 with a prepositional constant for EXP
- Logic of Proofs for Bounded Arithmetic
- Biological Perspectives Irreversible Lithium-Induced Neuropathy: Two Cases
- scientific article; zbMATH DE number 5037198
- scientific article; zbMATH DE number 1341927
- Cuts, consistency statements and interpretations
- scientific article; zbMATH DE number 4059391 (Why is no real title available?)
- Modal analysis of generalized rosser sentences
- On the \(\Sigma{}^ 0_ 1\)-conservativity of \(\Sigma{}^ 0_ 1\)- completeness
- On the proof of Solovay's theorem
- On the scheme of induction for bounded arithmetic formulas
- Provability interpretations of modal logic
- Rosser sentences
- The decision problem for exponential diophantine equations
- The provability logics of recursively enumerable theories extending Peano arithmetic at arbitrary theories extending Peano arithmetic
- On the scheme of induction for bounded arithmetic formulas
- Structure and definability in general bounded arithmetic theories
- On the \(\Sigma{}^ 0_ 1\)-conservativity of \(\Sigma{}^ 0_ 1\)- completeness
- Bounded arithmetic, proof complexity and two papers of Parikh
- On the bounded version of Hilbert's tenth problem
- A bounded arithmetic AID for Frege systems
- A proof theory for the logic of provability in true arithmetic
- Montague's paradox, informal provability, and explicit modal logic
- No escape from Vardanyan's theorem
- Provability logic: models within models in Peano arithmetic
- Quantified propositional calculi and fragments of bounded arithmetic
- scientific article; zbMATH DE number 4006264 (Why is no real title available?)
- Finite automata, real time processes and counting problems in bounded arithmetics
- PROVABILITY LOGIC IN THE GENTZEN FORMULATION OF ARITHMETIC
- A small reflection principle for bounded arithmetic
- Provability and interpretability logics with restricted realizations
- The second incompleteness theorem and bounded interpretations
- Bimodal logics for extensions of arithmetical theories
- Weak forms of the Regularity Principle in the presence of \documentclass{article}\usepackage{amssymb}\begin{document}\pagestyle{empty}$\bf {\mathsf {I}{\mathrm{E}}_1}$\end{document}
- scientific article; zbMATH DE number 2196511 (Why is no real title available?)
- Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
- Reflections on Orlov
- Solutions to the knower paradox in the light of Haack's criteria
- The bounded proof property via step algebras and step frames
- Feasible operations on proofs: the logic of proofs for bounded arithmetic
This page was built for publication: On the provability logic of bounded arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685071)
