Provability and interpretability logics with restricted realizations

DOI10.1215/00294527-1715653MaRDI QIDQ435232zbMATH OpenOpenAlexWikidataFDO

Authors Joost J. Joosten, Thomas F. III Icard

Publication date 11 July 2012

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2006.10539, https://projecteuclid.org/euclid.ndjfl/1336588246

zbMATH Keywords

GLPinterpretability logiclinear framesPRAprovability logicrestricted substitutions

Mathematics Subject Classification ID

Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Abstract: The provability logic of a theory T is the set of modal formulas, which under any arithmetical realization are provable in T . We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $Gamma$. We make an analogous modification for interpretability logics. This is a paper from 2012. We first studied provability logics with restricted realizations, and show that for various natural candidates of theory T and restriction set $Gamma$, where each sentence in $Gamma$ has a well understood (meta)-mathematical content in T, the result is the logic of linear frames. However, for the theory Primitive Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic, by capitalizing on the well-studied relationship between PRA and I$Sigm{a}_1$. We then study interpretability logics, obtaining some upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely relatively to linear frames. The technique is also applied to yield the non-trivial result that IL(PRA) $subset$ ILM.

Review text

The provability logic GL (Gödel-Löb) is a simple modal description of provability. The axioms of GL are all tautologies, \(\square (A\rightarrow B)\rightarrow (\square A\rightarrow \square B),\) \(\square (\square A\rightarrow A)\rightarrow \square A.\) The inference rules of GL are modus ponens and necessitation \(A/ \square A.\) Modal provability logic usually studies the operator `provability in PA' as the modal connective necessary, \(\square.\) The propositional provability logic GL was axiomatized by \textit{R. M. Solovay} [Isr. J. Math. 25, 287--304 (1976; Zbl 0352.02019)].NEWLINENEWLINENEWLINE The paper under review deals with restricted cases of Solovay's theorem where an alternative proof method is available. The authors study provability logics of some theory with restricted arithmetical realizations. The result is a logic of linear frames. After that, the interpretability logics are considered. An interpretability logic is a modal description of the notion of relativized interpretability between two theories. For detailed definitions see e.g. [\textit{A. Visser}, CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020); \textit{G. Japaridze} and \textit{D. de Jongh}, in: Handbook of proof theory. Amsterdam: Elsevier, 475--546 (1998; Zbl 0915.03019)]. An interpretability logic can be viewed as an extension of provability logic. The authors give upper bounds for the logic IL(PRA). The characterization of IL(PRA) remains a major open question in interpretability logics (see e.g. [\textit{M. Bílkova} et al., Ann. Pure Appl. Logic 16, No. 2, 128--138 (2009; Zbl 1184.03011)]). It is necessary to mention that upper bounds are connected with linear frames, too. The new method is used to obtain the nontrivial result \(\mathrm{IL(PRA)}\subset \mathrm{ILM}\).

Recommendations

• Interpretability in PRA
• The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)
• TWO NEW SERIES OF PRINCIPLES IN THE INTERPRETABILITY LOGIC OF ALL REASONABLE ARITHMETICAL THEORIES
• scientific article; zbMATH DE number 218496
• scientific article; zbMATH DE number 1215477

Cites work

• A Finitary Treatment of the Closed Fragment of Japaridze's Provability Logic
• A new principle in the interpretability logic of all reasonable arithmetical theories
• A note on the normal form of closed formulas of interpretability logic
• A propositional logic with explicit fixed points
• A topological study of the closed fragment of GLP
• An effective fixed-point theorem in intuitionistic diagonalizable algebras. (The algebraization of the theories which express Theor. IX.)
• Bimodal logics for extensions of arithmetical theories
• scientific article; zbMATH DE number 4059391 (Why is no real title available?)
• scientific article; zbMATH DE number 1215477 (Why is no real title available?)
• scientific article; zbMATH DE number 1215499 (Why is no real title available?)
• scientific article; zbMATH DE number 1045790 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• scientific article; zbMATH DE number 218514 (Why is no real title available?)
• scientific article; zbMATH DE number 3351517 (Why is no real title available?)
• Interpretability in PRA
• Kripke semantics for provability logic GLP
• Modal logic
• On n-quantifier induction
• On strong provability predicates and the associated modal logics
• On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
• On the proof of Solovay's theorem
• On the provability logic of bounded arithmetic
• Reflection principles and provability algebras in formal arithmetic
• Solution of a problem of Leon Henkin
• The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)
• The interpretability logic of all reasonable arithmetical theories. The new conjecture
• The interpretability logic of Peano arithmetic
• The logic of \(\Pi_ 1\)-conservativity
• The logic of \(\Pi_ 1\)-conservativity continued
• Undecidable theories
• Ways of proof theory. Collected papers by speakers of the colloquium and workshop held on the occasion of the retirement of Wolfram Pohlers, July 17--19, 2008, Münster, Germany

Cited in

(9)

• Interpretability suprema in Peano arithmetic
• Interpretability degrees of finitely axiomatized sequential theories
• The polytopologies of transfinite provability logic
• The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)
• Provability in finite subtheories of PA and relative interpretability: a modal investigation
• Topological interpretations of provability logic
• scientific article; zbMATH DE number 3269880 (Why is no real title available?)
• Theory and application of labelling techniques for interpretability logics
• An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics

This page was built for publication: Provability and interpretability logics with restricted realizations

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