Introduction

A miracle happens. This is the openings phrase of an article by Albert Visser [Vis97] and hereby of this paper as well. The miracle mentioned emerges in metamathematical considerations of interpretations. Interpretations are interesting mathematical objects on their own. They frequently turn up in various areas. As a classical example one can mention the use of interpretations in establishing the undecidability of certain theories as exposed in [TMR53] Tarski, Mostowski, Robinson. The notion is frequently encountered in relative consistency results as well. Interpretations are also a very natural device when comparing different structures. Rather then paying importance to the names of the individual objects one would merely like to be able to talk about alikeness and imbeddability or better: interpretability. It turns out that the notion of interpretability can be formalized within the language of sufficiently strong mathematical theories. The methods used here are the same as when it came to formalizing the provability predicate. Actually, one makes explicit use of the formalized provability predicate to formalize interpretability and indeed both topics are closely related. Proceeding along like this yields a logic of interpretability with a Kripke-like semantics. As complex as is the notion of interpretability, as simple a method can be distilled representing this originally very complex notion. Solovay's method establishing arithmetical completeness of provability logic can be generalized to obtain arithmetically complete systems of interpretability logic and behold: decidability! Yes miracles do exist.

The logic of interpretability can thus be viewed as an extension to the logic of provability. The logic of provability includes important results concerning formal provability and provides a very sophisticated way of representing important results of, for example, Gödel, [Göd92], and Löb, [Löb55]. The subject of study in provability logic as with interpretability logic is formal theories. Provability is quite a stable notion though and does not distinguish between even very different theories. From quite weak theories onwards, all the provability logics come out the same. It is known that all theories in which $I\Delta_0 + \mathrm{EXP}$ is interpretable and which are $\Sigma_1$-sound under the translation, have the same provability logic: Löb's logic. See for example [Vis97], or [Vis84]. One could think of three approaches if one wants to obtain different logics, for fine tuning so to say.
First one could try to descend to theories weaker than $I\Delta_0 + \mathrm{EXP}$, where Löbs logic is still arithmetically valid. This becomes an extremely difficult venture and despite intensive investigations very little is known on this subject. See e.g. [BV93]. Another direction would be to alter the bare logic. One could switch to, for example, intuitionistic logic in its relation to Heyting arithmetic obtaining a variety of new valid principles. Significant progress is made, [Iem98], [Vis94], but for example it is still unknown whether the provability logic of Heyting Arithmetic is axiomatizable at all. A third possibility would be to enrich the modal language. Where the logic of provability employs only one modal operator $\Box$, for formal provability, the language of interpretability logic includes also a binary modality $\rhd$ for interpretability. Although $\Box$can be defined in terms of $\rhd$, one prefers to use both modalities. The whole provability logic now becomes a sublogic of the logic of interpretability. Moreover, distinctions between different theories are reflected by having different corresponding interpretability logics. So, interpretability is not that stable a notion as provability is. Furthermore, all sorts of arithmetical results can now be expressed, as we will see later, very elegantly like for example the model existence lemma, $\Diamond A \rhd A$, or a more intricate formalization of the second incompleteness theorem of Gödel, $\Diamond A \rightarrow \neg ( A \rhd \Diamond A)$.

For two main interpretability logics, arithmetical completeness results are known. On the one hand that is the interpretability logic of $\mathit{PA}$, $\mathit{ILM}$, and on the other hand the interpretability logic of any (sufficiently strong) finitely axiomatizable theory, $\mathit{ILP}$. As these two logics are different, it seems very natural to ask for the core logic, that is the interpretability logic of all reasonable arithmetical theories. ``Reasonable'' in this context is not such a tight notion and can be read here as ``containing $I\Delta_0 + \mathrm{SUPEXP}$''. Looking for this notion is not just a matter of a simple intersection of all logics; Stronger logics can prove more but also have more expressive power. The primary aim of this paper is to contribute to the quest for the interpretability logic of all reasonable arithmetical theories. In due time many seemingly relevant interpretability logics have seen the light and many of them faded away already. The situation at the start of this research is sketched below.

$\mathit{IL}$, $\mathit{ILP}$ and $\mathit{ILM}$ are known to be decidable and modally complete. $\mathit{ILM}$ and $\mathit{ILP}$ are also arithmetically complete with regard to some theories. See e.g. [JdJ98]. In an article soon to appear, [dJV], $\mathit{ILW}$ is shown to be decidable and modally complete. In [Vis90] $\mathit{ILW}$ was put forward as the interpretability logic of all reasonable arithmetical theories. After the discovery that M₀ is a valid principle in [Vis91], the conjecture was updated to $\mathit{ILW}^*(={\mathit ILWM_0})$.

By the end of this paper we obtain a new picture which is given below. We develop a strategy for obtaining modal completeness without necessarily also obtaining decidability. This method is applied to $\mathit{ILM}$ to get both completeness and decidability. The same method shows to be fruitful when it is applied to $\mathit{ILM_0}$; we obtain the modal completeness of $\mathit{ILM_0}$. $\mathit{ILW}^*$ is shown to be inadequate as a candidate for $\mathit{GIL}$, the logic of all reasonable arithmetical theories. This is done by introducing a new arithmetically valid principle P₀, which is not derivable over $\mathit{ILW}^*$.