Provability and interpretability logics with restricted realizations

TL;DR

This paper explores provability and interpretability logics with restricted arithmetical realizations, revealing that for many theories the resulting logic aligns with linear frames, and provides bounds for interpretability logic of PRA.

Contribution

It introduces a modified notion of provability and interpretability logics with restrictions, and characterizes their structures for various theories, especially PRA, advancing understanding of interpretability logic.

Findings

For many theories, the provability logic with restrictions is the logic of linear frames.

A new fragment of PRA yields a more interesting provability logic.

Upper bounds for IL(PRA) are established, including IL(PRA) ⊆ ILM.

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$\Sigma_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.