The interpretability logic of all reasonable arithmetical theories. The new conjecture (Q1840999): Difference between revisions

The provability logic is a simple modal description of the provability predicate. Interpretability logic is an extension of provability logic suitable for a modal study of relative interpretability [cf. \textit{A. Visser}, CSLI Lect. Notes 87, 307-359 (1998; Zbl 0915.03020)]. There are three great problems in provability and interpretability logic. The first one is the problem of the provability logics of Buss' \(S^1_2\) and Wilkie-Paris' \(I\Delta_0+ \Omega_1\) [cf. \textit{A. Berarducci} and \textit{R. Verbrugge}, Ann. Pure Appl. Logic 61, 75-93 (1993; Zbl 0803.03037)]. The second one is the problem of the provability logic of Heyting arithmetic. The third problem, the problem explained in the paper under review, is the problem of the interpretability logic of all reasonable arithmetical theories. The authors present both the arithmetical side and the modal side of the problem. The paper provides the necessary definitions and a detailed explanation of the latest conjecture. The interpretability logic of all reasonable arithmetical theory is denoted by \({\mathcal I}l(all)\). In the first time the interpretability logic \(ILW\) stood as the conjectured candidate for being \({\mathcal I}l(all)\). This conjecture was eventually refuted. \textit{A. Visser} [Stud. Log. 50, 81-105 (1991; Zbl 0744.03023)] conjectured that the system \(ILW M_0\), or \(ILW^*\), was \({\mathcal I}l(all)\). Recently, A. Visser found a new principle \(P_0: A\triangleright\diamondsuit B\to\square (A\triangleright B)\). The authors pose the new conjecture: \(ILW^*P_0= {\mathcal I}l(all)\).