Proof Theory for Indexed Nested Sequents

Abstract

Fitting’s indexed nested sequents can be used to give deductive systems to modal logics which cannot be captured by pure nested sequents. In this paper we show how the standard cut-elimination procedure for nested sequents can be extended to indexed nested sequents, and we discuss how indexed nested sequents can be used for intuitionistic modal logics.

S. Marin—Supported by ERC Advanced Grant “ProofCert”.

1 Introduction

Modal logics were originally defined in terms of axioms in a Hilbert system, and later in terms of their semantics in relational structures. Structural proof theory for modal logics, however, was considered a difficult topic as traditional (Gentzen) sequents did not provide fully satisfactory (i.e. analytic and modular) proof systems even for some common modal logics. Nonetheless, the proof theory of modal logics has received more attention in the last decades, and some extensions of traditional sequents were successfully proposed to handle modalities. Two approaches can be distinguished: (1) systems that incorporate relational semantics in the formalism itself like labelled sequent systems (e.g., [18, 24, 27]) which use sequents that explicitly refer to the relational semantics: formulas are labelled with states and relational atoms describe the accessibility relation, and (2) systems that use syntactical devices to handle the modalities like nested sequents, which are an extension of ordinary sequents to a structure of tree, first introduced by Kashima [12], and then independently rediscovered by Brünnler [3] and Poggiolesi [21]. They can be translated into a subclass of labelled sequents called in [11] labelled tree sequents, if the relational structure is made explicit. However, compared to labelled deductive systems, the tree structure restricts the expressivity of nested sequents. In particular, it seems that nested sequents cannot give cut-free deductive systems for logics obeying the Scott-Lemmon axioms, which correspond to a “confluence" condition on the relational structure [14].

Fitting recently introduced indexed nested sequents [7], an extension of nested sequents which goes beyond the tree structure to give a cut-free system for the classical modal logic $\mathsf {K}$ extended with an arbitrary set of Scott-Lemmon axioms. In some sense indexed nested sequents are more similar to labelled systems than pure nested sequents—in fact, the translation between nested sequents and labelled tree sequents mentioned above is naturally extended in [23] to a translation between indexed nested sequents and labelled tree sequents with equality, where some nodes of the underlying tree can be identified.

In this paper we investigate some proof-theoretical properties of indexed nested sequents. The first and foremost one is the cut-elimination theorem. As Fitting’s original system does not use a cut rule, this result is actually entailed by his (semantical) completeness theorem. Using the translation mentioned above, one could also use the cut-elimination result for labelled tree sequents with equality, yielding an indirect proof [23]. However, only an internal cut-elimination proof makes a proof formalism a first-class citizen for structural proof theory. For this reason we give in this paper a syntactic proof of cut-elimination carried out within indexed nested sequents. We achieve this by making some subtle but crucial adjustments to the standard cut-elimination proof for pure nested sequents.

One of the main advantages is that this proof can be exported to the intuitionistic framework with basically no effort. We achieve this by using the techniques that had already been successfully used for ordinary nested sequents [8, 15, 26]. This allows us to present the cut-free indexed nested sequents systems in a uniform manner for classical and intuitionistic modal logic. The deductive systems are almost identical, the main difference being that an intuitionistic sequent has only one “output” formula, in the same way as in ordinary sequent calculus an intuitionistic sequent has only one formula on the right.

As there is no straightforward definition of the extension of intuitionistic modal logic with Scott-Lemmon axioms, the indexed nested sequents system can be seen as one way to define it. This point is examined in the last section with a discussion on the various alternatives that exist in the literature and how they relate to the proposed system.

2 Indexed Nested Sequents and the Scott-Lemmon Axioms

We start by working with formulas in negation normal form, generated by the following grammar, which extends the language of propositional classical logic with the two modalities $\Box$ and $\Diamond$

(1)

where a is taken from a countable set of propositional atoms, $\bar{a}$ is its negation, and $\bar{\bar{a}}$ is equivalent to a. For every formula A, its negation $\bar{A}$, is defined as usual via the De Morgan laws. For now, we use $A\supset B$ as abbreviation for $\bar{A}\vee B$.

Classical modal logic $\mathsf {K}$ is obtained from classical propositional logic by adding the axiom $\mathsf {k_{:}}\Box (A \supset B) \supset (\Box A \supset \Box B)$ and the necessitation rule that allows to derive the formula $\Box A$ from any theorem A.

Stronger modal logics can be obtained by adding to $\mathsf {K}$ other axioms. We are interested here specifically in the family of Scott-Lemmon axioms of the form

$$\begin{aligned} \mathsf {g_{k,l,m,n}} :\Diamond ^k \Box ^l A \supset \Box ^m \Diamond ^n A \end{aligned}$$

(2)

for a tuple $\langle k,l,m,n \rangle$ of natural numbers, where $\Box ^m$ stands for m boxes and $\Diamond ^n$ for n diamonds. Fitting [7] introduced indexed nested sequents exactly to provide a structural proof system for classical modal logic $\mathsf {K}$, that could be extended with rules for the Scott-Lemmon axioms.

A (pure) nested sequent is a multiset of formulas and boxed sequents, according to the following grammar where A is a modal formula. We understand such a nested sequent through its interpretation as a modal formula, written $fm(\cdot )$, given inductively by $fm(\emptyset ) = \bot$; $fm(A, \varGamma ) = A \vee fm(\varGamma )$; and $fm([\varGamma _1], \varGamma _2) = \Box fm(\varGamma _1) \vee fm(\varGamma _2)$. A nested sequent can therefore be seen as a tree of ordinary one-sided sequents, with each node representing the scope of a modal $\square$. It therefore is of the general form

$$\begin{aligned} A_1,\ldots ,A_k, [\varGamma _1],\ldots ,[\varGamma _n] \end{aligned}$$

(3)

An indexed nested sequent, as defined in [7], is a nested sequent where each sequent node (either the root or any interior node) carries an index, denoted by lowercase letters like $u,v,w,x,\ldots$, and taken from a countable set (e.g., for simplicity, the set of natural numbers), so we write an indexed sequent by extending (3) in the following way

(4)

where $\varGamma _1$, ..., $\varGamma _n$ are now indexed sequents, and where the index of the root is not explicitly shown (e.g., we can assume that it is 0). For an indexed nested sequent $\varSigma$, we write $I_{\varSigma }$ to denote the set of indexes occurring in $\varSigma$.

Intuitively, indexed nested sequents are no longer trees, but any kind of rooted directed graphs, by identifying nodes carrying the same index.

In nested sequent calculi, a rule can be applied at any depth in the structure, that is, inside a certain nested sequent context. We write for an n-ary context (i.e. one with n occurrences of the $\{\;\}$) where $i_1,\ldots ,i_n$ are the indexes of the sequent nodes that contain the $\{\;\}$, in the order of their appearance in the sequent. A hole in a context can be replaced by a formula or sequent. More precisely, we write for the sequent that is obtained from by replacing the k-th hole by $\varDelta _k$, for each $k\in \{1,\ldots ,n\}$ (if $\varDelta _k = \emptyset$ it simply amounts to removing the $\{\;\}$). We might omit the index at the context-braces when this information is clear or not relevant.

Example 2.1

For example, is a ternary context that we can write as . If we substitute the sequents ; $\varDelta _2 = F$; and into its holes, we get: .

In Fig. 1, the classical system that we call $\mathsf {iNK}$ is an adaptation of the system described by Fitting in [7] to our notations and to the one-sided setting. It can also be seen as Brünnler’s system [3] extended with indexes.

What is different from the pure nested sequent system is the addition of the two structural rules $\mathsf {tp}$ and $\mathsf {bc}$, called teleportation and bracket-copy, respectively, which are variants of the formula-contraction $\mathsf {FC}$ and the sequent-contraction $\mathsf {SC}$ of [7]. We need two versions of $\mathsf {bc}$ to take care of every possible context where the rule may be applied. Another peculiarity is that in the rules for $\Box$ we demand that the index of the new bracket in the premiss does not occur in the conclusion.

Fig. 1.

System $\mathsf {iNK}$

Fig. 2.

Inference rule $\mathsf {g_{k,l,m,n}}$ (where $l+n \not = 0$, $v_1 \ldots v_k$ and $x_1 \ldots x_n$ are fresh, and $v_l=x_n$)

Fig. 3.

Special case for $\mathsf {g_{k,0,m,0}}$

Finally, for a tuple $\langle k,l,m,n \rangle$ with $l+n\not =0$, the rule $\mathsf {g_{k,l,m,n}}$ in Fig. 2 is defined as in [7]. It must satisfy that $v_1 \ldots v_k$ and $x_1 \ldots x_n$ are fresh indexes which are pairwise distinct, except for the confluence condition: we always have $v_l = x_n$. When one or more elements of the tuple $\langle k,l,m,n \rangle$ are equal to 0, then we have the following special cases:

• if $k = 0$ (or $m=0$) then $u_1$ to $u_k$ (resp. $w_1$ to $w_m$) all collapse to $u_0$.

• if $l = 0$ then $w_1$ to $w_l$ all collapse to $u_k$, and similarly, if $n = 0$ then $x_1$ to $x_n$ all collapse to $v_m$. In particular, if $k=0$ and $l=0$, we must have $x_n=u_0$, and similarly, if $m=0$ and $n=0$, we demand that $v_l=u_0$.

An example of how this rule can be used to derive an instance of the Scott-Lemmon axioms can be found in the proof of Theorem 4.2.

The case where $l=0$ and $n=0$ was not handled by Fitting in [7]; we give a corresponding rule in Fig. 3. In that case, not only do we identify $u_k$ and $w_m$, but it is also necessary to apply a substitution $\sigma :I_{\varGamma }\rightarrow I_{\varGamma }$ to the indexes in the context , giving the new context , such that $\sigma (u_k) = \sigma (w_m)$ in the whole sequent (and $\sigma (y) = y$ for any other $y \in I_{\varGamma }$).

For a given set $\mathsf G\subseteq \mathbb {N}^4$, write $\mathsf {iNK}+\mathsf G$ for the system obtained from $\mathsf {iNK}$ by adding the corresponding rules given in Figs. 2 and 3. System $\mathsf {iNK}+\mathsf G$ is sound and complete wrt. the logic corresponding $\mathsf {K}+ \mathsf G$ (which is obtained from $\mathsf {K}$ by adding the corresponding axioms (2)). Soundness is proven by Fitting [7] wrt. relational frames; and completeness via a translation to set-prefixed tableaux system for which in turn he gives a semantic completeness proof.

3 Cut-Elimination

In this section, we present a cut-elimination proof for the indexed nested sequent system $\mathsf {iNK}+\mathsf G$ that relies on a standard double-induction on the height of the derivation above a given cut-rule (left of Fig. 4), and the cut rank.

Fig. 4.

Left: the one-sided cut-rule – Right: additional structural rules

Definition 3.1

The height of a derivation tree $\pi$, denoted by $\mathsf {ht}(\pi )$, is the length of the longest path in the tree from its root to one of its leaves. The rank of an instance of $\mathsf {cut}$ is the depth of the formula introduced by the cut. We also write $\mathsf {cut}_r$ to denote an instance of $\mathsf {cut}$ with rank at most r. The cut-rank of a derivation $\pi$, denoted by $\mathsf {rk}(\pi )$, is the maximal rank of a $\mathsf {cut}$ in $\pi$.

To facilitate the overall argument, we consider a variant of system $\mathsf {iNK}$, that we call system $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}$, that is obtained from $\mathsf {iNK}$ by removing the teleportation rule $\mathsf {tp}$ (but keeping the $\mathsf {bc}$-rules), and by replacing the $\mathsf {id}$- and $\Diamond$-rules by

respectively. The reason behind this is that $\mathsf {iNK}$ and $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}$ are equivalent (with and without cut, as shown below in Lemma 3.4), but the $\mathsf {tp}$-rule is admissible in the new system. We will also need some additional structural rules called weakening, contraction, necessitation, and index substitution respectively, which are shown on the right in Fig. 4. The rules for weakening and contraction are similar to the standard sequent rules except that they can apply deeply inside a context. The rules $\mathsf {nec}$ and $\mathsf {isub}$ on the other hand cannot be applied deep inside a context; they always work on the whole sequent. In $\mathsf {isub}$, the sequent $\sigma \varGamma$ is obtained from $\varGamma$ by applying the substitution $\sigma :I_{\varGamma }\rightarrow I_{\varGamma }$ on the indexes occurring in $\varGamma$, where $\sigma$ can be an arbitrary renaming.

Lemma 3.2

The rules $\mathsf {nec}$, $\mathsf {w}$, $\mathsf {isub}$ and $\mathsf {c}$ are cut-rank and height preserving admissible for $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$, and all rules of $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ (except for the axiom ) are cut-rank and height-preserving invertible.

Proof

This proof is analogous to that for the pure nested sequent systems in [3]. For $\mathsf {bc}$ and $\mathsf {g_{k,l,m,n}}$, note that their inverses are just weakenings.    $\square$

Lemma 3.3

The rule $\mathsf {tp}$ is admissible for $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ (and for $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G+ \mathsf {cut}$).

Proof

The proof uses an induction on the number of instances of $\mathsf {tp}$ in a proof, eliminating topmost instances first, by an induction on the height of the proof above it and a case analysis of the rule $\mathsf {r}$ applied just before $\mathsf {tp}$. The only nontrivial case is when $\mathsf {r}= \Box$:

we transform the derivation as follows and then use the admissibility of weakening (Lemma 3.2) and the induction hypothesis to conclude.    $\square$

Lemma 3.4

A sequent $\varDelta$ is provable in $\mathsf {iNK}+\mathsf G$ (or in $\mathsf {iNK}+\mathsf G+ \mathsf {cut}$) if and only if it is provable in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ (resp. in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G+ \mathsf {cut}$).

Proof

Given a proof of $\varDelta$ in $\mathsf {iNK}+\mathsf G$, we can observe that the rules $\mathsf {id}$ and ${\Diamond }$ are just special cases of the rules and , respectively. Thus, we obtain a proof of $\varDelta$ in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ from admissibility of $\mathsf {tp}$ (Lemma 3.3). Conversely, if we have a proof of $\varDelta$ in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$, we can obtain a proof of $\varDelta$ in $\mathsf {iNK}+\mathsf G$ by replacing all instance of and by the following derivations:

respectively. The same proof goes for the system with $\mathsf {cut}$.    $\square$

Finally we can prove the reduction lemma.

Lemma 3.5

(Reduction Lemma). If there is a proof $\pi$ of shape

in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ such that $\mathsf {rk}(\pi _1)\le r$ and $\mathsf {rk}(\pi _2)\le r$, then there is proof $\pi '$ of $\varGamma \{\emptyset \}$ in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$ such that $\mathsf {rk}(\pi ')\le r$.

Proof

We proceed by induction on $\mathsf {ht}(\pi _1)+\mathsf {ht}(\pi _2)$, making a case analysis on the bottommost rules in $\pi _1$ and $\pi _2$. The cases are almost identical to [3]; we only show the ones that are new or different. Details can be found in [16]. As an example of commutative case, we consider when the bottommost rule $\mathsf {r}$ of $\pi _1$ (or $\pi _2$) is $\mathsf {g_{k,0,m,0}}$. Then we have

which can be replaced by

where $\varGamma _{k-1}\{\}$ and $\varGamma _{m-1}\{\}$ correspond to contexts which are of the form and respectively, and we can proceed by induction hypothesis.

The most interesting key case is when the cut-formula $A=\Diamond B$, that is, when when the bottommost rule $\mathsf {r}$ of $\pi _1$ is :

which can be reduced to

where on the left branch we use height-preserving admissibility of weakening and proceed by induction hypothesis, and on the right branch we use admissibility of the $\mathsf {isub}$- and $\mathsf {tp}$-rules (Lemmas 3.2 and 3.3).    $\square$

Theorem 3.6

If a sequent $\varGamma$ is derivable in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G+ \mathsf {cut}$ then it is also derivable in $\mathsf {i}\ddot{\mathsf {N}}\mathsf {K}+\mathsf G$.

Proof

The proof goes by induction on the cut rank of $\pi$; the induction step uses also an induction on the number of occurrences of $\mathsf {cut}$ with the maximal rank and Lemma 3.5 to eliminate each time the topmost occurrence in the proof.    $\square$

Theorem 3.7

If a sequent $\varGamma$ is derivable in $\mathsf {iNK}+\mathsf G+ \mathsf {cut}$ then it is also derivable in $\mathsf {iNK}+\mathsf G$.

Proof

Following Theorem 3.6 and Lemma 3.4.    $\square$

4 From Classical to Intuitionistic

Starting from the proof system for classical modal logic discussed in the previous section, we will show now how to obtain an intuitionistic variant. This will be done in a similar way as Gentzen did in his original work for the ordinary sequent calculus [9].

The first step is to enrich the language of formulas with implication and disallow negation on atoms, i.e., we no longer restrict formulas to negative normal form:

(6)

We can define $\lnot A=A\supset \bot$ and $\top =\lnot \bot$. Intuitionistic modal logic $\mathsf {IK}$ is obtained from intuitionistic propositional logic by adding the axioms

$$\begin{aligned} \begin{array}{r@{\;}l} \mathsf {k_{1}}:&{}\Box (A\supset B)\supset (\Box A\supset \Box B)\\ \mathsf {k_{2}}:&{}\Box (A\supset B)\supset (\Diamond A\supset \Diamond B) \end{array} \qquad \begin{array}{r@{\;}l} \mathsf {k_{3}}:&{}\Diamond (A\vee B)\supset (\Diamond A\vee \Diamond B)\\ \mathsf {k_{4}}:&{}(\Diamond A\supset \Box B)\supset \Box (A\supset B)\\ \mathsf {k_{5}}:&{}\Diamond \bot \supset \bot \end{array} \quad \end{aligned}$$

(7)

and the rule $\mathsf {nec}$, similarly to Sect. 2. The axioms in (7) are logical consequences of $\mathsf {k}$ in the classical case but not in the intuitionistic case.¹

We will consider the following schema as the intuitionistic equivalent to Scott-Lemmon axioms:

$$\begin{aligned} \mathsf {g_{k,l,m,n}} :(\Diamond ^k\Box ^l A \supset \Box ^m\Diamond ^n A) \wedge (\Diamond ^m\Box ^n A \supset \Box ^k\Diamond ^l A) \end{aligned}$$

(8)

The two conjuncts correspond to the classical $\mathsf {g_{k,l,m,n}}$ and $\mathsf {g_{m,n,k,l}}$ which are equivalent via De Morgan in classical logic, but not in intuitionistic modal logic.

In the following, we will first present a two-sided version of the classical one-sided system $\mathsf {iNK}$ that was given in Fig. 1. For this, the first step is to include the distinction between input and output formulas into the data structure. To that purpose we use here the notion of polarity, as studied by Lamarche in [13]. We assign to every formula in the nested sequent a unique polarity: either input, denoted by a $\bullet$-superscript, or output, denoted by a $\circ$-superscript. A two-sided indexed nested sequent therefore is of the following form, denoted by $\varGamma ^\circ$ if it contains at least one input formula and by $\varLambda ^\bullet$ otherwise:

(9)

We are now ready to see the inference rules. The two-sided version of $\mathsf {iNK_2}$ is shown in Fig. 5. As expected, the rules for output formulas are the same as in the one-sided case, and the rules for input formulas show dual behavior.

Fig. 5.

Two-sided classical system $\mathsf {iNK_2}$

Finally, the step from classical to intuitionistic simply consists in restricting the number of output formulas in the sequent to one, but it is crucial to observe that we count the whole sequent, and not every bracket separately [26]. So an intuitionistic indexed nested sequent is of the form:

(10)

where $\varLambda ^\bullet$ is defined as in (9). Moreover, since we do not have an explicit contraction rule, but have it incorporated into inference rules (e.g., $\Box ^\bullet$), the inference rules $\vee ^\circ$, $\supset ^\bullet$ and $\Diamond ^\circ$ have to adapted, as shown on Fig. 6, in order to maintain the property that each sequent in a proof contains exactly one output formula. In particular, to ensure that both premisses of the $\supset ^\bullet$-rule are intuitionistic sequents, the notation ${\varGamma ^{\downarrow }}\{\}$ stands for the context obtained from $\varGamma \{\}$ by removing the output formula. We define $\mathsf {iNIK}=\mathsf {iNK_2}\setminus \{\supset ^\bullet ,\vee ^\circ _c,\Diamond ^\circ _c\}\cup \{\supset ^\bullet _i,\vee ^\circ _{1},\vee ^\circ _{2},\Diamond ^\circ _i\}$. Observe that the structural rules $\mathsf {tp}$, $\mathsf {bc}_1$, and $\mathsf {bc}_2$ are identical for all three systems (one-sided classical, two-sided classical, and two-sided intuitionistic).

Fig. 6.

Intuitionistic variants of some rules for system $\mathsf {iNIK}$

It is also the case that each system can be extended with the rules presented in Figs. 2 and 3. In the classical case, it will give the system $\mathsf {iNK_2}+\mathsf G$ equivalent to $\mathsf {iNK}+\mathsf G$ and basically identical to Fitting’s system [7]. In the intuitionistic case, it gives us a system $\mathsf {iNIK}+\mathsf G$, and the rest of the paper is dedicated to the study of this system. This modular way of adding structural rules for the Scott-Lemmon axioms to the basic deductive system corresponding to $\mathsf {K}$ or $\mathsf {IK}$ is similar to the way labelled sequent systems handle the Scott-Lemmon axioms.²

Finally, the cut-elimination proof conducted in $\mathsf {iNK}+\mathsf G$ can be reproduced in a similar fashion in $\mathsf {iNK_2}+\mathsf G$ and $\mathsf {iNIK}+\mathsf G$, the two-sided cut-rule being of the form in the classical case, and in the intuitionistic case, where a unique output needs to be maintained in the left branch.

Theorem 4.1

If a sequent $\varGamma$ is derivable in $\mathsf {iNK_2}+\mathsf G+ \mathsf {cut}_c$ (resp. $\mathsf {iNIK}+\mathsf G+ \mathsf {cut}_i$) then it is also derivable in $\mathsf {iNK_2}+\mathsf G$ (resp. $\mathsf {iNIK}+\mathsf G$).

Proof

The proof works similarly to the one of Theorem 3.7. For the intuitionistic system, the cases are similar to [26], except for the specific indexed ones. Details can be found in [16].    $\square$

The cut-elimination theorem can be used to show completeness: every theorem of $\mathsf {K}+ \mathsf {G}$ (resp. $\mathsf {IK}+ \mathsf {G}$) is a theorem of $\mathsf {iNK_2}+\mathsf G$ (resp. $\mathsf {iNIK}+\mathsf G$).

Theorem 4.2

If a formula A is provable in the Hilbert system $\mathsf {IK}+\mathsf {G}$, then the sequent $A^\circ$ is provable in the indexed nested sequent system $\mathsf {iNIK}+\mathsf G$.

Proof

The axioms of intuitionistic propositional logic as well as the axioms $\mathsf {k_{1}}$-$\mathsf {k_{5}}$ can be derived in $\mathsf {iNIK}$, in the same way as in [26]. The inference rule $\mathsf {nec}$ can be simulated by the structural rule $\mathsf {nec}$, which is admissible in $\mathsf {iNIK}+\mathsf G$ (Lemma 3.2), and modus ponens $\mathsf {mp}$ can be simulated by the $\mathsf {cut}$-rule, which is also admissible (Theorem 4.1). Thus, it remains to show that any $\mathsf {g_{k,l,m,n}}$ axiom can be derived, using the corresponding $\mathsf {g_{k,l,m,n}}$-rule (which is the same as $\mathsf {g_{m,n,k,l}}$):

And similarly for the other conjunct.    $\square$

The same proof can be done in the classical case, and provides an alternative to the completeness of indexed nested sequents wrt. set prefixed tableaux in [7].

However, there are examples of theorems of $\mathsf {iNIK}+\mathsf G$ that are not theorems of $\mathsf {IK}+ \mathsf {G}$, that is, the indexed nested sequent system is not sound with respect to the Hilbert axiomatisation using what we gave above as the intuitionistic alternative to Scott-Lemmon axioms. There is already a simple counter-example when one considers $\mathsf {G}$ to be composed with only the axiom $\mathsf {g_{1,1,1,1}} : \Diamond \Box A \supset \Box \Diamond A$. Then

$$\begin{aligned} F = (\Diamond (\Box (a \vee b) \wedge \Diamond a) \wedge \Diamond (\Box (a \vee b) \wedge \Diamond b)) \supset \Diamond (\Diamond a \wedge \Diamond b) \end{aligned}$$

(11)

is derivable in $\mathsf {iNIK}+ \mathsf {g_{1,1,1,1}}$, but is not a theorem of $\mathsf {IK}+ \mathsf {g_{1,1,1,1}}$ (as mentioned in [25]). Thus, the logic given by the Hilbert axiomatisation $\mathsf {IK}+ \mathsf G$ and the one given by the indexed nested sequent system $\mathsf {iNIK}+\mathsf G$ actually differ in the intuitionistic case. We will address this issue in more detail in the next section.

5 Semantics of the Scott-Lemmon Axioms

In the classical case, the indexed nested sequent system is not only equivalent to the Hilbert axiomatisation using Scott-Lemmon axioms, it is actually sound and complete wrt. the corresponding Kripke semantics. In this section, we investigate the behavior of the indexed nested sequents system $\mathsf {iNIK}+\mathsf G$ with respect to Kripke semantics. For this, we briefly recall the standard Kripke semantics of classical and intuitionistic modal logics. The classical semantics is standard, but the intuitionistic might be less well-known. We use here the birelational models, as they are discussed in [4, 20, 25].

A classical frame $\langle W,R \rangle$ is a non-empty set W of worlds and a binary relation $R\subseteq W\times W$, called the accessibility relation. An intuitionistic frame $\langle W,R,\le \rangle$ is additionally equipped with a preorder $\le$ on W, such that:

 

(F1):

For all $u, v, v' \in W$, if uRv and $v \le v'$, there exists $u' \in W$ such that $u \le u'$ and $u' R v'$.

(F2):

For all $u', u, v \in W$, if $u \le u'$ and uRv, there exists $v' \in W$ such that $u' R v'$ and $v \le v'$.

A classical model $\mathcal M= \langle W,R,V \rangle$ is a classical frame together with a valuation function $V:W\rightarrow 2^\mathcal A$ mapping each world w to the set of propositional variables which are true in w. In an intuitionistic model $\langle W,R,\le ,V \rangle$, the function V must be monotone with respect to $\le$, i.e. $w\le v$ implies $V(w)\subseteq V(v)$.

We write $w\Vdash a$ if $a\in V(w)$. From there, the relation $\Vdash$ is extended to all formulas in a parallel way in the classical and intuitionistic case, that is, considering a classical model to be a special case of an intuitionistic model, where $w\le v$ iff $w=v$, we give below the definition for both at the same time:

$$\begin{aligned} \begin{array}{ll} w\Vdash A\wedge B &{}\qquad \text {iff}\quad w\Vdash A \text { and } w\Vdash B\\ w\Vdash A\vee B &{}\qquad \text {iff}\quad w\Vdash A \text { or } w\Vdash B\\ w\Vdash A\supset B &{}\qquad \text {iff}\quad \text {for all } w' \text { with } w\le w', \text { if }w'\Vdash A \text { then also } w'\Vdash B\\ w\Vdash \Box A &{}\qquad \text {iff}\quad \text {for all } w' \text { and } u \text { with } w\le w' \text { and } w'Ru, \text { we have } u\Vdash A\\ w\Vdash \Diamond A &{}\qquad \text {iff}\quad \text {there is a } u\in W \text { such that } wRu \text { and } u\Vdash A\\ \end{array} \end{aligned}$$

If $w\Vdash A$ we say that w forces A. We write $w\nVdash A$ if w does not force A, i.e. it is not the case that $w\Vdash A$. It follows that $\Vdash$ also satisfies monotonicity, i.e. if $w\le v$ and $w\Vdash A$ then $v\Vdash A$. (In the classical case we also have $w\Vdash \lnot A$ iff $w\nVdash A$ which implies the de Morgan dualities, in particular, $w\Vdash \Box (\lnot A)$ iff $w\Vdash \lnot (\Diamond A)$.) We say that a formula A is valid in a model $\mathcal M$, if for all $w\in W$ we have $w\Vdash A$. Finally, we say a formula is classically (or intuitionistically) valid, if it is valid in all classical (resp. intuitionistic) models.

The Hilbert systems for $\mathsf {K}$ and $\mathsf {IK}$, introduced in Sects. 2 and 4 respectively, are sound and complete with respect to arbitrary classical and intuitionistic models respectively. We are now going to adapt the method of Fitting [7] for proving the soundness of the classical system $\mathsf {iNK_2}+\mathsf G$ to study the soundness of our proposed intuitionistic system $\mathsf {iNIK}+\mathsf G$ with respect to a subclass of intuitionistic models. The first step is to put intuitionistic indexed nested sequent in correspondence with intuitionistic models in order to define the validity of a sequent in a model.

Definition 5.1

Let $\varSigma$ be an indexed nested sequent. We write $I_{\varSigma }$ to denote the set of indexes occurring in $\varSigma$, and we write $R_{\varSigma }$ for the accessibility relation induced by $\varSigma$, that is, the binary relation $R_{\varSigma }\subseteq I_{\varSigma }\times I_{\varSigma }$ defined as: $wR_{\varSigma }v$ iff for some $\varGamma \{\;\}$ and $\varDelta$, i.e. v is the index of a child of w.

Example 5.2

If we consider the sequent $\varSigma$ obtained in the Example 2.1, we have that $I_{\varSigma } = \{0,1,2,3,4,5\}$ with 0 being the index of the root, so $R_{\varSigma }= \{(0,1), (0,2), (0,3), (1,2), (2,4), (2,5), (3,1)\}.$

Definition 5.3

Let $\varSigma$ be an indexed nested sequent and let $\mathcal M= \langle W,R,\le ,V \rangle$ be an intuitionistic Kripke model. A homomorphism $h:\varSigma \rightarrow \mathcal M$ is a mapping $h:I_{\varSigma }\rightarrow W$, such that $wR_{\varSigma }v$ implies h(w)Rh(v) for all $w,v\in I_{\varSigma }$.

A preorder relation between homomorphisms can be obtained from the preorder in an intuitionistic model: For $h,h':\varSigma \rightarrow \mathcal M$ two homomorphisms, we write $h\le h'$ if $h(w)\le h'(w)$ in $\mathcal M$ for all $w\in I_{\varSigma }$. The notion of validity can then be defined by induction on the subsequents of a given sequent.

Definition 5.4

Let $\varSigma$ and $\varDelta$ be indexed nested sequents, and $w\in I_{\varSigma }$. We say that $\langle \varDelta ,w \rangle$ is an exhaustive subsequent of $\varSigma$ if either $\varDelta =\varSigma$ and $w=0$, or for some context $\varGamma \{\;\}$.

Note that for a given index v of $\varSigma$, there might be more than one $\varDelta$ such that $\langle \varDelta ,v \rangle$ is an exhaustive subsequent of $\varSigma$, simply because v occurs more than once in $\varSigma$. For this reason we will write $\dot{v}$ to denote a particular occurrence of v in $\varSigma$ and $\varSigma |_{\dot{v}}$ for the subsequent of $\varSigma$ rooted at the node $\dot{v}$. $\langle \varSigma |_{\dot{v}},v \rangle$ stands then for a uniquely defined exhaustive subsequent of $\varSigma$.

Definition 5.5

Let $h:\varSigma \rightarrow \mathcal M$ be a homomorphism from a sequent $\varSigma$ to a model $\mathcal M$. Let $w\in I_{\varSigma }$ and let $\langle \varDelta ,w \rangle$ be an exhaustive subsequent of $\varSigma$. From (9) and (10), $\varDelta$ has one of the following forms:

• . Then we define $\langle h,w\rangle \Vdash _{\mathsf {i}}\varDelta$ if $h(w)\nVdash B_i$ for some $i\le l$ or $\langle h,v_j\rangle \Vdash _{\mathsf {i}}\varLambda _j^\bullet$ for some $j\le n$.

• . Then we define $\langle h,w\rangle \Vdash _{\mathsf {i}}\varDelta$ if either $h(w)\nVdash B_i$ for some $i\le l$ or $\langle h,v_j\rangle \Vdash _{\mathsf {i}}\varLambda _j^\bullet$ for some $j\le n$ or $h(w)\Vdash A$.

• . Then we define $\langle h,w\rangle \Vdash _{\mathsf {i}}\varDelta$ if either $h(w)\nVdash B_i$ for some $i\le l$ or $\langle h,v_j\rangle \Vdash _{\mathsf {i}}\varLambda _j^\bullet$ for some $j\le n$ or for all homomorphisms $h'\ge h$, we have that $\langle h',u\rangle \Vdash _{\mathsf {i}}\varPi ^\circ$.

If, for all $h'\ge h$, $\langle h',w\rangle \Vdash _{\mathsf {i}}\varDelta$, we say that $\langle \varDelta ,w \rangle$ is intuitionistically valid in $\mathcal M$ under h. Then, a sequent $\varSigma$ is valid in a model $\mathcal M$, if $\langle \varSigma ,0 \rangle$ is valid in $\mathcal M$ under every $h:\varSigma \rightarrow \mathcal M$.

Informally, an indexed nested sequent is valid if it contains anywhere in the sequent tree a valid output formula or an invalid input formula. More formally:

Lemma 5.6

Let $\varSigma$ be an indexed nested sequent. Let $\langle \varDelta ,v \rangle$ be a exhaustive subsequent of $\varSigma$. Suppose for some context and some formula A. Let $\mathcal M$ be a Kripke model and $h :\varSigma \rightarrow \mathcal {M}$ a homomorphism.

• If $A = A^\circ$ and $h(w)\Vdash A$, then $\langle h,v\rangle \Vdash _{\mathsf {i}}\varDelta$.

• If $A = A^\bullet$ and $h(w)\nVdash A$, then $\langle h,v\rangle \Vdash _{\mathsf {i}}\varDelta$.

Proof

By induction on the height of the tree rooted at the considered occurrence of v. The base case occurs when $A^\circ$ (or $A^\bullet$) is at the root of that tree.    $\square$

We now make explicit the class of model that we are going to consider in order to interpret system $\mathsf {iNIK}+\mathsf G$. We adapt the notion of graph-consistency introduced by Simpson [25] to the indexed nested sequents framework.

Definition 5.7

A intuitionistic model $\mathcal M$ is called graph-consistent if for any indexed nested sequent $\varGamma$, given any homomorphism $h:\varGamma \rightarrow \mathcal M$, any $w \in I_{\varGamma }$, and any $w' \ge h(w)$, there exists $h' \ge h$ such that $h'(w) = w'$.³

Definition 5.8

Let $\mathcal M=\langle W,R,\le ,V \rangle$ be a be an intuitionistic model and let $\langle k,l,m,n \rangle \in \mathbb {N}^4$. We say that $\mathcal M$ is a $\mathsf {g}(k,l,m,n)$ -model if for all $w,u,v\in W$ with $wR^ku$ and $wR^mv$ there is a $z\in W$ such that $uR^lz$ and $vR^nz$.⁴ For a set $\mathsf G$ of $\mathbb {N}^4$-tuples, we say that $\mathcal M$ is a $\mathsf G$ -model, if for all $\langle k,l,m,n \rangle \in \mathsf G$ we have that $\mathcal M$ is a $\mathsf {g}(k,l,m,n)$-model.

We finally prove that any theorem of $\mathsf {iNIK}+\mathsf G$ is valid in every graph-consistent $\mathsf G$-model by showing that each rule of $\mathsf {iNIK}+\mathsf G$ is sound when interpreted in these models.

Lemma 5.9

Let $\mathsf G\subseteq \mathbb {N}^4$, and let be an instance of an inference rule in $\mathsf {iNIK}+\mathsf G$ for $n=0,1,2$. If all of $\varSigma _1$, ..., $\varSigma _n$ are valid in every graph-consistent $\mathsf G$-model, then so is $\varSigma$.

Proof

First, assume that $\mathsf {r}$ is , for some $\langle k,l,m,n \rangle \in \mathsf G$ such that $k,l,m,n>0$ (similar proof when one parameter is 0). By way of contradiction, suppose that $\varPhi$ is valid in every graph-consistent $\mathsf G$-model and that there is a $\mathsf G$-model $\mathcal M= \langle W,R, \le ,V \rangle$, a homomorphism $h:\varPsi \rightarrow \mathcal M$ such that $\langle \varPsi ,0 \rangle$ is not valid in $\mathcal M$ under h. Recall that $\varPsi$ is of form

Therefore, there exist $\mathtt u_0,\mathtt u_k ,\mathtt w_m$ in $W$ such that $\mathtt u_0 = h(u_0)$, $\mathtt u_k = h(u_k)$, $\mathtt w_m = h(w_m)$, and $\mathtt u_0 R^k\mathtt u_k$, and $\mathtt u_0 R^m\mathtt w_m$ (Definitions 5.1 and 5.3). Hence, as $\mathcal M$ is in particular a $\mathsf {g}(k,l,m,n)$-model, there exists $\mathtt y\in W$ with $\mathtt u_k R^l \mathtt y$ and $\mathtt w_m R^n\mathtt y$ (Definition 5.8). Namely, there are worlds $\mathtt v_1,\ldots ,\mathtt v_l, \mathtt x_1,\ldots ,\mathtt x_n$ in $W$ such that $\mathtt u_k R\mathtt v_1\ldots \mathtt v_{l-1} R\mathtt v_l$, $\mathtt w_m R\mathtt x_1\ldots \mathtt x_{n-1} R\mathtt x_n$, and $\mathtt v_l=\mathtt y=\mathtt x_n$. By noting that

we can define a homomorphism $h':\varPhi \rightarrow \mathcal M$ with $h'(z)=h(z)$ for all $z\in I_{\varPsi }$, $h'(v_i)=\mathtt v_i$ for $1\le i\le l$ and $h'(x_j)=\mathtt x_j$ for $1\le j\le n$.

We are now going to show that for every $h:\varPsi \rightarrow \mathcal M$, and every occurrence $\dot{z}$ of an index $z\in I_{\varPsi }$, we have $\langle h,z\rangle \Vdash _{\mathsf {i}}\varPsi |_{\dot{z}}$ iff $\langle h',z\rangle \Vdash _{\mathsf {i}}\varPhi |_{\dot{z}}$. We proceed by induction on the height of the tree rooted at $\dot{z}$.

• 1. The node of $\dot{z}$ is a leaf node of $\varPsi$, and $z\ne u_k$ and $z\ne w_m$. Then we have $\varPsi |_{\dot{z}}=\varPhi |_{\dot{z}}$ and the claim holds trivially.

• 2. The node of $\dot{z}$ is an inner node of $\varPsi$, and $z\ne u_k$ and $z\ne w_m$. By the induction hypothesis, for every $t\in I_{\varPsi }$ with $z R_\varPsi t$, every occurrence $\dot{t}$ of t in $\varPsi |_{\dot{z}}$, and every $h:\varPsi \rightarrow \mathcal M$, $\langle h,t\rangle \Vdash _{\mathsf {i}}\varPsi |_{\dot{t}}$ iff $\langle h',t\rangle \Vdash _{\mathsf {i}}\varPhi |_{\dot{t}}$. The statement follows then by unravelling the definition of $\Vdash _{\mathsf {i}}$ (Definition 5.5).

• 3. $z=u_k$. For any occurrence $\dot{z}$ in the context , the proof is similar to one of the previous cases. Otherwise, we know that $\varPsi |_{\dot{z}} =\varDelta _k$ and . Furthermore, for all $i\le l$ and $h''\ge h$ we have , and therefore $\langle h,z\rangle \Vdash _{\mathsf {i}}\varPsi |_{\dot{z}}$ iff $\langle h',z\rangle \Vdash _{\mathsf {i}}\varPhi |_{\dot{z}}$.

• 4. $v=w_m$. This case is similar to the previous one.

Since we assumed that $\langle \varPsi ,0 \rangle$ is not valid in $\mathcal M$ under h, we can conclude that $\langle \varPhi ,0 \rangle$ is not valid in $\mathcal M$ under $h'$, contradicting the validity of $\varPhi$.

The proof for $\mathsf {bc}$, $\mathsf {tp}$, and the other cases of $\mathsf {g_{k,l,m,n}}$ is similar.

For the logical rules, we will only consider in detail the case for $\Box ^\circ$, the others being similar. Suppose that is valid in every graph-consistent $\mathsf G$-model. For , suppose that there exists a graph-consistent $\mathsf G$-model $\mathcal M= \langle W, R, \le , V \rangle$ and a homomorphism $h :\varPsi \mapsto \mathcal M$ such that $\langle \varPsi ,0 \rangle$ is not valid in $\mathcal M$ under h. Therefore, there exists $h' \ge h$ such that $\langle h',0\rangle \nVdash _{\mathsf {i}}\varPsi$, in particular by Lemma 5.6, $h'(w)\nVdash \Box A$. So there exists $\mathtt {w}$ and $\mathtt {v}$ such that $\mathtt {w}R\mathtt {v}$, $h'(w) \le \mathtt {w}$ and $\mathtt {v}\nVdash A$. As $\mathcal M$ is graph-consistent, there exists $h''$ such that $\mathtt {w} = h''(w)$. Thus, we can extend $h''$ by setting $h''(v) = \mathtt {v}$ to obtain a homomorphism $h'' :\varPhi \mapsto \mathcal M$, indeed $\varPhi$ and $\varPsi$ have the same set of indexes related by the same underlying structure, but for the fresh index v that does not appear in $\varPsi$. Finally, as $h''(v)\nVdash A$, we have by Lemma 5.6 that $\langle \varPhi , 0 \rangle$ is not valid in $\mathcal M$ under $h''$ which contradicts the assumption of validity of $\varPhi$.   $\square$

Theorem 5.10

Let $\mathsf G$ be given. If a sequent $\varSigma$ is provable in $\mathsf {iNIK}+\mathsf G$ then it is valid in every graph-consistent intuitionistic $\mathsf G$-model.

Proof

By induction on the height of the derivation, using Lemma 5.9.    $\square$

The soundness result in [7] can be obtained as a corollary of this theorem, as our proof method extends Fitting’s technique to the intuitionistic framework.

Corollary 5.11

Let $\mathsf G$ be given. If a sequent $\varSigma$ is provable in $\mathsf {iNK_2}+\mathsf G$ then it is valid in every classical $\mathsf G$-model.

6 Discussion

It has long been known that there is a close correspondence between the logic $\mathsf {K}+ \mathsf {G}$ and the Kripke semantics:

Theorem 6.1

(Lemmon and Scott [14]). Let $\mathsf G\subseteq \mathbb {N}^4$. A formula is derivable in $\mathsf {K}+ \mathsf {G}$, iff it is valid in all classical $\mathsf G$-models.

This means that in the classical case, we have a complete triangle between Kripke models, Hilbert axiomatisation and nested sequents systems via Theorems 4.2, 5.11 and 6.1.

In the intuitionistic case, the correspondence is less clear, and a lot of questions are still open. We do have Theorem 4.2 giving that every theorem of $\mathsf {IK}+\mathsf {G}$ is a theorem of $\mathsf {iNIK}+\mathsf G$, and Theorem 5.10 giving that every theorem of $\mathsf {iNIK}+\mathsf G$ is valid in all graph-consistent $\mathsf G$-models, but there is no proper equivalent to Theorem 6.1 to “link” the two theorems into an actual soundness and completeness result for $\mathsf {iNIK}+\mathsf G$. As we have seen in Sect. 4, the first inclusion is strict, since the formula in (11) is provable in $\mathsf {iNIK}+\mathsf G$, but not in $\mathsf {IK}+ \mathsf {G}$. However, the strictness of the second inclusion is open. The question is: Is there a certain set $\mathsf G\subseteq \mathbb {N}^4$, such that there exists a formula that is valid in every directed graph-consistent $\mathsf G$-models, but that is not a theorem of $\mathsf {iNIK}+\mathsf G$?

On the other hand, Theorems 6.2.1 and 8.1.4 of [25] entail a parallel result to Theorem 6.1 for a restricted family of the intuitionistic Scott-Lemmon axioms, those for which $l=1$ and $n=0$ (or equivalently $l=0$ and $n=1$), that is, of the form: $(\Diamond ^k \Box A \supset \Box ^m A) \wedge (\Diamond ^kA \supset \Box ^m \Diamond A)$. Therefore, in this restricted case, the inclusions collapse too. The reason why this result holds seems to be that in a derivation of a theorem of such a logic, the steps referring to non-tree graphs can be eliminated via appealing to the closure of the accessibility relation (see [25]). This is similar to what happens when going from indexed to pure nested sequents calculi, and suggests that a pure nested sequent calculus could be provided for these logics in the intuitionistic case too. Indeed, these axioms are the intuitionistic variants of some of the path axioms of [10], for which a pure nested sequent calculus is given; but for the general case, [10] only provides a display calculus.

To conclude, we can say that for intuitionistic modal logics the accurate definition might actually come from structural proof-theoretical studies rather than Hilbert axiomatisations or semantical considerations. For Simpson [25] there are two different (but equivalent) ways to define intuitionistic modal logics, either the natural deduction systems he proposes, or the extension of the standard translation for intuitionistic modal logics into first-order intuitionistic logic. Equivalence between the natural deduction systems and the Hilbert axiomatisations, or direct interpretation of the natural deduction systems in intuitionistic (birelational) structures are just side-results. He therefore sees their failure for the majority of logics not as a problem, but rather as another justification of the validity of the proof-theoretic approach.