Interpretability suprema in Peano arithmetic (Q2402961)

A theory $S$ interprets a theory $T$ if there is a translation of the language $T$ into the language of $S$ mapping theorems to theorems. If $T$ is a sufficiently strong theory one can consider the relation of relative interpretability: $T+\varphi$ interprets $T+\psi$ where $\varphi$ and $\psi$ are formulas. Mutual interpretability is an equivalence relation. Equivalence classes are called degrees of interpretability, and they are denoted by $[\varphi]$. \par The structure of the degrees of interpretabiltiy of r.e. theories extending PA is distributive lattice [\textit{V. Švejdar}, Commentat. Math. Univ. Carol. 19, 789--813 (1978; Zbl 0407.03020)]. The degree $[\varphi\vee \psi]$ is the infimum of $[\varphi]$ and $[\psi].$ The construction of the supremum of $[\varphi]$ and $[\psi]$ is somewhat more complicated. The provability logic is a simple modal description of the provability predicate. \par Interpretability logic is an extension of provability logic suitable for a modal study of relative interpretability [\textit{A. Visser}, CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020)]. \textit{A. Berarducci} [J. Symb. Log. 55, No. 3, 1059--1089 (1990; Zbl 0725.03037)] and \textit{V. Shavrukov} [The logic of relative interpretability over Peano arithmetic. Techn. Rep. No. 5. Moscow: Steklov Mathematical Institute (1988)] proved (independently) that the interpretability logic \textbf{IL}M is complete for arithmetical interpretations in essentially reflexive theories -- such as PA. \par The notion of the infimum of degrees of interpretability can be handled in \textbf{IL}M, but the supremum may not. In the paper under review, it is shown how the system \textbf{IL}M can be augmented with a new modality as a supremum operator. The authors explore different options for specifying the exact meaning of the new modality.