1 Introduction
1.1 Background
Interpretations arise in several (meta)mathematics areas, and many variations exist.Footnote
1
For instance, it is possible to interpret propositional intuitionistic logic into classical Gödel–Löb logic GL by establishing an equivalence between the axiomatisation
$\mathbb {GL}$
and the axiomatic calculus
$\mathbb {IPC}$
; from that, one could also interpret
$\mathbb {IPC}$
into an arithmetical theory
$\mathsf {T}$
that is adequate to
$\mathbb {GL}$
.
An even simpler example is given by Gödel’s numbering, which, according to Tarski [Reference Tarski and Corcoran47], interprets (a model for) meta-mathematical reasoning into the standard model for arithmetic by defining an injective function that maps finite strings of arithmetical symbols into
$\mathbb {N}$
, and a further function mapping each meta-predicate into its arithmetical counterpart.
In the present work, we will assume a very general version of that concept: An interpretation of a theory
$\mathsf {T}$
into a theory
$\mathsf {T}'$
is just a structure-preserving translation t such that if
$\mathsf {T}\vdash A$
then
$\mathsf {T}'\vdash t(A)$
. More precisely, we will consider interpretability between arithmetical theories of the form
$\mathsf {T}+A$
, where
$\mathsf {T}$
is some base theory satisfying the standard Hilbert–Bernays–Löb provability conditions as discussed in e.g., [Reference Boolos5, Reference Smorynski42, Reference Smorynski43], and A is a schema in the language of
$\mathsf {T}$
.Footnote
2
Modal logics for interpretability arise as an extension of the language of provability logic through a binary modal operator
$\rhd $
capturing the relation of (relative) interpretability between two arithmetical theories.
Recall first that, in provability logic, we denote by
$\ast $
a standard arithmetical realisation of the modal language, as described in e.g., [Reference Verbrugge and Zalta51]: In particular,
$\ast $
commutes with the classical operators and maps
$\Box A$
into
$\textit {Bew}(\ulcorner A^{\ast }\urcorner )$
, where
$\textit {Bew}(x)$
is the standard provability predicate for the given arithmetical theory
$\mathsf {T}$
.
In interpretability logics, the propositional formula
$A\rhd B$
is then intended as the modal counterpart of the arithmetical formula
$\textit {Int}_{\textsf {T}}(\ulcorner A^{\ast }\urcorner ,\ulcorner B^{\ast }\urcorner )$
—where
$\textit {Int}_{\mathsf {T}}(x,y)$
is the formal predicate in the language of
$\mathsf {T}$
for relative interpretability over
$\mathsf {T}$
itself—expressing the fact that the arithmetical theory
$\mathsf {T}$
extended by
$A^{\ast }$
interprets the arithmetical theory
$\mathsf {T}$
extended by
$B^{\ast }$
.
The origins of interpretability logics date back to [Reference Visser54], which axiomatised the basic modal framework by extending the language of
$\mathbb {GL}$
with some minimal axioms for the core logic for interpretability
$\mathbb {IL}$
, on top of which several systems can be constructed.
Completeness results w.r.t. a Kripke-style relational semantics, based on so-called Veltman frames, were presented first in [Reference de Jongh and Veltman7] for
$\mathbb {IL}$
and some extensions by using a canonical model construction. More complex proofs were developed by the same authors in 1999, and further techniques were introduced to achieve subsequent completeness results since the beginning of the 2000s starting with [Reference Goris and Joosten12]. Recent results have been obtained also for subsystems of
$\mathbb {IL}$
in [Reference Iwata, Kurahashi and Okawa16, Reference Kurahashi and Okawa19, Reference Okawa34].
On the arithmetical side, by tweaking the proof strategy in [Reference Solovay45] for
$\mathbb {GL}$
, it is possible to prove also the arithmetical completeness of some extensions of
$\mathbb {IL}$
. The interpretability logic for
$\mathsf {T}$
is, as expected,
$$ \begin{align*}\mathsf{IL}(\mathsf{T}):=\{ A \,|\,\,\textrm{for any realisation}\,\ast, \mathsf{T}\vdash A^{\ast}\}.\end{align*} $$
In [Reference Shavrukov41], it is proven that this notion is
$\Sigma ^{0}_{3}$
-complete. It is also known, that
$\mathbb {IL}$
is not the interpretability logic for any arithmetical theory
$\mathsf {T}$
. However, if we assume that
$\mathsf {T}$
is
$\Sigma _{1}$
-sound and proves full induction, by adding the schema
$$ \begin{align*} \mathsf{M}:= A\rhd B\rightarrow A\wedge\Box C\rhd B\wedge\Box C, \end{align*} $$
weFootnote 3 have that
$$ \begin{align*} \mathsf{IL}(\mathsf{T})=\mathbb{ILM}:=\mathbb{IL}+\mathsf{M}. \end{align*} $$
Similarly if we add to
$\mathbb {IL}$
the schema
$$ \begin{align*} \mathsf{P}:=A\rhd B\rightarrow\Box(A\rhd B), \end{align*} $$
then
$$ \begin{align*} \mathbb{IL}+\mathsf{P}=:\mathbb{ILP}=\mathsf{IL}(\mathsf{T}) \end{align*} $$
for any
$\mathsf {T}$
that is
$\Sigma _{1}$
-sound, finitely axiomatised, and such that it proves the totality of
$\mathtt {supexp}$
.Footnote
4
The most intriguing aspect of interpretability logics is this sensitivity to the base arithmetical theory. The main open question in the field is indeed establishing the interpretability logic of all reasonable arithmetical theories, i.e.,Footnote 5
$$ \begin{align*}\mathsf{IL}(\textit{All}):=\{A\, |\,\forall \mathsf{T}\supseteq\mathsf{I}\Delta_{0}+\mathsf{exp},\,\textrm{for any realisation}\,\ast, \mathsf{T}\vdash A^{\ast}\}.\end{align*} $$
What we know, after [Reference Visser55], is that
$\mathbb {IL}\subset \mathsf {IL}(\textit {All})\subset \mathbb {ILM}\cap \mathbb {ILP}$
, but a modal characterisation of
$\mathsf {IL}(\textit {All})$
is still unknown.
1.2 This article
There are many further open questions in the field of interpretability logics. In our setting, it is worth noticing that very little is known about the structural proof theory for interpretability logics: Sasaki [Reference Sasaki39] gives a Gentzen-style sequent calculus for
$\mathbb {IL}$
only, while Hakoniemi and Joosten [Reference Hakoniemi and Joosten15] presents a labelled tableaux system for some extensions of
$\mathbb {IL}$
based on standard Veltman semantics.Footnote
6
In the present paper, we extend the proof-theoretic analysis of interpretability logics by introducing a family
$\mathsf {G3IL}^{\star }$
of labelled sequent calculi which cover a wide range of modal systems for interpretability naturally. Their design is based on the methodology of Negri [Reference Negri28, Reference Negri31] but, instead of working with formal relational semantics or formal neighbourhood semantics, these original calculi internalise the hybrid models by Rineke Verbrugge, also called generalised Veltman structures in [Reference Verbrugge50].
One of the main advantages of reasoning on interpretability logics by using Verbrugge semantics instead of standard Veltman semantics is that the former subsumes the latter, but it is also capable of distinguishing interpretability principles that are equivalent in a model theory based on Veltman frames. Moreover, some interpretability logics can be characterised in terms of semantic properties that are more simple when dealing with Verbrugge frames than in the standard relational setting. Furthermore, some modal logics for interpretability are known to be incomplete w.r.t. Veltman semantics, while being complete w.r.t. Verbrugge semantics.
At the same time, the results collected by Joosten et al. [Reference Joosten, Rovira, Mikec, Vuković, Bezhanishvili, Iemhoff and Yang17] after sever years of active research show that the interactions between Veltman and Verbrugge semantics are subtle: When it comes to models, the two semantics are equally powerful, but when reasoning on frames, the situation is quite different, and variations on the definition of Verbrugge frames lead to different results.
The main contribution of the work presented here consists of designing modular sequent systems satisfying the main structural desiderata, namely, admissibility of contraction and weakening, invertibility of logical rules, and a cut-elimination algorithm.
More precisely, we build on Verbrugge semantics to define labelled sequent calculi for IL and the most relevant of its extensions, including ILM, ILP, and, more interestingly, ILW, which was not covered before in proof-theoretic literature. These calculi utilise world and neighbourhood labels to incorporate relevant semantic features into the syntax. At the same time, each proof system adheres to standard proof-theoretic principles, ensuring that each connective is addressed by dual left and right rules, supporting a clear syntactic explanation of its meaning. With the intent to stick to principled design philosophy, we also defined a non-normal operator
$\langle ]_{x}$
for neighbourhoods indexed on world labels, introduced for translating naturally the meaning of the
$\rhd $
modality into sequent rules. Moreover, we adapted the methodology used by Negri [Reference Negri28] for dealing with Noetherianity of GL-frames, with the intent of capturing within our proof systems the same notion, modulo the necessary generalisation to consider Verbrugge frames for interpretability logics. In short, as Verbrugge semantics is not per se expressible as a geometric theory—i.e., cannot be reduced to a finite set of axiom schemas in the language of first-order logic of shape
$A\rightarrow B$
, where A and B do not contain
$\forall $
and
$\rightarrow $
—defining sequent rules based on the geometric rule schemas by Negri and von Plato [Reference Negri and von Plato33] was a not-so-easy task, and required a careful approach to the design of the calculi, in order to obtain precise structural properties of the systems for these logics.
By adopting such a principled set of design choices, our calculi markedly exhibit a modular nature, where logical rules remain consistent across all systems. In contrast, relational rules for neighbourhood and world labels are introduced to define specific calculi for each considered extension.
In addition to their simplicity and modularity, the calculi boast robust structural properties. These include the invertibility of all rules and the admissibility of contraction and cut, proven in a once-for-all way for the base system and its extensions. From the technical viewpoint, we remark that the definition of the cut-elimination algorithm required the use of a ternary measure of the cut complexity, which is borrowed from the proof of cut admissibility for
$\mathsf {G3GL}$
in [Reference Negri28], modulo some tweaks to deal with the more general setting of Verbrugge semantics.
As of the current literature, the comprehensive proof-theoretic analyses of interpretability logics presented here are unparalleled in scope. The only relevant limitation of the current version of our sequent calculi is that it can be interpreted as a framework “for Veltman frames in disguise” because of the correspondence established by Verbrugge [Reference Verbrugge50] between Veltman models and the version of Verbrugge models we adopted.Footnote 7 Still, our findings collected here suggest a promising avenue for the canonical extension of the results presented in the following pages to cover other variants of Verbrugge semantics and more intricate logical frameworks dealing with modal logic for meta-mathematics.
1.3 Paper structure
The paper is organised as follows: In §2, we recall the axiomatic calculi for the main interpretability logics under investigations; in §3, the basic definitions and results in the model theory for interpretability logics are recalled, and the Verbrugge semantics (a.k.a. Generalised Veltman Semantics) (GVS) is discussed according to the most recent literature on the topic. Our family of sequent calculi
$\mathsf {G3IL}^{\star }$
is then presented in §4; §5 is committed to the structural analysis of those calculi, and includes a constructive proof of admissibility of the cut rule for all the extensions. Finally, in §6, we prove the soundness and completeness of our systems w.r.t. the semantic and axiomatic presentations, respectively. A section discussing related and future work closes the article.
2 Axiomatic calculi
Let us start by recalling the formal definitions of a propositional modal language for interpretability logics.
Definition 2.1. The set of formulas in a standard formal language
$\mathcal {L}_{\Box ,\rhd }$
for interpretability logics is given by the following grammar:
$$ \begin{align*}p\;\, |\;\, A\wedge B\,\, |\;\, A \vee B\;\, |\;\, A\rightarrow B\;\, |\;\, \bot\;\,|\;\, \Box A\;\, |\;\, A\rhd B,\,\end{align*} $$
where p belongs to a denumerable set
$\texttt {Atm}$
of atomic propositions. Truth, negation and coimplication are defined in the standard way:
$\top :=\bot \rightarrow \bot $
,
$\neg A := A\rightarrow \bot $
, and
$A\leftrightarrow B:= (A\rightarrow B)\wedge (B\rightarrow A)$
, respectively. When reasoning in a classical setting, we can also consider a further modal operator
$\Diamond $
, which we define as
$\Diamond A:=\neg \Box \neg A$
.
The basic axiomatic calculus for interpretability logics is given by the following definition.
Definition 2.2. Let
$\mathbb {IL}$
denote the axiomatic system determined by
-
• the axiom schemas of any classical propositional calculus
$\mathbb {CPC}$
; -
• schema
$\mathsf {K}$
:
$\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$
; -
• schema
$\mathsf {GL}$
:
$\Box (\Box A \rightarrow A)\rightarrow \Box A$
; -
• interpretability schemasFootnote 8
-
–
$\mathsf {IL1}$
:
$\Box (A\rightarrow B)\rightarrow A\rhd B$
; -
–
$\mathsf {IL2}$
:
$A\rhd B \rightarrow (B\rhd C\rightarrow A\rhd C)$
-
–
$\mathsf {IL3}$
:
$A\rhd C\rightarrow (B\rhd C\rightarrow A\vee B\rhd C)$
-
–
$\mathsf {IL4}$
:
$A\rhd B\rightarrow (\Diamond A\rightarrow \Diamond B)$
-
–
$\mathsf {IL5}$
:
$\Diamond A\rhd A$
-
-
• MP (Modus Ponens) rule
-
• Necessitation rule
As usual, we write
$\Gamma \vdash _{\mathbb {IL}} A$
when A is derivable in
$\mathbb {IL}$
assuming the set of hypotheses
$\Gamma $
, with the proviso that the rule of necessitation is applied only to theorems, otherwise the rule is not sound and the deduction theorem fails, as discussed by [Reference Hakli and Negri14]. We write
$\mathbb {IL}\vdash A$
when
$\Gamma =\varnothing $
.
For this calculus, some interesting lemmas are provable.
Lemma 2.3. The following hold
-
(i)
$\mathbb {IL}\vdash \Box \neg A\rightarrow (A\rhd B)$
; -
(ii)
$\mathbb {IL}\vdash A\vee \Diamond A\rhd A$
; -
(iii)
; -
(iv)
, and are inter derivable over
$\mathbb {IL}$
; -
(v)
and
$\Box \neg A$
are inter derivable over
$\mathbb {IL}$
; -
(vi)
.
;
, 
and 
are inter derivable over 
and 
.Proof. Refer to e.g., [Reference Visser54].
Item (v) of the previous lemma shows that we could dismiss the
$\Box $
modality since we could define
$\Box A$
as 
. This definition would simplify our base language. However, we will see in §3.1, §3.2, and, more poignantly, §4.1, that it is possible to define
$\Box $
via
$\rhd $
as well as
$\rhd $
via
$\Box $
by semantics considerations. Those will lead to the design of our family of sequent calculi in §4.Footnote
9
2.1 Axiomatic extensions
On top of
$\mathbb {IL}$
, it is possible to add further modal principles that have specific relevance for arithmetical realisations. Here, we will consider the following calculi.
Definition 2.4. Let us define as proper extensions of
$\mathbb {IL}$
-
•
$\mathbb {ILM}:=\mathbb {IL}+\mathsf {M}$
, where is called the Montagna schema;
$$ \begin{align*}\mathsf{M}:= A\rhd B\rightarrow A\wedge\Box C\rhd B\wedge\Box C\end{align*} $$
-
•
$\mathbb {ILP}:=\mathbb {IL}+\mathsf {P}$
, where is called the persistence schema;
$$ \begin{align*}\mathsf{P}:=A\rhd B\rightarrow\Box(A\rhd B)\end{align*} $$
-
•
$\mathbb {ILW}:=\mathbb {IL}+\mathsf {W}$
, where
$$ \begin{align*}\mathsf{W}:=A\rhd B\rightarrow A\rhd B\wedge\Box\neg A;\end{align*} $$
-
•
$\mathbb {ILKM}1:=\mathbb {IL}+\mathsf {KM1}$
, where
$$ \begin{align*}\mathsf{KM1}:=A\rhd\Diamond B\rightarrow\Box(A\rightarrow\Diamond B);\end{align*} $$
-
•
$\mathbb {ILM}_{0}:=\mathbb {IL}+\mathsf {M}_{0}$
, where
$$ \begin{align*}\mathsf{M}_{0}:=A\rhd B\rightarrow\Diamond A\wedge\Box C\rhd B\wedge\Box C.\end{align*} $$
3 Semantics for interpretability logics
As stated in the introduction, we know—after [Reference Berarducci2, Reference Shavrukov40], and [Reference Visser54, Reference Zambella57], respectively—that
$\mathbb {ILM}$
is the interpretability logic for arithmetical theories proving full induction, and
$\mathbb {ILP}$
captures the properties of formal interpretability over finitely axiomatised theories proving the totality of the superexponential function.Footnote
10
Their proofs are based on Solovay’s strategy for arithmetical completeness of Gödel–Löb logic as exposed in [Reference Boolos5, Reference Smorynski43]; therefore, they effectively use the characterisation of those axiomatic systems in terms of relational models. We now turn our presentation to these semantic aspects of interpretability logics.
3.1 Veltman semantics
To obtain a standard relational semantics for interpretability logics from possible world semantics one usually proceeds by “decorating” frames with additional indexed accessibility relations.
Definition 3.1. A Veltman frame
$\mathcal {F}$
consists of:
-
• a nonempty set W of possible worlds;
-
• a binary relation R on W which is transitive and NoetherianFootnote 11 ;
-
• a collection
$\{S_{x} \,|\, x\in W\}$
of binary relations which are reflexive, transitive and such that-
– if
$yS_x z$
, then
$y\in R[x]$
and
$z\in R[x]$
, where
$R[x]:=\{y\in W\,|\, xRy\}$
; and -
– if
$xRyRz$
, then
$yS_{x}z$
.
-
A Veltman model
$\mathcal {M}$
is obtained by adding an evaluation function
$v: \texttt {Atm}\times W \rightarrow \{0,1\}$
to a given Veltman frame, as usual. A forcing relation
$\Vdash $
is then obtained by a standard definition for propositional connectives and
$\Box $
-modality
$$ \begin{align*} x\Vdash_{\mathcal{M}}\Box B\qquad\textrm{iff}\qquad\textrm{for all}\; y\in W, \textrm{if}\,xRy\, \textrm{then}\, y\Vdash_{\mathcal{M}}B \end{align*} $$
while for
$\rhd $
-modality we stipulate that
$$ \begin{align*} \begin{array}{l l l} x\Vdash_{\mathcal{M}} A\rhd B & \text{iff} & \text{for all } y\in W, \text{ if } xRy \text{ and } y\Vdash_{\mathcal{M}} A, \text{then} \\ & & \text{there exists a } z\in W \text{ such that } yS_{x}z \text{ and } z \Vdash_{\mathcal{M}} B. \end{array} \end{align*} $$
We write
$\vDash _{\mathcal {M}}A$
when A is forced by any world in
$\mathcal {M}$
; similarly, we write
$\vDash _{\mathcal {F}}A$
when
$\vDash _{\mathcal {M}}A$
for any model
$\mathcal {M}$
based on
$\mathcal {F}$
.
For extensions, some frame conditions are needed. A frame condition for a modal schema A is a (first or higher order) formula
$(A)$
in the language
$\{W,R,\{S_{x}\}\}$
such that the structure
$\mathcal {F}$
satisfies the property
$(A)$
if and only if
$\vDash _{\mathcal {F}}A$
.
In [Reference Visser53, Reference Visser54], many principles for interpretability were proposed first, together with their semantic characterisations. We then know that
$$ \begin{align*} (\mathsf{W})=(\mathsf{KW1})=(\mathsf{F})=\textrm{"}R\circ S_{x}\,\textrm{is Noetherian" for all}\,x\in W, \end{align*} $$
where
$$ \begin{align*} \begin{array}{l l l} \mathsf{KW1} & := & A\rhd\Diamond\top\rightarrow\top\rhd\neg A \\ \mathsf{F} & := & A\rhd\Diamond A\rightarrow\Box\neg A. \end{array} \end{align*} $$
Moreover we have that
$$ \begin{align*} (\mathsf{M})=(\mathsf{KM1})=(\mathsf{KM2})=\,\textrm{if}\,\, yS_{x}zRu,\,\,\textrm{then}\,\, yRu, \end{align*} $$
where
$$ \begin{align*} \begin{array}{l l l} \mathsf{KM2} & := & A\rhd B\rightarrow(\Box(B\rightarrow\Diamond C)\rightarrow\Box(A\rightarrow\Diamond C)), \end{array} \end{align*} $$
and we know, after Visser [Reference Visser53], that
$\mathsf {KM1}$
and
$\mathsf {KM2}$
are interderivable over
$\mathbb {IL}$
.
By using Veltman semantics, Švejdar [Reference Švejdar46] proved that
$$ \begin{align*}\mathbb{IL}\{\mathsf{F},\mathsf{KW1}\}\not\vdash\mathsf{KW1}^{\circ},\end{align*} $$
where
$$ \begin{align*}\mathsf{KW1}^{\circ} := A\wedge B\rhd\Diamond A\rightarrow A\rhd(A\wedge\neg B).\end{align*} $$
After the work on those systems by Švejdar [Reference Švejdar46], we furthermore know that
$\mathbb {ILF}$
,
$\mathbb {ILKW}1$
,
$\mathbb {ILKW}1^{\circ }$
are incomplete w.r.t. the standard relational semantics.
3.2 Verbrugge semantics
Verbrugge semantics (also called GVS) rescues the situation. Rineke Verbrugge has developed it in [Reference Verbrugge50] by considering interpretations reminiscent of neighbourhood semantics for non-classical logics.
To be more precise, each
$S_{x}$
is now a relation between worlds and sets of worlds, satisfying specific properties identified by the schemas for
$\rhd $
.
Definition 3.2. A Verbrugge frame
$\mathcal {F}$
consists of
-
• a finite set
$W\not =\varnothing $
; -
• a binary relation
$R\subseteq W\times W$
which is irreflexive and transitive; -
• a W-indexed set of relations
$S_{x}\subseteq R[x]\times (\wp (R[x])\smallsetminus \{\varnothing \})$
;
satisfying the following conditions:
-
• Quasi-reflexivity: if
$xRy$
then
$yS_{x}\{y\}$
; -
• Definiteness: if
$xRyRz$
then
$yS_{x}\{z\}$
; -
• Monotonicity: if
$yS_{x}a$
and
$a\subseteq b\subseteq R[x]$
then
$yS_{x}b$
; -
• Quasi-transitivity: if
$yS_{x}a$
and
$vS_{x}b_{v}$
for all
$v\in a$
, then
$yS_{x}(\bigcup _{v\in a}b_{v})$
.
Remark 1. The frames used in Verbrugge semantics are, in a sense, relational frames for Gödel–Löb logic enriched with indexed relations between worlds and nonempty sets of worlds.Footnote 12 Those frames for Gödel–Löb logic are conventionally those that are endowed with an accessibility relation that is transitive and Noetherian. However, we know that a semantics based on irreflexive, transitive and finite frames (ITF) is also adequate for Gödel–Löb logic. Therefore, we adopt here this second semantic characterization of the system for provability, noting that this has no impact on the “neighbourhood aspects” of Verbrugge semantics for the logics we investigate here, since they all satisfy the finite model property for GVS—and the same could have been done for standard Veltman semantics.Footnote 13
A Verbrugge model is obtained by considering a usual evaluation function, which can be extended to a forcing relation defined as for standard semantics, with only one difference:
where 
abbreviates the expression “for any
$z\in a, z\Vdash B$
”.
As for relational semantics, extensions for
$\mathbb {IL}$
need generalised frame conditions: We denote by
$(A)_{\textit {gen}}$
the frame condition w.r.t. Verbrugge semantics corresponding to the modal schema A.
We know that the following holdFootnote 14
$$ \begin{align*}\begin{array}{l@{\kern4pt}l@{\kern4pt}l} (\mathsf{M})_{\textit{gen}} & = & yS_{x}a\Rightarrow\exists b\subseteq a, yS_{x}b\,\&\,R[b]\subseteq R[y] \\(\mathsf{KM1})_{\textit{gen}} & = & yS_{x}a\Rightarrow\exists i\in a,\forall z(iRz\Rightarrow yRz) \\(\mathsf{P})_{\textit{gen}} & = & xRx'RyS_{x}a\Rightarrow\exists b\subseteq a, yS_{x'}b \\(\mathsf{M}_{0})_{\textit{gen}} & = & wRuRxS_{w}a\Rightarrow\exists b\subseteq a, uS_{w}b\,\&\,R[b]\subseteq R[u] \\(\mathsf{P}_{0})_{\textit{gen}} & = & wRxRuS_{w}a\,\&\forall v\in a(R[v]\cap b\neq\varnothing)\Rightarrow\exists c\subseteq b, uS_{x}c \\(\mathsf{W})_{\textit{gen}} & = & yS_{x}a\Rightarrow\exists b\subseteq a, yS_{x}b\,\&\,R[b]\cap S_{x}^{-1}b =\varnothing \\(\mathsf{R})_{\textit{gen}} & = & wRxRuS_{w}a\Rightarrow\forall c\in\mathcal{C}(x,u),\exists b\subseteq a, xS_{W}b\,\&\,R[b]\subseteq c \\(\mathsf{W}^{\ast})_{\textit{gen}} & = & (\mathsf{M}_{0})_{\textit{gen}}\;\&\;(\mathsf{W})_{\textit{gen}}, \end{array}\end{align*} $$
where
-
•
$i\in R[b]$
iff there is an
$x\in b$
such that
$xRi$
; -
•
$i\in S_{x}^{-1}b$
iff
$iS_{x}b$
; -
•
$\mathcal {C}(x,u) := \{c\subseteq R[x] \,|\, \forall d, uS_{x}d\Rightarrow d\cap c\neq \varnothing \}$
; -
•
$\mathsf {P}_{0} := A\rhd \Diamond B\rightarrow \Box (A\rhd B)$
; -
•
$\mathsf {R} := A\rhd B\rightarrow \neg (A\rhd \neg C)\rhd B\wedge \Box C)$
; -
•
$\mathsf {W}^{\ast } := A\rhd B\rightarrow B\wedge \Box C\rhd B\wedge \Box C\wedge \Box \neg A$
.
For the basic system
$\mathbb {IL}$
, completeness results are known w.r.t. both standard Veltman semantics and GVS. Moreover, the techniques used to prove the completeness theorem for that system w.r.t. GVS can be easily extended to consider analogous results for
$\mathbb {ILM},\mathbb {ILP},$
and
$\mathbb {ILW}$
proven by de Jongh and Veltman [Reference de Jongh and Veltman7, Reference de Jongh and Veltman8] w.r.t. ordinary Veltman semantics.
However, for the other extensions, the proof of modal completeness can be quite convoluted and very sensitive to the logic under consideration, so proving that an extension of a given system is complete may need a very different proof strategy w.r.t. the one used for the completeness of the original subsystem. Some promising advances have been made recently by Joost Joosten and collaborators in a series of works aiming at developing a modular and uniform methodology to deal with GVS for interpretability logics: The most recent literature on the topic includes Mikec and Vukovic [Reference Mikec and Vuković27], who leverage techniques from Bilkova et al. [Reference Bilkova, Goris and Joosten3] and Goris et al. [Reference Goris, Bílková, Joosten and Mikec11], subsequently surveyed by Joosten et al. [Reference Joosten, Rovira, Mikec, Vuković, Bezhanishvili, Iemhoff and Yang17] and Rovira et al. [Reference Rovira, Mikec and Joosten38].Footnote 15
In any case, investigations on GVS suffice to establish that, for the interpretability logics, we have mentioned the interdependencies rendered in Figure 1 hold.
Interdependencies among interpretability logics, after Vuković [Reference Vuković56]. An arrow from
$\mathsf {S}$
to
$\mathsf {S}'$
is interpreted as
$\mathbb {IL}+\mathsf {S}'\subsetneq \mathbb {IL}+\mathsf {S}.$
Finally, we can summarise the current model-theoretic knowledge on interpretability logic by the glossary in Figure 2
This information is collected from the results in [Reference Verbrugge50], [Reference de Jongh and Veltman7, Reference de Jongh and Veltman8], [Reference Goris and Joosten12], [Reference Mikec, Perkov and Vuković26, Reference Mikec and Vuković27], [Reference Perkov and Vuković37]. Here FMP abbreviates “finite model property”.
4 Design of the labelled sequent calculi
We have seen that the language 
is somehow redundant: After Lemma 2.3(v), we know that
$\Box A$
is equivalent to
$\neg A\rhd \bot $
. This equivalence invites to minimise the formal language for interpretability by considering the
$\rhd $
-modality as primitive. The resulting language will be denoted by
$\mathcal {L}_{\rhd }$
.
We need now to rephrase the inductive definition of well-formed formulas of
$\mathbb {IL}$
—and its extensions—as follows.
Definition 4.1. The set of well-formed formulas of
$\mathbb {IL}$
and its extensions w.r.t.
$\mathcal {L}_{\rhd }$
is given by the following grammar
$$ \begin{align*}\mathtt{Form}_{\rhd} ::=\,\, p\;\, |\;\, A\wedge B\,\, |\;\, A \vee B\;\, |\;\, A\rightarrow B\;\, |\;\, \bot\;\,|\;\, A\rhd B\;\,,\end{align*} $$
where
$p\in \mathtt {Atm}$
and
$A,B\in \mathtt {Form}_{\rhd }$
.
As the reader might expect, we define
$\neg A\hspace{-0.5pt}:=\hspace{-0.5pt} A\hspace{-0.5pt}\rightarrow\hspace{-0.5pt} \bot $
,
$A\hspace{-0.5pt}\leftrightarrow\hspace{-0.5pt} B\hspace{-0.5pt}:=\hspace{-0.5pt}(A\hspace{-0.5pt}\rightarrow\hspace{-0.5pt} B)\hspace{-0.5pt}\wedge\hspace{-0.5pt} (B\hspace{-0.5pt}\rightarrow\hspace{-0.5pt} A)$
,
$\Box A:=\neg A\rhd \bot $
, and
$\Diamond A := \neg \Box \neg A$
.
On the axiomatic side, such a minimalist choice about the basic modal language (only
$\rhd $
is used as modal operator) is reflected by a minimalist axiomatisation of the basic modal system for interpretability.
Definition 4.2. Let
$\mathbb {IL}_{\rhd }$
denote the axiomatic calculus defined in [Reference Visser55] byFootnote
16
-
• Axiom schemas of
$\mathbb {CPC}$
; -
• schema
$\mathsf {IL2}$
:
$A\rhd B \rightarrow (B\rhd C\rightarrow A\rhd C)$
; -
• schema
$\mathsf {IL3}$
:
$A\rhd C\rightarrow (B\rhd C\rightarrow A\vee B\rhd C)$
; -
• schema
$\mathsf {IL\textsf {-Löb}}$
:
$A\rhd (A\wedge (A\rhd \bot ))$
; -
• MP Rule
; -
•
$\rhd $
Rule .
;
.The extensions of
$\mathbb {IL}_{\rhd }$
are obtained by adding the axiom schemas that we discussed in §2.1 and §3; they will be denoted analogously to the systems based on multimodal
$\mathbb {IL}$
.
The calculi we will present are obtained by labelling the formulas in
$\mathtt {Form}_{\rhd }$
. The classes of models we are using for the definition of these calculi are based on Verbrugge semantics: This is in line with the procedure initiated by Negri [Reference Negri28] for relational semantics and generalised further to neighbourhood semantics in e.g., [Reference Girlando, Negri and Olivetti9, Reference Girlando, Negri, Olivetti and Risch10, Reference Negri31].Footnote
17
4.1 Core system
By
$\mathsf {G3IL}$
we denote the labelled sequent calculus for
$\mathbb {IL}_{\rhd }$
. The design of
$\mathsf {G3IL}$
is based on an explicit internalisation of GVS employing labels, which formalises the semantic information into a proof system.
According to Definition 3.2, the forcing condition for the
$\rhd $
-modality is
As it comes, that forcing condition cannot be directly translated into a single sequent calculus geometric rule because of the presence of alternating nested quantifiers on the right-hand side of (
$\sharp $
).Footnote
18
To circumvent that issue, it is convenient to introduce an intermediate indexed modality, which obeys the following forcing condition
where 
abbreviates the expression “for any
$z\in a, z\Vdash B$
”, as in (
$\sharp $
).
The forcing condition for
$\rhd $
can then be rephrased as
$$ \begin{align*} \begin{array}{l l l l} \displaystyle (\sharp\flat)&\displaystyle x\Vdash A\rhd B &\displaystyle \textrm{iff} &\displaystyle \textrm{for all } y, \textrm{if } xRy \textrm{ and } y\Vdash A,\\ & & & \displaystyle\textrm{then } y\Vdash \langle]_{x} B. \end{array} \end{align*} $$
Unfortunately, this is not enough yet. Models for
$\mathbb {IL}$
are based on frames for Gödel–Löb logic, that is: irreflexive, transitive and finite—or, alternatively, transitive and Noetherian. Neither finiteness nor Noetherianity can be expressed by a semantic rule in line with the methodology of explicit internalisation available so far in the literature.
However, the treatment of Gödel–Löb logic described in [Reference Negri30] gives the right hint for proceeding with the design. Notice first that condition (
$\sharp \flat $
) establishes the logical equivalence
$$ \begin{align} x\Vdash A\rhd B\qquad\textrm{iff}\qquad x\Vdash\Box(A\rightarrow\langle]_{x}B). \end{align} $$
Moreover, we know that in any model based on
$\textit {ITF}$
Footnote
19
$$ \begin{align} x\Vdash\Box A\qquad\textrm{iff}\qquad\,\,\textrm{for any}\,\,y,\,\,\textrm{if}\,\,xRy\,\,\textrm{and}\,\,y \Vdash\Box A,\,\,\textrm{then}\,\,y\Vdash A. \end{align} $$
This suggests to index with worlds the
$\rhd $
-modality and, by chaining the equivalences (1) and (2), we can safely take the following forcing condition for that indexed
$\rhd $
-modality whenever we are reasoning in models based on GVS:
$$ \begin{align*} \begin{array}{l l l l} \displaystyle (\natural) &\displaystyle x\Vdash A\rhd_{i} B &\displaystyle \textrm{iff} &\displaystyle \textrm{for all } y, \textrm{if } xRy \textrm{ and } y\Vdash A\rhd_{i}B,\\ & & &\displaystyle \textrm{then, if } y\Vdash A,\,\, y\Vdash\langle]_{i} B. \end{array} \end{align*} $$
Let
$\mathtt {Form}_{\rhd }^{i}$
denote the formulas allowing indexed
$\rhd $
-modalities as well as the intermediate indexed modalities
$\langle ]_{x}$
.
We are now ready to define the labelled sequent calculus
$\mathsf {G3IL}$
.
Definition 4.3. Let
$i,j,k,\ldots ,x,y,z,\ldots $
be variables for worlds in a Verbrugge model, and
$s,t,u,\ldots $
variables for neighbourhoods. By neighbourhood term
$a,b,c,\ldots $
we refer to a neighbourhood variable or an expression of shape
$\{x\}$
or
$R[x]$
for x a world variable.
Relational atoms are formulas of the following form and meaning:
-
•
$y\in R[x]$
, “world
$y$
is accessible to world
$x$
”; -
•
$yS_{x}a$
, “neighbourhood
$a$
is
$S_{x}$
-accessible to world
$y$
”; -
•
$y\in a$
, “world
$y$
is a member of neighbourhood
$a$
”; -
•
$a\subseteq b$
, “neighbourhood
$a$
is included into neighbourhood
$b$
”.
We will use
$\{x\}$
to denote the singleton neighbourhood of exactly the world
$x$
.
Labelled formulas are defined as follows, for
$A\in \mathtt {Form}_{\rhd }^{i}$
:
-
• Relational atoms are labelled formulas;
-
•
$x:A$
, “world
$x$
forces formula A”; -
•
$a\Vdash ^{\forall }A$
, “formula A is forced by any world belonging to neighbourhood
$a$
”.
Definition 4.4. Sequents of
$\mathsf {G3IL}$
are expressions
$\Gamma \Rightarrow \Delta $
, where
$\Gamma $
and
$\Delta $
are multisets of labelled formulas, and relational atoms may occur only in
$\Gamma $
.
The rules defining
$\mathsf {G3IL}$
are given in Figure 3.
Rules for
$\mathsf {G3IL.}$
Remark 2. Some of those rules might deserve a little explanation:
-
• Side condition
$(x!)$
in expresses the fact that x is a ‘fresh varibale’, i.e., it does not occur in the conclusion of the rule; similarly for
$(y!)$
in
$\mathcal {R}\rhd _{i}$
; the meaning of
$(a!)$
in
$\mathcal {L}\langle ]$
is analogous; the meaning of
$(z!)$
in the rule
$\textit {NE}$
is analogous. -
• The rules for
$\langle ]_{x}$
are defined according to the forcing condition (
$\flat $
), following the standard practice for labelled sequent calculi based on neighbourhood semantics.Footnote
20
-
• The rules for
$\rhd _{i}$
are defined according to the forcing condition (
$\natural $
). -
• The rules for GVS are defined as geometric rules of Negri and von Plato [Reference Negri and von Plato33]; in particular, we opted for an alternative definition of quasi-transitivity of the indexed S-relation. The condition imposed by Definition 3.2 is
This condition cannot be directly translated as a geometric rule with the language at hand: recall from e.g., [Reference Negri and von Plato33] that every geometric formula can be shown to be equivalent to a formula of shapeif
$yS_{x}a$
and
$vS_{x}b_{v}$
for all
$v\in a$
, then
$yS_{x}(\bigcup _{v\in a}b_{v})$
.where
$$ \begin{align*} \forall\vec{x}(P_{1}\wedge\cdots\wedge P_{m}\rightarrow\exists\vec{y_{1}}\mathbf{Q_{1}}\vee\cdots\vee\exists\vec{y_{n}}\mathbf{Q_{n}}), \end{align*} $$
$P_{i}$
and
$\mathbf {Q_{j}}$
are atomic formulas and finite conjunctions of atomic formulas, respectively.Every geometric formula can then be converted into an n-ary geometric rule:where
$\vec {P}$
corresponds to
$P_{1},\ldots ,P_{m}$
and
$[y_{i}/x_{i}]$
denotes the replacement of the variable
$x_{i}$
with a fresh variable
$y_{i}$
which does not occur in the conclusion of the rule.Nevertheless, in the literature, it is possible to find several different conditions for quasi-transitivity:Footnote
21
Condition 2 is the most natural: the monotone closure of any
$S_{x}$
that satisfies any of conditions 1–8 also satisfies condition 2, allowing us to define an equivalent model. For conditions 3–6, obtaining a related standard model from a GVS model is always possible, as demonstrated in [Reference Joosten, Rovira, Mikec, Vuković, Bezhanishvili, Iemhoff and Yang17, Reference Verbrugge50]. The rule
$\textit {Qtrans6}$
represents the natural formalization of condition 6 from the previous table, which is the simplest one according to the methodology outlined in [Reference Negri and von Plato33] that we have briefly summarised. However, the correspondence between GVS models satisfying condition 6 and standard Veltman models limits the expressive power of our current systems. To achieve full adequacy of the interpretability logics under investigation with respect to the notion of Verbrugge frames standard in the literature—i.e., based on condition 2—we need to revise this semantic rule, as issue that we intend to tackle in future work.Footnote
22
-
• Rule
$\textit {Sing}$
assures that the singleton contains at least one element; rules
$\textit {Repl}_{1}$
and
$\textit {Repl}_{2}$
that it contains at most one element, for indiscernibility of identicals. -
• From Figure 3 the rules obtained by the closure condition of the system, discussed in [Reference Negri28], are omitted. For some rules dealing with GVS—for instance,
$\textit {Trans}$
—there might be a duplication of a relational atom in the conclusion. Structural considerations—namely, the desideratum of admissibility of contraction—require then that a new rule is added to the system, in which the duplicated formulas are contracted into one.Footnote
23
However, the rules added to a system in order to satisfy such a closure condition play no role in the proof of semantic completeness of the calculi we are considering here, and they can be shown to be admissible. This justifies our omission in favour of a better readability of the figure.
expresses the fact that x is a ‘fresh varibale’, i.e., it does not occur in the conclusion of the rule; similarly for 
Here, we see that the version of Verbrugge semantics for
$\mathbb {IL}$
adopted here can be considered a geometric theory, and thus, it can be formalised by a sequent calculus based on purely geometric rules.
4.2 Extensions
Calculi for extensions of
$\mathbb {IL}$
are denoted by adding to
$\mathsf {G3IL}$
the name of a modal schema as apex. Thus, for instance,
$\mathsf {G3IL^{M}}$
is the labelled calculus for
$\mathbb {ILM}$
, and
$\mathsf {G3IL^{P}}$
is the labelled calculus for
$\mathbb {ILP}$
. We denote by
$\mathsf {G3IL}^{\star }$
the whole family of calculi for the interpretability logics considered in Definition 2.4.
Figure 4 shows the rules for the
$\mathbb {IL}$
extensions in which we are interested.
Rules for
$\mathsf {G3IL}^{\star }.$
As the reader sees, these rules are obtained by considering the generalised frame conditions characterising each
$\mathbb {IL}$
extension. Moreover, we need to consider an extension of the language of labelled formulas.
Definition 4.5. Extend Definition 4.3 by considering among neighbourhood labels expressions of shape
$\varnothing $
,
$a \cap b$
,
$R[a]$
, and
$S_x^{-1}a$
with
$a,b$
neighbourhood labels and x a world label. Relational atoms are accordingly defined as follows:
-
•
$y\in a\cap b$
, “world y if a member of both neighbourhood a and neighbourhood b”; -
•
$y\in R[a]$
, “world y is accessible to a world x belonging to a”; -
•
$y\in S_{x}^{-1}a$
, “neighbourhood a is
$S_{x}$
-accessible to a world y”; -
•
$x\in \varnothing $
, “world x is a member of the neighbourhood
$\varnothing $
” – we take the latter as the only constant for neighbourhoods of our language.
Labelled formulas are defined as in Definition 4.3 w.r.t. this extended set of relational atoms.
5 Structural properties
We now want to study the structural properties of
$\mathsf {G3IL}^{\star }$
. In order to proceed, we need first some preliminary definitions.
By the height of a derivation, we mean the number of nodes occurring in the longest derivation branch minus one. In particular, the height of a derivation consisting only of an initial sequent is 0. We write
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta $
whenever there is a derivation of the sequent
$\Gamma \Rightarrow \Delta $
in
$\mathsf {G3IL}^{\star }$
with height bounded by n.
Next, we need the notion of weight of labelled formulas.
Definition 5.1. The weight of relational atoms is 0. As for the other labelled formulas, let us say that the label of
$x:A$
is
$x$
, and the label of 
is
$a$
. The label of a formula
$\varphi $
is denoted by
$l(\varphi )$
, and
$p(\varphi )$
denotes the pure part of the formula, i.e., the part of the formula without the label and the forcing condition.
The weight
$\mathfrak {w}(\varphi )$
of a labelled formula
$\varphi $
which is not a relational atom is given by the ordered pair
$\langle \mathfrak {w}(p(\varphi )),\mathfrak {w}(l(\varphi )\rangle ,$
where
-
• For all world labels
$x$
and all neighbourhood labels
$a$
,
$\mathfrak {w}(x)=0$
and
$\mathfrak {w}(a)=1+n(\cap )$
, where
$n(\cap )$
denotes the number of formal intersections in a; -
•
$\mathfrak {w}(p)=\mathfrak {w}(\bot )=1$
; -
•
$\mathfrak {w}(A\circ B)=\mathfrak {w}(A)+\mathfrak {w}(B)+1$
, for
$\circ $
conjunction, disjunction or implication; -
•
$\mathfrak {w}(\langle ]_{i}A)=\mathfrak {w}(A)+1;$
-
•
$\mathfrak {w}(A\rhd _{i}B)=\mathfrak {w}(A)+\mathfrak {w}(B)+2$
.
In the following, when reasoning by induction on the weight of a labelled formula we do so by considering the lexicographic order on
$\langle \mathfrak {w}(p(\varphi )),\mathfrak {w}(l(\varphi )\rangle $
:
$\langle \mathfrak {w}(p(\varphi )),\mathfrak {w}(l(\varphi )\rangle \leq \langle \mathfrak {w}(p(\varphi ')),\mathfrak {w}(l(\varphi ')\rangle $
if and only if
$\mathfrak {w}(p(\varphi ))<\mathfrak {w}(p(\varphi '))$
or
$\mathfrak {w}(p(\varphi ))=\mathfrak {w}(p(\varphi '))$
and
$\mathfrak {w}(l(\varphi )<\mathfrak {w}(l(\varphi ')$
For substitution of labels, we can rely on the definitions given in [Reference Negri31, Reference Negri and von Plato33]. We borrow notation from those works and write, e.g., 
to mean the result of simultaneously substituting b for a, this way obtaining 
; similarly for world label substitution.
It is now routine to show that
$\mathsf {G3IL}^{\star }$
enjoys height preserving substitution for world and neighbourhood labels.
Proposition 5.2. The following hold:
-
(i) If
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta $
, then
$\overset {n}{\vdash }\Gamma [y/x]\Rightarrow \Delta [y/x]$
; -
(ii) If
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta $
, then
$\overset {n}{\vdash }\Gamma [b/a]\Rightarrow \Delta [b/a]$
.
Proof. Straightforward induction on n. If
$n=0$
, then
$\Gamma \Rightarrow \Delta $
is an initial sequent, or a conclusion of
$\mathcal {L}\bot $
,
$\mathcal {L}\varnothing $
, or
$\textit {Irrefl}$
. The same is true for
$\Gamma [y/x]\Rightarrow \Delta [y/x]$
and for
$\Gamma [b/a]\Rightarrow \Delta [b/a]$
.Footnote
24
If
$n>0$
, we consider the last rule applied. If the latter has no variable conditions, we apply the inductive hypothesis to the premise(s), followed by that very rule. Otherwise, the rule needs some care in case the substituted variable coincides with the fresh variable of the premise. In that case, we need to apply twice the inductive hypothesis to the premise, first to replace the fresh variable with another fresh variable—different from the one we wish to substitute—and secondly, to perform the desired substitution.
5.1 General initial sequents, weakening, contraction, invertibility
Let
$\varphi $
denote either a relational atom or a (proper) labelled formula for the remaining sections.
We start with a relatively simple result.
Lemma 5.3. The following sequents are derivable in
$\mathsf {G3IL}^{\star }$
:
-
1.
; -
2.
$x:A,\Gamma \Rightarrow \Delta ,x:A$
.
;
Proof. The two cases are proven by mutual induction on the weight of the labelled formulas. The general strategy is to apply the left and right rule to treat the two formula occurrences until two formula occurrences of smaller weight are reached.
By means of example, we prove case 2, subcase
$x:\langle ]_{i}A$
:
where we can apply the inductive hypothesis to the top sequent since
$\mathfrak {w}(a\Vdash ^{\forall }A)<\mathfrak {w}(x:\langle ]_{i}A)$
.
Notice that the subcase
$x:A\rhd _{i}B$
is easily managed since sequents
$x:A\rhd _{i}B,\Gamma \Rightarrow \Delta ,x:A\rhd _{i}B$
are initial, and hence derivable by design.
We want now to establish the admissibility of weakening in
$\mathsf {G3IL}^{\star }$
.
Lemma 5.4. The rules of weakening
are height-preserving admissible in
$\mathsf {G3IL}^{\star }$
.
Proof. We need to show that if
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta $
, then
$\overset {n}{\vdash }\varphi ,\Gamma \Rightarrow \Delta $
and
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta ,\varphi $
. The proof consists of a straightforward induction on n, following the lines of the analogous results in [Reference Negri31, Reference Negri and von Plato33], which the reader is referred to for the details.
Next, we can prove that all the rules of
$\mathsf {G3IL}^{\star }$
are invertible.Footnote
25
Lemma 5.5. All the rules of
$\mathsf {G3IL}^{\star }$
are invertible.
Proof. We proceed by induction on the height of the derivation, distinguishing cases based on the rule under consideration. Notice first that the rules for extensions are clearly (height-preserving) invertible by (height-preserving) admissibility of weakening; the same remark applies to the rules for GVS, as well as to
$\mathcal {L}\rhd $
, 
, and
$\mathcal {R}\langle ]$
. Propositional cases are dealt with as in [Reference Negri28]. The cases
$\mathcal {L}\langle ]$
and 
are the same as in [Reference Negri31]. We can thus focus our proof on the invertibility of
$\mathcal {R}\rhd $
. Assume then that
$\overset {n}{\vdash }\Gamma \Rightarrow \Delta ,x:A\rhd _{i}B$
. If
$n=0$
and
$x:A\rhd _{i}B$
is not principal, then also
$\overset {0}{\vdash }y\in R[x],y:A,y:A\rhd _{i}B,\Gamma \Rightarrow \Delta ,y:\langle ]_{i}B$
. If it is principal, then
$\Gamma =\Gamma ',x:A\rhd _{i}B$
and we need to prove that
$$ \begin{align*}y\in R[x],y:A,y:A\rhd_{i}B,\Gamma',x:A\rhd_{i}B\Rightarrow\Delta,y:\langle]_{i}B\end{align*} $$
is derivable. But this is provable by application of
$\mathcal {L}\rhd $
to the initial sequent
$$ \begin{align*}y\in R[x],y:A,y:A\rhd_{i}B,\Gamma',x:A\rhd_{i}B\Rightarrow\Delta,y:\langle]_{i}B,y:A\rhd_{i}B\end{align*} $$
with the sequents
$$ \begin{align*}y\in R[x],\mathbf{y:A},y:A\rhd_{i}B,\Gamma',x:A\rhd_{i}B\Rightarrow\Delta,y:\langle]_{i}B,\mathbf{y:A}\end{align*} $$
and
$$ \begin{align*}\mathbf{y:\langle]_{i}B},y\in R[x],y:A,y:A\rhd_{i}B,\Gamma',x:A\rhd_{i}B\Rightarrow\Delta,\mathbf{y:\langle]_{i}B},\end{align*} $$
which are both derivable in virtue of the highlighted labelled formulas occurring on both sides of each sequent (Lemma 5.3.(1))
If
$n>0$
and
$x:A\rhd _{i}B$
is principal in the last rule, then we have the desired result. Otherwise, applying the inductive hypothesis to the premise(s) suffices.
Remark 3. Notice that Lemma 5.5 cannot be strengthened into a height-preserving invertibility of the rules just because of the case we discussed in its proof: This is analogous to what happens for
$\mathsf {G3GL}$
in [Reference Negri28], which we used as a model for the design of
$\mathsf {G3IL}^{\star }$
.
We now want to prove the admissibility of contraction. Before we proceed with the proof, it is appropriate to introduce a notion that will also be used in the proof of cut elimination.
Definition 5.6 (After Negri and von Plato [Reference Negri and von Plato33]).
The range
$\mathfrak {r}(x)$
of a world label
$x$
in a derivation
$\mathcal {D}$
in
$\mathsf {G3IL}^{\ast }$
is the set of world labels y such that either
$y\in R[x]$
or for some
$n\geq 1$
and for some
$x_{1},\ldots ,x_{n}$
the relational atoms
$x_{1}\in R[x]$
,
$x_{2}\in R[x_{1}]$
,
$\ldots , y\in R[x_{n}]$
appear in the antecedent of sequents of
$\mathcal {D}$
. The range
$\mathfrak {r}(a)$
of a neighbourhood label
$a$
in
$\mathcal {D}$
is defined as
$\mathfrak {r}(a):=\textit {max}\{\mathfrak {r}(x)\,|\,x\in a\}\cup \{\ast \}$
ordered w.r.t. set inclusion. We set
$\mathfrak {r}(\{x\})=\mathfrak {r}(x)$
and
$\mathfrak {r}(\varnothing )=\varnothing $
.
Finally, we say that a rule is range-preserving admissible if the rule’s elimination does not increase the ranges of labels in the derivation.
Theorem 5.7. The rules of contraction
are range-preserving admissible in
$\mathsf {G3IL}^{\star }$
.
Proof. By simultaneous induction for left and right contraction, with primary induction on the weight of the contracted formula and secondary induction on the height of the derivation. The only case requiring some care is when the contracted formula is
$x:A\rhd _{i}B$
in the consequent, of weight n. If the contracted formula is not principal for the last rule in the derivation—i.e. the latter is not
$\mathcal {R}\rhd $
on
$x:A\rhd _{i}B$
—then we apply the secondary inductive hypothesis to the premise(s), followed by the rule. Otherwise, we invert the premise of
$\mathcal {R}\rhd $
to obtain
$$ \begin{align*}y\in R[x],y:A,y:A\rhd_{i}B,y\in R[x],y:A,y:A\rhd_{i}B,\Gamma\Rightarrow\Delta,y:\langle]_{i}B,y:\langle]_{i}B.\end{align*} $$
By applying the main inductive hypothesis once for
$y\in R[x]$
, once for
$y:A$
, and once for
$y:\langle ]_i B$
to get
$$ \begin{align*} y:A\rhd_{i}B,y\in R[x],y:A,y:A\rhd_{i}B,\Gamma\Rightarrow\Delta,y:\langle]_{i}B. \end{align*} $$
Now, we claim that the following rule is height- and range-preserving admissible:
and we prove it by primary induction on the weight of the contracted formula and secondary induction on the height of the derivation: If none instance of
$w:A\rhd _i B$
is the main formula in the last rule of the derivation, then the height of the derivation is
$0$
and we can contract any formulas without increasing the height, as initial sequents are arbitrary weakened by design; if, on the contrary, one instance of
$w:A\rhd _i B$
is the main formula of the last rule, then the derivation is as follows:
where S is the sequent
$v\in R[w],w:A\rhd _{i} B,w:A\rhd _{i} B,\Gamma \Rightarrow \Delta ,v:A\rhd _{i} B$
.
We can apply the secondary induction hypothesis to each premise and then apply the
$\mathcal {L}\rhd _i$
rule to get the desired conclusion.
Thus, we can use the just proven claim on
$$ \begin{align*}y\in R[x],y:A\rhd_{i}B,y\in R[x],y:A,y:A\rhd_{i}B,\Gamma\Rightarrow\Delta,y:\langle]_{i}B.\end{align*} $$
to derive then the conclusion of
$\mathcal {R}\textit {Ctr}$
by application of
$\mathcal {R}\rhd _i$
.
The range is preserved since, in inverting
$\mathcal {R}\rhd $
and in the proof of the intermediate claim, we use labels already present in the derivation tree.
For the other cases, refer to e.g., [Reference Negri31, Reference Negri and von Plato33].
5.2 Cut elimination theorem
We have finally collected all the material required to prove the paper’s main result, namely, cut elimination for
$\mathsf {G3IL}^{\star }$
.
Theorem 5.8 (Cut admissibility).
The rule of cut
is admissible in
$\mathsf {G3IL}^{\star }$
.
Proof. The proof proceeds by primary induction on the weight of the cut formula, secondary induction on the range of the label of the cut formula,Footnote 26 and tertiary induction on the sum of heights of the cut premises.
Notice first that if y is in the range of x, then
$\mathfrak {r}(y)\subsetneq \mathfrak {r}(x)$
because of the proof system design.
Following [Reference Negri and von Plato32, Reference Negri and von Plato33], we start by distinguishing cases according to the rules applied to derive the premises of cut:
-
1. At least one of the premises of Cut is an initial sequent;
-
2. The cut formula is not principal in the derivation of at least one premise;
-
3. The cut formula is the principal formula of both derivations of the premises.
-
Case 1. Assume the leftmost premise of Cut is an initial sequent. If the cut formula is
$x:p$
or
$x:A\rhd _iB$
, then by weakening the rightmost premise, we obtain the cut conclusion. If the sequent is initial in virtue of some labelled formula
$\psi $
occurring in both
$\Gamma $
and
$\Delta $
, then the conclusion of Cut is an initial sequent too.A similar argument works if we assume that the rightmost premise of Cut is an initial sequent.
If
$x:\bot $
is the cut formula
$\varphi $
and the leftmost premise of Cut is not initial, we have derived it by some rule R. If R is
$\mathcal {L}\bot $
, then
$x:\bot $
occurs in the conclusion of the cut, and therefore we can obtain that sequent from
$\mathcal {L}\bot $
. Similarly if R is
$\mathcal {L}\varnothing $
or Irrefl. Otherwise, if R is different from
$\mathcal {L}\bot $
,
$\mathcal {L}\varnothing $
and Irrefl, we can permute the cut up on the left premise and eliminate it by inductive hypotheses. -
Case 2. Assume the cut formula is not principal in the last rule leading to the leftmost premise of Cut. The general situation is the following:
Then, we perform the following lifting of the cut and rely on the inductive hypotheses:
Next, we have the subcases of
$\textit {Repl}_{1}$
and
$\textit {Repl}_{2}$
. We describe the situation with the right premise of Cut obtained by
$\textit {Repl}_{1}$
since the general setting follows the same line of reasoning. Assume then we haveNow, if
$\mathcal {D}_{1}$
is an initial sequent, or if
$x:\bot $
,
$x\in \varnothing $
, or
$x\in R[x]$
occurs in
$\Gamma $
we can weaken the right premise of Cut, or recur to the appropriate 0-ary
$\mathcal {L}$
-rule. Otherwise, we must have derived the left premise of the cut by some rule, and
$x:p$
cannot be its principal formula. Lifting the cut does the job. -
Case 3. We omit the propositional (sub)cases, referring to [Reference Negri and von Plato33, theorem 11.9].
Notice first that we do not need to consider the rules for GVS nor the rules for extensions of
$\mathbb {IL}$
since, by design, relational atoms only occur in the antecedent of sequents.For the local forcing rules, we have
which is solved by
where the upper cut is on derivations of smaller height and on a label of the same range; the lower one is on formulas of smaller weight. Application(s) of contraction to the conclusion gives the cut conclusion.
For the intermediate modality, we have
which is solved by
where the upper cut is on derivations of smaller height, and the lower one is on formulas of smaller weight. Application(s) of contraction to the conclusion gives the cut conclusion.
Finally, we consider the case of rules for
$\rhd $
. The general setting is
where
-
$\mathcal {D}_{2}$
is a derivation of
$y\in R[x],x:A\rhd _{i} B,\Gamma '\Rightarrow \Delta ',y:A$
;
-
$\mathcal {D}_{3}$
is a derivation of
$y:\langle ]_{i}B,y\in R[x],x:A\rhd _{i} B,\Gamma '\Rightarrow \Delta '$
; and
-
$\mathcal {D}_{4}$
is a derivation of
$y\in R[x],x:A\rhd _{i} B,\Gamma '\Rightarrow \Delta ',y:A\rhd _{i} B$
.
Perform the following steps:
-
a.
where the cut is on derivations of smaller height.
-
b.
where the cut is on derivations of smaller height.
-
c.
where the cut is on derivations of smaller height.
-
d. Finally proceed as follows:
where the first cut from the top is on a label of a smaller range, and the second and the third are on formulas of smaller weight.Footnote 27 We obtain the conclusion of the original cut by applying steps of contraction to the conclusion of the derivation described at point d.
Now that we know that the cut rule is admissible in
$\mathsf {G3IL}^{\star }$
, we can prove the admissibility of generalised replacement rules.
Lemma 5.9. The rules
$\textit {Repl}_{1}$
and
$\textit {Repl}_{2}$
generalised to all formulas of the language are admissible in
$\mathsf {G3IL}^{\star }$
.
Proof. By simultaneous induction on the weight of formulas. Since contraction and cut are admissible for our calculi, it is enough to prove that the sequent
$y\in \{x\},\varphi (x)\Rightarrow \varphi (y)$
is derivable for any labelled formula
$\varphi $
, and then apply a Cut, followed by contraction steps, to the premise of generalised
$\textit {Repl}_{1}$
. For
$\textit {Repl}_{2}$
, we reason symmetrically.
The proof then proceeds by a straightforward induction on the weight of
$\varphi (x)$
on the lines of [Reference Negri and von Plato32, lemma 6.5.2].
Remark 4. Raymond Smullyan famously wrote in [Reference Smullyan44]:
“The real importance of cut-free proofs is not the elimination of cuts per se, but rather that such proofs obey the subformula principle.”
For classical propositional logic, cut admissibility guarantees that the subformula principle holds in
$\mathsf {G3cp}$
, as documented in [Reference Troelstra and Schwichtenberg49]. For labelled calculi, that principle needs to be relaxed. In its original version, the subformula property holds whenever any sequent occurring in a derivation of a given sequent
$\Gamma \Rightarrow \Delta $
contains only subformulas of the formulas composing the latter. In our systems, the rules for
$\rhd $
introduce the intermediate modality
$\langle ]_{i}$
by decomposing
$A\rhd _{i}B$
into A and
$\langle ]_{i}B$
, and the latter is not, in strict terms, a subformula of
$A\rhd _{i}B$
. However, its weight is defined to be smaller than that of interpretability formulas: Therefore, we might say that it is less complex and, in that flexible sense, loosely generated by a
$\rhd $
-formula. Moreover, it is not hard to prove a pureness condition on labels: In
$\mathsf {G3IL}^{\star }$
, any derivation contains either eigenvariables in rules with freshness condition or labels already present in the conclusion. In this sense, the family of calculi we have designed can be considered analytic, in line with the standard
$\mathsf {G3}$
paradigm.
6 Completeness
In this section, we prove that our family of labelled sequent calculi is sound and complete w.r.t. the semantic and axiomatic presentations of interpretability logics under investigation.
We give syntactic proofs of those results and then discuss some aspects concerning a direct proof of semantic completeness for
$\mathsf {G3IL}^{\star }$
.
6.1 Syntactic completeness
For a start, we need to interpret the underlying language of the labelled formulas into
$\mathcal {L}_{\rhd }$
, in which the modality is not indexed. Therefore, we agree to read
$x:A\rhd B$
as
$x:A\rhd _{x}B$
, unless otherwise stated.
We immediately have the following theorem.
Theorem 6.1 (Completeness).
If a formula A is derivable in
$\mathbb {IL}$
or any of its extensions from Definition 2.4, then there is a derivation of the sequent
$\Rightarrow x:A$
in the calculus
$\mathsf {G3IL}^{\star }$
for the corresponding logic.
Proof. We rely on the equivalence between
$\mathbb {IL}$
and
$\mathbb {IL}_{\rhd }$
and prove that all the axiom schemas and inference rules of the latter are derivable or proven to be admissible in
$\mathsf {G3IL}$
. For the extensions, we only need to prove the axiom schema corresponding to the specific semantic rule of the family of labelled systems.
We recall the axiomatisation of
$\mathbb {IL}_{\rhd }$
and its extensions from Definition 4.2 and §2.1:
For propositional logic, the derivability of axiom schemas is straightforward; the admissibility of cut assures the admissibility of modus ponens.
Next notice that the simpler
$\mathcal {L}$
-rule for
$\rhd $
is admissible in our systems, for any sequent of the form
$$ \begin{align*} y\in R[x],x:A\rhd_{i} B,\Gamma\Rightarrow\Delta,y:A\rhd_{i} B \end{align*} $$
is derivable in
$\mathsf {G3IL}^{\ast }$
.
The same holds for the rule
Now, we proceed with the basic calculus:
-
$\mathsf {IL2}$
: The derivation is rendered in Figure 5.
-
$\mathsf {IL3}$
: The derivation is rendered in Figure 6.
-
$\mathsf {IL}\text {-}\textsf {Löb}$
: The derivation is rendered in Figure 7.
-
$\rhd $
Rule: The derivation is as follows:
The derivations of each principle in the corresponding extension of
$\mathsf {G3IL}$
are given in Appendix A.
Derivation of
$\mathsf {IL2}$
.
Derivation of
$\mathsf {IL3}$
.
Derivation of
$\mathsf {IL}\text {-}\textsf {Löb}$
.
6.2 Soundness
We must interpret relational atoms and labelled formulas in Verbrugge models to prove the converse direction. The calculi per se do not have a direct formula interpretation in the language of
$\mathtt {Form}^{(i)}_{\rhd }$
but we can define an interpretation for them in GVS: We need a function that interprets the labels in Verbrugge frames, thus connecting the syntactic elements of the calculus with the semantic notions of §3.2.
Definition 6.2. Let
$\mathcal {M}=\langle W, R, \{S_{x}\}_{x\in W}, v\rangle $
be a Verbrugge model for
$\mathbb {IL}$
or its extensions,
$\mathcal {W}$
a set of world labels, and
$\mathcal {A}$
a set of neighbourhood labels. A
$\mathcal {WA}$
-interpretation over
$\mathcal {M}$
consists of a pair of functions
$(\rho ,\sigma )$
such that:
-
•
$\rho :\mathcal {W}\rightarrow W$
maps each
$i\in \mathcal {W}$
into a world
$\rho (i)\in W$
; -
•
$\sigma :\mathcal {A}\rightarrow \wp (W)$
maps each
$a\in \mathcal {A}$
into a nonempty set of worlds
$\sigma (a)\in \wp (R[x])$
, for
$x\in W$
, and
$\varnothing $
into
$\varnothing $
.
The notion of satisfiability of a labelled formula under a
$\mathcal {WA}$
-interpretation is defined by cases on the form of that formula:
-
•
$\rho ,\sigma \vDash _{\mathcal {M}} y\in R[x]$
if
$\rho (x)R\rho (y)$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} y\in a$
if
$\rho (y)\in \sigma (a)$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} yS_{x}a$
iff
$y\in S_{x}^{-1}a$
: if
$\rho (y)S_{\rho (x)}\sigma (a)$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} y\in R[a]$
if, for some
$x\in \sigma (a)$
,
$xR\rho (y)$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} a\subseteq b$
if
$\sigma (a)\subseteq \sigma (b)$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} y\in \{x\}$
if
$\rho (y)\in \{\rho (x)\}$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} yS_{i}\{x\}$
if
$\rho (y)S_{\rho (i)}\{\rho (x)\}$
; -
•
$\rho ,\sigma \vDash _{\mathcal {M}} x:p$
if
$\rho (x)\Vdash _{\mathcal {M}} p$
, and similarly for formulas obtained by classical propositional connectives; -
•
if ; -
•
$\rho ,\sigma \vDash _{\mathcal {M}}x:\langle ]_{i} A$
if, for some
$a\in (\wp (R[\rho (i)])\smallsetminus \{\varnothing \})$
,
$\rho (x)S_{\rho (i)}a$
and ; -
•
$\rho ,\sigma \vDash _{\mathcal {M}}x:A\rhd _{i}B$
if, for all
$y\in R[\rho (x)]$
, if
$y\Vdash _{\mathcal {M}}A$
, then
$y\Vdash _{\mathcal {M}}\langle ]_{\rho (i)}B$
.
if 
;
;
Given a sequent
$\Gamma \Rightarrow \Delta $
, let
$\mathcal {W},\mathcal {A}$
be the sets of world and neighbourhood labels occurring in
$\Gamma \cup \Delta $
, and let
$(\rho ,\sigma )$
be a
$\mathcal {WA}$
-interpretation.
Define
$\rho ,\sigma \vDash _{\mathcal {M}}\Gamma \Rightarrow \Delta $
if either
$\rho ,\sigma \not \vDash _{\mathcal {M}}\varphi $
for some
$\varphi \in \Gamma $
or
$\rho ,\sigma \vDash _{\mathcal {M}}\psi $
for some
$\psi \in \Delta $
. Define then validity under all interpretations by
$\vDash _{\mathcal {M}}\Gamma \Rightarrow \Delta $
if and only if
$\rho ,\sigma \vDash _{\mathcal {M}}\Gamma \Rightarrow \Delta $
for all
$(\rho ,\sigma )$
. Finally, let us say that a sequent is valid in all Verbrugge models if
$\vDash _{\mathcal {M}}\Gamma \Rightarrow \Delta $
for all models based on GVS appropriate to a specific interpretability logic.
Theorem 6.3 (Soundness).
If a sequent
$\Rightarrow x:A$
is derivable in
$\mathsf {G3IL}^{\star }$
, then A is a theorem of
$\mathbb {IL}$
or of the corresponding extension.
Proof. We prove something stronger, namely:
-
If a sequent
$\Gamma \Rightarrow \Delta $
is derivable in
$\mathsf {G3IL}^{\star }$
, then it is valid in the corresponding class of Verbrugge models.
If a sequent 
The main theorem follows by modal completeness of the axiomatic calculi for interpretability we are dealing with.
Now, the proof of 
is by straightforward induction on the height of the derivation, by recurring to the notion of interpretation defined before. By means of example, we show the soundness of the left and right rule for the
$\rhd $
-operator.
-
$\mathcal {L}\rhd $
By inductive hypothesis we have
$$ \begin{align*}\rho,\sigma\vDash_{\mathcal{M}}y\in R[x],x:A\rhd_{i} B,\Gamma\Rightarrow\Delta,y:A;\end{align*} $$
$$ \begin{align*}\quad\rho,\sigma\vDash_{\mathcal{M}}y:\langle]_{i}B,y\in R[x],x:A\rhd_{i} B,\Gamma\Rightarrow\Delta;\end{align*} $$
$$ \begin{align*}\rho,\sigma\vDash_{\mathcal{M}}y\in R[x],x:A\rhd_{i} B,\Gamma\Rightarrow\Delta,y:A\rhd_{i} B.\end{align*} $$
There are two relevant cases to consider.
One has
$\rho ,\sigma \vDash _{\mathcal {M}}y:A$
,
$\rho ,\sigma \vDash _{\mathcal {M}}y\in R[x]$
and
$\rho ,\sigma \not \vDash _{\mathcal {M}}\langle ]_{i}B$
. From the former we have that
$\rho (y)\Vdash A$
; from the latter that
$\rho (y)\not \Vdash \langle ]_{i}B$
. By definition, this means that
$\rho ,\sigma \not \vDash _{\mathcal {M}}x:A\rhd _{i}B$
, so that
$\rho ,\sigma \vDash _{\mathcal {M}}y\in R[x],x:A\rhd _{i}B,\Gamma \Rightarrow \Delta $
.The second one is
$\rho ,\sigma \vDash _{\mathcal {M}}y\in R[x]$
and
$\rho ,\sigma \not \vDash _{\mathcal {M}}y:A\rhd _{i}B$
. From the latter we have that
$\rho (y)\not \Vdash A\rhd _{i}B$
, from which we know that there exists a
$z\in R[y]$
such that
$z\Vdash A$
and
$z\not \Vdash \langle ]_{i}B$
. By transitivity, we can reduce the situation to the first one. -
$\mathcal {R}\rhd $
Assume by inductive hypothesis that
$\vDash _{\mathcal {M}}y\in R[x],y:A\rhd _{i}B,y:A,\Gamma \Rightarrow \Delta ,y:\langle ]_{i}B$
. We reason by contradiction. If none of
$\Delta $
and
$x:A\rhd _{i}B$
is valid under this interpretation, then there exists a
$w\in R[\rho (x)]$
such that
$w\Vdash A$
and
$w\not \Vdash \langle ]_{i}B$
. Then we can define a new
$\rho '$
which is identical to
$\rho $
except possibly on y, for which we set
$\rho '(y)=w$
. However, by assumption on validity of the premise of the rule, since
$w\Vdash A$
and
$w\not \Vdash \langle ]_{i}B$
, we have
$w\not \Vdash A\rhd _{i}B$
. It is now straightforward to see that an ascending R-chain can be built on the model, contrary to the assumption that
$\mathcal {M}$
is finite—or, alternatively, Noetherian.
Remark 5. The literature confirms that
$\mathbb {IL}$
is sound and complete with respect to the version of Verbrugge semantics based on the quasi-transitivity condition 6 that we have adopted. Consequently, our system
$\mathsf {G3IL}$
is sound with respect to
$\mathbb {IL}$
. However, we cannot extend this claim to the other axiomatic extensions considered here, as the existing proofs of completeness for those logics specifically address the version of Verbrugge semantics based on condition 2 for quasi-transitivity. Notably, a margin note in [Reference Verbrugge50] indicates that for
$\mathbb {ILKM}1$
, GVS based on condition 6 cannot distinguish this logic from
$\mathbb {ILM}$
.Footnote
28
Thus, a key focus of our future work will be to incorporate the more expressive condition for quasi-transitivity within our framework.
6.3 On termination
Labelled sequent calculi have a peculiar characteristic: From a failed proof search, extracting a countermodel to the sequent at the root of the derivation tree is generally possible. This way, a direct and constructive proof of modal completeness is obtained.Footnote 29
For our family
$\mathsf {G3IL}^{\star }$
, we could claim that the same holds: It is possible to define a Tait–Schütte–Takeuti procedure to construct a refutation of a sequent from a failed proof-search; however, in the present setting, it is essential to define that saturation process along with a terminating strategy for performing a proof search in
$\mathsf {G3IL}^{\star }$
.
The reader familiar with this kind of task will see at once that our systems are rather complex to handle from a combinatorial perspective, and this imposes several cases to check when proving that root-first proof search in
$\mathsf {G3IL}^{\star }$
does terminate.Footnote
30
It is essential to present an equivalent basic proof system for IL, that—following [Reference Negri28, sec. 5]—one might call
$\mathsf {G3KIL}$
. By replacing
$\mathcal {L}\rhd $
with the simplified rule
$\mathcal {L}\rhd ^{S}$
that we used in the proof of Theorem 6.1, we get the basic calculus; extensions are built on top of it, according to the rules in Figure 4.
We are confident that
$\mathsf {G3KIL}$
—as well as its extensions
$\mathsf {G3KIL^{M}}$
and
$\mathsf {G3KIL^{P}}$
—can be shown to satisfy terminating proof search by adapting the proof strategy of Girlando et al. [Reference Girlando, Negri, Olivetti and Risch10] to our much more intricate setting. A complete proof of termination for those systems should be easily extended to the other interpretability logic constituting our uniform family. A further step in difficulty would probably materialise when dealing with the labelled sequent calculus for
$\mathbb {ILP}_{0}$
, since—in order to define the generalised frame condition corresponding to the schema
$\mathsf {P}_{0}$
utilising a geometric rule—we would need further rules for set-theoretic operations on world sets, and thus further cases of interaction between world and neighbourhood labels.
Since, at present, we can only provide an informal argument supporting our claims, in complete earnestness, we prefer to propose the termination of proof search in our family of labelled sequent calculi as the following.
Conjecture 6.4 (Termination).
There exists a strategy making proof search in
$\mathsf {G3KIL}^{\star }$
for a sequent of the form
$\Rightarrow x:A$
always terminate in a finite number of steps. Moreover, it is possible to extract a countermodel to A belonging to the appropriate class of Verbrugge frames from a failed proof search.
7 Conclusions
In the present work, we have introduced a family
$\mathsf {G3IL}^{\star }$
of labelled sequent calculi for interpretability logics based on Verbrugge semantics of [Reference Verbrugge50], which subsumes the standard relational semantics for those modal logics discussed in [Reference de Jongh and Veltman7].
Our systems are modularly obtained from a basic calculus
$\mathsf {G3IL}$
according to the methodology of [Reference Negri and von Plato32, chap. 6] for formalising geometric theories in the
$\mathsf {G3}$
paradigm for sequent calculi. We have proved that all these calculi do satisfy the main desiderata for good
$\mathsf {G3}$
-sequent systems; in particular, we have given a detailed, syntactic proof of the cut-admissibility
$\mathsf {G3IL}^{\star }$
(Theorem 5.8), for which we used a ternary measure of complexity of the cut instance. Our proof is constructive and it thus provides a cut-elimination algorithm for equivalent formulations of these labelled sequent calculi including a cut rule: We have an effective procedure for removing any instance of the cut rule from formal derivations in these (apparently richer) systems which can be, in principle, be implemented in as a proper computer algorithm.Footnote
31
To our knowledge, there are no proof-theoretic treatments of interpretability logics as extensive as the one we have presented here.
What we have discussed in this paper can also be viewed as a case study for exploring the potential of explicit internalization of semantics in sequent calculi. Indeed, it is not immediately clear how to design a sequent system for the logics we have considered using the methodology of implicit internalization. To the best of our knowledge, no attempt has yet been made in the literature to achieve this.
7.1 Related work
The preprint [Reference Hakoniemi and Joosten15] defines a labelled system for IL and some extensions as prefixed tableaux that internalise standard Veltman semantics. Our approach can be viewed as its direct dual—due to the duality between labelled tableaux and labelled sequent calculi—but it differs in its focus on the structural properties of the calculi and is based on GVS. With the adjustments discussed below, this approach allows us to cover a broader range of interpretability principles, notably the system
$\mathbb {ILW}$
based on the de Jongh–Visser schema, which cannot be characterised by a first-order formula in the language of standard Veltman semantics.
On a more traditional note, Sasaki [Reference Sasaki39] presents a Gentzen-style sequent calculus for the basic interpretability logic IL. This work does not consider any extensions, and, as is typical for standard sequent calculi, it is not straightforward to modularly extend the calculus discussed in that paper to encompass additional interpretability logics.Footnote 32
7.2 Future work
In the near future, we would be pleased to resolve Conjecture 6.4 by providing a comprehensive proof of the termination of proof search in our sequent calculi. Settling this conjecture would not merely be a technical achievement; although the decidability of all the interpretability logics under consideration is known, their analysis from the perspective of complexity theory remains a work in progress, as demonstrated by the work of Bou and Joosten [Reference Bou and Joosten6], Mikec et al. [Reference Mikec22] and Mikec [Reference Mikec, Pakhomov and Vuković25].
Nevertheless, as we noted above, even prior to resolving the termination conjecture, it is more crucial to extend our proof systems for interpretability logics to formalise, through labelled sequent calculi, the most expressive version of Verbrugge semantics, based on the quasi-transitivity condition 2 discussed in §4.1. This semantics is undoubtedly capable of distinguishing the interpretability principles explored in the most advanced literature on the topic.Footnote 33
Furthermore, it may be pertinent to apply the labelling technique we have adopted here to provide a constructive proof of modal completeness for interpretability logics. This area is indeed a flourishing research field, and several model-theoretic techniques have been developed in recent years, as summarised by Joosten et al. [Reference Joosten, Rovira, Mikec, Vuković, Bezhanishvili, Iemhoff and Yang17]. Despite progressively achieving a modular character, parts of these proofs remain somewhat obscure and sensitive to the logic under investigation, as they rely on (variations of) Henkin’s method.Footnote 34 A “reverse engineering” approach, relying on the design methodology employed in this work, may prove beneficial in developing alternative modular proofs of completeness and even in addressing some open problems related to model-theoretic matters for specific interpretability principles. In particular, it would be intriguing to test the capabilities of our methodology for proof system design concerning more exotic interpretability principles, such as those in the so-called broad series by Goris and Joosten [Reference Goris and Joosten13], or the subsystems of IL discussed by [Reference Kurahashi and Okawa19].
Finally, from a more applicative perspective, it would be interesting to consider implementations of automated theorem provers for interpretability logics based on the mechanisation of our calculi, following the lines of previous work by [Reference Bilotta, Maggesi, Perini Brogi, Quartini, Porello, Vinci and Zavatteri4, Reference Maggesi, Perini Brogi, Cohen and Kaliszyk20, Reference Maggesi and Perini Brogi21] within a general-purpose proof assistant.
A Appendix: Proofs of syntactic completeness for extensions
We present here the formal derivations of the interpretability principles for the extensions considered in Definition 2.4. For space reasons, we have to omit some components of some sequents in order to make the derivations fit the page layout. Notice thus that the best way to read the following proof trees is root-first, in a bottom-up construction. We highlighted in boldface the formulas in wide sequents closing derivation branches.
A.1
$\mathsf {G3ILM}$
The derivation in
$\mathsf {G3ILM}$
of the schema
$\mathsf {M}$
is given in Figure A1.
Derivation of
$\mathsf {M.}$
A.2
$\mathsf {G3ILP}$
The derivation in
$\mathsf {G3ILP}$
of the schema
$\mathsf {P}$
is given in Figure A2.
Derivation of
$\mathsf {P.}$
A.3
$\mathsf {G3ILM_0}$
The derivation in
$\mathsf {G3ILM_0}$
of the schema
$\mathsf {M_0}$
is given in Figure A3.
Derivation of
$\mathsf {M_0.}$
The derivable sequent S occuring in the derivation has shape
$$ \begin{align*}z\in R[x],z\in R[y],\textbf{z:A},y\in R[x],\ldots\Rightarrow \ldots,\textbf{z:A}.\end{align*} $$
A.4
$\mathsf {G3ILKM1}$
The derivation in
$\mathsf {G3ILKM1}$
of the schema
$\mathsf {KM1}$
is given in Figure A4.
Derivation of
$\mathsf {KM1.}$
A.5
$\mathsf {G3ILW}$
For space reasons, we must omit the derivation of the schema
$\mathsf {W}$
in
$\mathsf {G3ILW}$
since it could not be readable in its rendering on screen. In any case, we invite the reader to check by pencil and paper that the principle characterising that extensions is indeed derivable in the calculus we designed.
Acknowledgements
The authors would like to express our sincere gratitude to the two anonymous reviewers for their valuable feedback and insightful comments, which have significantly enhanced the quality of our paper.
The first author wishes to thank Joost Joosten and Luka Mikec for their invaluable support in analysing the literature on interpretability logics, including access to unpublished manuscripts.
Funding
The first author’s current position is supported the project SERICS—Security and Rights in CyberSpace PE0000014, financed within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S); he also acknowledges the EC-COST Action (CA20111) “EuroProofNet”. The material discussed here is based on Chapter 5 of his PhD thesis [Reference Perini Brogi35], which was supported by a MUR PhD Scholarship (2018-2021).
The second author acknowledges the project “Infinity and Intensionality: Towards A New Synthesis” funded by the Research Council of Norway, and “Modalities in Substructural Logics: Theory, Methods and Applications MOSAIC”, funded by the Community Research and Development Information Service (CORDIS) of the European Commission, the MIUR Excellence Department Project awarded to Dipartimento di Matematica, Università di Genova, CUP D33C23001110001 and the “Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni” (GNSAGA) of the Istituto Nazionale di Alta Matematica (INdAM).
