Provability and interpretability logics with restricted realizations

DOI10.1215/00294527-1715653zbMATH Open1255.03054arXiv2006.10539OpenAlexW2086071144WikidataQ119883088 ScholiaQ119883088MaRDI QIDQ435232FDOQ435232

Thomas F. III Icard, Joost J. Joosten

Publication date: 11 July 2012

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

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.

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

zbMATH Keywords

provability logicinterpretability logicGLPlinear framesPRArestricted substitutions

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modal logic
• Undecidable theories
• A propositional logic with explicit fixed points
• Reflection principles and provability algebras in formal arithmetic
• On strong provability predicates and the associated modal logics
• Solution of a problem of Leon Henkin
• On the proof of Solovay's theorem
• The logic of \(\Pi_ 1\)-conservativity continued
• A new principle in the interpretability logic of all reasonable arithmetical theories
• The interpretability logic of Peano arithmetic
• The logic of \(\Pi_ 1\)-conservativity
• Kripke semantics for provability logic GLP
• Interpretability in PRA
• An effective fixed-point theorem in intuitionistic diagonalizable algebras. (The algebraization of the theories which express Theor. IX.)
• The interpretability logic of all reasonable arithmetical theories. The new conjecture
• The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)
• On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
• A Topological Study of the Closed Fragment of GLP
• Bimodal logics for extensions of arithmetical theories
• On n-quantifier induction
• A Finitary Treatment of the Closed Fragment of Japaridze's Provability Logic
• On the provability logic of bounded arithmetic
• A note on the normal form of closed formulas of interpretability logic
• 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 (8)

• Interpretability degrees of finitely axiomatized sequential theories
• Provability in finite subtheories of PA and relative interpretability: a modal investigation
• Theory and application of labelling techniques for interpretability logics
• Topological Interpretations of Provability Logic
• An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics
• Title not available (Why is that?)
• Interpretability suprema in Peano arithmetic
• The polytopologies of transfinite provability logic

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)