Hard provability logics

DOI10.1007/978-3-030-53654-1_9MaRDI QIDQ2658282zbMATH OpenOpenAlexFDO

Authors Mojtaba Mojtahedi

Publication date 19 March 2021

Full work available at URL https://arxiv.org/abs/1911.04284

zbMATH Keywords

Heyting arithmetic HAintuitionistic logicPeano arithmetic PAprovability logicrelative provability logicrreductionstandard model

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Abstract: Let $mathcalPL(sfT,s^{\prime }fT)$ and $mathcal{PL}_{Sigm{a}_1}(sfT,s^{\prime }fT)$ respectively indicates the provability logic and $Sigm{a}_1$-provability logic of $sfT$ relative in $sfT\text{'}$. In this paper we characterize the following relative provability logics: $mathcal{PL}_{Sigm{a}_1}(sfHA,mathbbN)$, $mathcal{PL}_{Sigm{a}_1}(sfHA,sfPA)$, $mathcal{PL}_{Sigm{a}_1}({sfHA}^{\ast },mathbbN)$, $mathcal{PL}_{Sigm{a}_1}({sfHA}^{\ast },sfPA)$, $mathcalPL(sfPA,sfHA)$, $mathcal{PL}_{Sigm{a}_1}(sfPA,sfHA)$, $mathcalPL({sfPA}^{\ast },sfHA)$, $mathcal{PL}_{Sigm{a}_1}({sfPA}^{\ast },sfHA)$, $mathcalPL({sfPA}^{\ast },sfPA)$, $mathcal{PL}_{Sigm{a}_1}({sfPA}^{\ast },sfPA)$, $mathcalPL({sfPA}^{\ast },mathbbN)$, $mathcal{PL}_{Sigm{a}_1}({sfPA}^{\ast },mathbbN)$ (see Table ef{Table-Theories}). It turns out that all of these provability logics are decidable. The notion of {em reduction} for provability logics, first informally considered in cite{reduction}. In this paper, we formalize a generalization of this notion (Cref{Definition-Reduction-PL}) and provide several reductions of provability logics (See diagram ef{Diagram-full}). The interesting fact is that $mathcal{PL}_{Sigm{a}_1}(sfHA,mathbbN)$ is the hardest provability logic: the arithmetical completenesses of all provability logics listed above, as well as well-known provability logics like $mathcalPL(sfPA,sfPA)$, $mathcalPL(sfPA,mathbbN)$, $mathcal{PL}_{Sigm{a}_1}(sfPA,sfPA)$, $mathcal{PL}_{Sigm{a}_1}(sfPA,mathbbN)$ and $mathcal{PL}_{Sigm{a}_1}(sfHA,sfHA)$ are all propositionally reducible to the arithmetical completeness of $mathcal{PL}_{Sigm{a}_1}(sfHA,mathbbN)$.

Recommendations

• Reduction of provability logics to _1-provability logics
• Provability logics relative to a fixed extension of Peano arithmetic
• scientific article; zbMATH DE number 4087630
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
• scientific article; zbMATH DE number 1341927

Cites work

• A Note on Indicator-Functions
• Arithmetization of metamathematics in a general setting
• Constructivism in mathematics. An introduction. Volume II
• scientific article; zbMATH DE number 3719132 (Why is no real title available?)
• scientific article; zbMATH DE number 1215477 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• scientific article; zbMATH DE number 5037198 (Why is no real title available?)
• Intermediate logics and the de Jongh property
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On the admissible rules of intuitionistic propositional logic
• On the completenes principle: A study of provability in heyting's arithmetic and extensions
• Provability interpretations of modal logic
• Provability logic and the completeness principle
• Reduction of provability logics to _1-provability logics
• Self-reference and modal logic
• Solution of a problem of Leon Henkin
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}^{*}\)
• The de Jongh property for basic arithmetic
• The disjunction property implies the numerical existence property
• The interpretability logic of Peano arithmetic

Cited in

(3)

• Reduction of provability logics to _1-provability logics
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Relative unification in intuitionistic logic: towards the provability logic of HA

This page was built for publication: Hard provability logics

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