Interpretability in PRA (Q1035648)

The provability logic GL (Gödel-Löb) is a simple modal description of provability. Interpretability logic (IL) is an extension of provability logic suitable for a modal study of relative interpretability. Various extensions of IL are obtained by adding some new axioms. These new axioms are called the principles of interpretability. The system ILP results from the IL by adding the persistence principle \(A\triangleright B\rightarrow \square (A\triangleright B).\) \textit{A.~Visser} [in: Mathematical logic. Proc. Summer Sch. Conf. Ded. 90th Anniv. Arend Heyting, Chaika/Bulg. 1988, 175--209 (1990; Zbl 0793.03064)] gave the proof of arithmetical completeness of the system ILP w.r.t.\ finitely axiomatized theories. The system ILM results from the IL by adding Montagna's principle \(A\triangleright B\rightarrow (A\wedge \square C)\triangleright (B\wedge \square C)\). \textit{A.~Berarducci} [J.\ Symb.\ Log.\ 55, No.~3, 1059--1089 (1990; Zbl 0725.03037)] and V.~Shavrukov (1988) proved (independently) that ILM is complete for arithmetical interpretations in essentially reflexive theories. For no theory that is neither finitely axiomatizable nor essentially reflexive, the interpretability logic is known. Primitive recursive arithmetic (PRA) is one such theory. In [\textit{A.\ Visser}, CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020)] it is shown that the interpretability logic of PRA strictly extends IL. In the paper under review, two characteristic principles for PRA are studied. One such principle is Beklemishev's principle that exploits the fact that any theory which is an extension of PRA by \(\Sigma_2\)-sentences is reflexive. The authors give a characterization of Beklemishev's principle in terms of the modal semantics for interpretability logics. Zambella's principle is considered, too. It is shown that Zambella's principle does not add new information. So, the authors solved, in the paper under review, a number of problems concerning the interpretability logic of PRA, but many remain open.