Provability and Interpretability Logics with Restricted Realizations

Notre Dame Journal of Formal Logic 53 (2):133-154 (2012)
  Copy   BIBTEX


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. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, 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$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM



    Upload a copy of this work     Papers currently archived: 92,369

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Bimodal logics for extensions of arithmetical theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.
Interpretability over peano arithmetic.Claes Strannegård - 1999 - Journal of Symbolic Logic 64 (4):1407-1425.
The interpretability logic of peano arithmetic.Alessandro Berarducci - 1990 - Journal of Symbolic Logic 55 (3):1059-1089.
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.


Added to PP

63 (#258,380)

6 months
22 (#125,216)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Thomas Icard
Stanford University
Joost Joosten
Universitat de Barcelona

References found in this work

Solution of a problem of Leon Henkin.M. H. Löb - 1955 - Journal of Symbolic Logic 20 (2):115-118.
The interpretability logic of peano arithmetic.Alessandro Berarducci - 1990 - Journal of Symbolic Logic 55 (3):1059-1089.
On n-quantifier induction.Charles Parsons - 1972 - Journal of Symbolic Logic 37 (3):466-482.

View all 24 references / Add more references