On Intuitionistic Diamonds (and Lack Thereof)

Abstract

A variety of intuitionistic versions of modal logic $K$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $\Box$-only (or $\Diamond$-free) fragment, suggesting some robustness of ‘$\Box$-only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $IK$ proves strictly more $\Diamond$-free theorems than Fitch’s $CK$, and indeed $i K$, the minimal $\Box$-normal intuitionistic modal logic.

On the other hand we show that the smallest extension of $i K$ by a normal $\Diamond$ is in fact conservative over $i K$ (over $\Diamond$-free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.

1 Introduction

Usual (propositional) modal logic extends the language of classical propositional logic ($CPL$) by two modalities, $\Box$ and $\Diamond$, informally representing ‘necessity’ and ‘possibility’, resp. This informality is made precise by relational semantics. This semantics gives rise to the ‘standard translation’, allowing us to distill the normal modal logic $K$ as a well-behaved fragment of the first-order logic (FOL).

Notably, over classical logic, $\Box$ and $\Diamond$ are De Morgan dual, just like $\forall$ and $\exists$: we have $\Diamond A = \lnot \Box \lnot A$. However, in light of the association with FOL, one would naturally expect an intuitionistic counterpart of modal logic not to satisfy any such reduction. The pursuit of a reasonable definition for an ‘intuitionistic’ modal logic goes back decades, including works such as [7,8,9, 14] as early as the 1950s-60s, more developments [13, 25, 29, 32] in the 1970s, and a growing interest [6, 12, 17, 26, 28, 30, 31, 34, 35] in the 1980s. See [33] or [20] for a survey.

Fig. 1.

Axioms and rules for intuitionistic modal logics.

The smallest such logic that is typically considered is $i K$, obtained by simply extending intuitionistic propositional logic ($IPL$) by the axiom $k_{1}$ and rules $mp , nec$ from Fig. 1, but not including any axioms involving $\Diamond$, e.g. [6, 36]. It seems that Fitch [14] was the first one to propose a way to treat $\Diamond$ in an intuitionistic setting by considering a version of $CK$, extending $i K$ with $k_{2}$. $CK$ enjoys a rather natural proof-theoretic formulation [35] that simply adapts the sequent calculus for $K$ according to the usual intuitionistic restriction: each sequent may have just one formula on the RHS. What is more, cut-elimination for this simple calculus is just a specialisation of the classical case.

$IK$, which includes all axioms and rules in Fig. 1, was introduced by [28] and is equivalent to the logic proposed by [31], or even to [12] in the context of intuitionistic tense logic. In [33] Simpson gives logical arguments in favour of $IK$, namely as a logic that corresponds to intuitionistic FOL along the same standard translation that lifts $K$ to classical FOL. The price to pay, however, is steep: there is no known cut-free sequent calculus complete for $IK$. On the other hand, Simpson demonstrates how the relational semantics of classical modal logic may be leveraged to recover a labelled sequent calculus. The cut-elimination theorem, this time, specialises the cut-elimination theorem for intuitionistic FOL.

Contribution. An apparently widespread perception about intuitionistic modal logics is that $i K$ and $IK$ (and so all logics in between) coincide on their ‘$\Box$-only’ (i.e. $\Diamond$-free) fragments. We show that this is not true by giving an explicit separation of $IK$ from $i K$ (also $CK$) by a $\Diamond$-free formula, and go on to initiate a comparison of the various logics by their $\Diamond$-free fragments. For the first separation, we show $IK$ validates a form of Gödel-Gentzen translation from $K$, but that $CK$ does not; the simplest such separation arising from this is given by $\lnot \lnot \Box \bot \rightarrow \Box \bot$. An important question at this point is whether it is even possible to conservatively extend $i K$ by a normal $\Diamond$, i.e. is $CK + k_{3} + k_{5}$ $\Diamond$-free conservative over $CK$? We answer this positively by designing a new system for the logic based on Fitting’s nested sequents for $IPL$ [16] and proving a cut-elimination result. Our results are summarised in Fig. 2.

Some of the ideas behind this work were announced and discussed on The Proof Theory Blog in 2022 [11] (but have not been peer-reviewed before). We shall reference that discussion further in Sect. 4.

Fig. 2.

Comparison of $\Diamond$-free fragments. Solid arrows denote inclusion, dashed arrows denote non-inclusion. All new results of this work are in red, where faded arrows are consequences of the non-faded ones. The dotted blue ? arrow is apparently open. (Color figure online)

2 Preliminaries

Let us fix a countable set of propositional variables, written p, q etc. When working in predicate logic, we shall simultaneously construe these as unary predicate symbols, and further fix a (infix) binary relation symbol R.

Throughout this paper we shall work with (modal propositional) formulas, written A, B etc., generated by:

$$ A \quad {:}{:}\!= \quad \bot \quad | \quad p \quad | \quad (A \vee B) \quad | \quad (A \wedge B) \quad | \quad (A\rightarrow B) \quad | \quad \Diamond A \quad | \quad \Box A $$

We may write $\lnot A := A \rightarrow \bot$, and frequently omit brackets to aid legibility when it is unambiguous. We write, say, $A\rightarrow B\rightarrow C$ for $A\rightarrow (B\rightarrow C)$.

Due to space constraints, we shall not cover any formal semantics in this work; however it is insightful to recall how modal formulas may be viewed as a fragment of first-order predicate logic. The standard translation is a certain action of modal formulas on first-order variables given by a predicate formula:

Definition 1

(Standard translation). For modal formulas A we define the predicate formula A(x) by:

For the reader familiar with the usual relational semantics of modal logic, note that the formula A(x) simply describes the evaluation of the modal formula A at a ‘world’ x, within predicate logic. From this point of view we have:

Definition 2

$K$ is the set of modal formulas A s.t. A(x) is classically valid.

2.1 Some Axiomatisations and Characterisations

The intuitionistic modal logics we consider will always be extensions of intuitionistic propositional logic ($IPL$) by some of the axioms and rules in Fig. 1. Let us first point out the following well-known axiomatisation:

Proposition 3

(see, e.g., [4, 5]). The $\Diamond$-free fragment of $K$ is axiomatised by classical propositional logic ($CPL$), $k_{1}$, $mp$ and $nec$.

In classical modal logic it suffices at this point to set $\Diamond A \leftrightarrow \lnot \Box \lnot A$ in order to recover the full axiomatisation of $K$, but this will not (in general) be the case for intuitionistic modal logics we are concerned with.

Fig. 3.

The cut-free sequent calculus $\textsf{LCK}$, obtained from the calculus for $K$ by requiring exactly one formula on the RHS.

Definition 4

We define the following intuitionistic modal logics:

• $i K$ extends $IPL$ by $k_{1}$ and is closed under $mp$ and $nec$;

• $CK$ extends $IPL$ by $k_{1}$, $k_{2}$ and is closed under $mp$ and $nec$;

• $IK$ extends $IPL$ by all the axioms $k_{1}$-$k_{5}$ and is closed under $mp$ and $nec$.

$i K$ was studied in, e.g., [6] and [36]. The logic $CK +k_{5}$ was considered in [35], while the restriction to $CK$ itself was given a categorical treatment in [3] and further in [23]. $IK$ was first defined in [30] and [28], and investigated in details in [33]. Note that it is clear from the definitions that $i K \subseteq CK \subseteq IK$.

Since we do not work with formal semantics, we shall introduce certain proof theoretic characterisations of the logics above in order to more easily reason about (non-)provability. At the same time, these characterisations will expose some naturality underlying the logics $i K , CK$ and $IK$.

First, let us point out that classical modal logic $K$ has a simple sequent calculus, extending the usual propositional fragment of Gentzen’s $\textsf{LK}$ by the modal rules (see, e.g., [15]):

Here $\varGamma$ and $\varDelta$ are sets of formulas (cedents) and $\Rightarrow$ is just a syntactic delimiter. A sequent $\varGamma \Rightarrow \varDelta$ is understood logically as $\bigwedge \varGamma \rightarrow \bigvee \varDelta$, its formula translation. Note in particular here the symmetry of the two rules, underpinned by the De Morgan duality between $\Diamond$ and $\Box$ in classical modal logic.

The characteristic property of the logic $CK$ is that it is obtained from the sequent calculus for $K$ by imposing the usual intuitionistic restriction: each sequent must have exactly one formula on the RHS. Formally, writing $\textsf{LCK}$ for the (cut-free) sequent calculus given in Fig. 3, we have the well-known result:

Theorem 5

(e.g., implied by [35]). $\textsf{LCK}$ is sound and complete for $CK$.

This has an entirely syntactic proof, simulating the axiomatisation of $CK$ using a ‘cut’ rule and proving cut-elimination (for the completeness direction). An immediate (and well-known) consequence of this result is the following, justifying the leftmost node of Fig. 2:

Corollary 6

$CK$ is conservative over $i K$, over $\Diamond$-free formulas.

Proof

(idea). By the subformula property of $\textsf{LCK}$ only $\Diamond$-free formulas appear in any proof with $\Diamond$-free conclusion. It is easily verified that any inference step whose premisses and conclusion are $\Diamond$-free are already derivable in $i K$.

Let us now turn to $IK$. One of the principal motivations behind $IK$ is its compatibility with the standard translation, analogous to classical $K$:

Theorem 7

(Intuitionistic standard translation, [33]). $IK$ is the set of modal formulas whose standard translations are intuitionistically valid.

This result corresponds to Simpson’s ‘Requirement 6’ in his PhD thesis [33]. Note here the analogy to $K$’s relationship with classical predicate logic, cf. Definition 2. The proof of the above theorem is a priori nontrivial and is beyond the scope of this work. Importantly, this result induces a proof-theoretic characterisation of $IK$ similar to that of $CK$, only beginning from a different underlying calculus. Namely, $IK$ can be obtained from the ‘labelled’ calculus for $K$ (e.g. [24]) by requiring that each sequent has exactly one formula on the RHS.

Remark 8

Before closing this section it is worthwhile to mention that several other logics intermediate to $CK$ and $IK$ have been studied. One notable choice is Wijesekara’s $CK + k_{5}$, sometimes called $WK$ (e.g. in [10]). Wijesekera used a minor adaptation of $\textsf{LCK}$ to allow empty RHS (as well as singleton), resulting in a calculus that is sound and (cut-free) complete for $WK$ [35]. We shall return to this idea later but for now let us point out that a similar argument to Corollary 6 above indeed shows that even $WK$ is $\Diamond$-free conservative over $i K$. This will be subsumed by our later result for $CK +k_{3} + k_{5}$.

3 Separating $CK$ and $IK$ over the $\Diamond$-Free Fragment

In this section we shall justify the main subject matter of this work: the comparison of $\Diamond$-free fragments of intuitionistic modal logics. That such an investigation is even nontrivial is surprising: for decades now numerous papers have claimed that $i K , CK , IK$ all coincide on their $\Diamond$-free fragments.¹ In this section we show that this is not the case.

3.1 The Gödel-Gentzen Negative Translation

Gödel and Gentzen (independently) introduced certain double negation translations for embedding classical first-order predicate logic into its intuitionistic counterpart [18, 19]. Inspired by the ‘standard translation’ of Definition 1, we duly adapt this translation to the language of modal logic:

Definition 9

(Gödel-Gentzen negative translation). For each modal formula A we define another modal formula $A^N$ as follows:

Note that the image of $\cdot ^N$ is $\{\vee ,\Diamond \}$-free: it is formed from only the ‘negative’ connectives $\bot , \wedge , \rightarrow , \Box$. For the reader familiar with the usual Gödel-Gentzen translation $\cdot ^N$ on first-order predicate formulas, note that our translation above is justified by the standard translation from Definition 1: $A^N (x)$ is the same as $A(x)^N$, up to double negations in front of atomic relational formulas xRy. Nonetheless due to this slight difference, and for self-containment of the exposition, we better give the necessary characterisations explicitly.

3.2 $IK$ Validates Gödel-Gentzen

Lemma 10

(Negativity). $IK$ proves the following:

$$ \begin{array}{c} \lnot \lnot \bot \rightarrow \bot \\ \lnot \lnot \lnot A \rightarrow \lnot A \end{array} \qquad \begin{array}{c} \lnot \lnot (A\wedge B) \rightarrow \lnot \lnot A \wedge \lnot \lnot B \\ \lnot \lnot (A\rightarrow B) \rightarrow \lnot \lnot A \rightarrow \lnot \lnot B \end{array} \qquad \lnot \lnot \Box A \rightarrow \Box \lnot \lnot A $$

Proof

The non-modal cases are already theorems of $IPL$, so it remains to check the final $\Box$ case:

Let us point out that $k_{3}$ was not used in the argument above. We shall keep track of $k_{3}$ (non-)use during this section and state stronger results later. From here by structural induction on formulas, using the above Lemma, we have:

Lemma 11

(Double-negation elimination).$IK \vdash \lnot \lnot A^N \rightarrow A^N$.

Theorem 12

If $K \vdash A$ then $IK \vdash A^N$.

Proof

(sketch). Referring to Proposition 3, simply take an axiomatic $K$ proof of A and replace every formula by its image under $\cdot ^N$. Any non-constructive reasoning is justified by appealing to Lemma 11 above.²

Let us point out that no modal reasoning was used to justify Lemma 11 and Theorem 12, further to what we used for Lemma 10. Thus it is immediate that $CK + k_{4} + k_{5}$ also validates the Gödel-Gentzen translation:

Corollary 13

If $K \vdash A$ then $CK + k_{4} + k_{5} \vdash A^N$.

Example 14

Instantiating the $\Box$-case of the proof of Lemma 10 by $A=\bot$, and since $IPL \vdash \lnot \lnot \bot \rightarrow \bot$, we have that $CK + k_{4} + k_{5} \vdash \lnot \lnot \Box \bot \rightarrow \Box \bot$.

3.3 $CK$ Does not validate Gödel-Gentzen

On the other hand, it is easy to show that $CK$ does not validate the Gödel-Gentzen translation. In particular the simplest such separation is given by:

Proposition 15

$CK \not \vdash \lnot \lnot \Box \bot \rightarrow \Box \bot$.

Proof

By case analysis on cut-free bottom-up proof search in $\textsf{LCK}$. The only applicable rule is $\rightarrow \text {-}r$, requiring us to prove $\lnot \lnot \Box \bot \Rightarrow \Box \bot$. At this stage there are two possible choices:

• weaken $\lnot \lnot \Box \bot$ on the LHS: this would require us to prove $\Rightarrow \Box \bot$, which is not even classically valid.

• apply $\rightarrow \text {-}l$ on $\lnot \lnot \Box \bot$ on the LHS:³ this requires us to prove $\Rightarrow \lnot \Box \bot$ (the left premiss) which is, again, not even classically valid.

Recalling Lemma 10 for $IK$, what breaks down here for $CK$ is the negativity of the $\Box$, i.e. $\lnot \lnot \Box A \rightarrow \Box \lnot \lnot A$. Its underivability in $CK$ is immediate from Proposition 15 above, cf. Example 14. In particular we have:

Corollary 16

$CK +k_{4}+k_{5}$ (and so also $IK$) proves strictly more $\Diamond$-free theorems than $CK$ (and so also $i K$).

4 Perspectives

4.1 On Other Separations and $\Diamond$-Free Axiomatisations

Despite the separation in the preceding section, $i K$ and $CK$ are known to validate some other double-negation translations, see e.g. [22]. Of course none of these translations rely on negativity of the $\Box$, i.e. $\lnot \lnot \Box A \rightarrow \Box \lnot \lnot A$. Our separation was announced (but not peer-review published) in a post on The Proof Theory Blog in August 2022 [11]. The discussion therein covered several other separating formulas too. In particular, Alex Simpson reported such a separation $C = (\lnot \Box \bot \rightarrow \Box \bot ) \rightarrow \Box \bot$ privately communicated to him in 1996 by Carsten Grefe. Let us point out that this latter separation is already a consequence of Proposition 15, as even $IPL$ already proves $C \rightarrow \lnot \lnot \Box \bot \rightarrow \Box \bot$: it is an instance of the $IPL$ theorem $((\lnot A \rightarrow A)\rightarrow A) \rightarrow \lnot \lnot A \rightarrow A$ by $A= \Box \bot$.

In the same discussion it was mentioned that the $\Diamond$-free fragment of $IK$ was not finitely $\Diamond$-free axiomatisable. We could not find this result in the literature, nor could we easily verify it independently. While its status is beyond the scope of this work, let us make an observation:

Proposition 17

We have:

• 1. The $\Diamond$-free fragment of $CK + k_{4} + k_{5}$ is finitely $\Diamond$-free axiomatised.

• 2. The $\{\vee ,\Diamond \}$-free fragment of $IK$ is finitely $\{\vee ,\Diamond \}$-free axiomatised and coincides with that of $CK + k_{4} + k_{5}$.

Proof

(sketch). Replacing $\Diamond \cdot$ by $\lnot \Box \lnot \cdot$ and $\cdot \vee \cdot$ by $\lnot (\lnot \cdot \wedge \lnot \cdot )$ in the axioms $k_{1}$-$k_{5}$ yields theorems of $CK + k_{4} + k_{5}$. Both results follow from here by carrying out the same replacement everywhere in an axiomatic proof, construing the modified versions of $k_{1}$-$k_{5}$ as the underlying axiomatisation.

Note that an immediate consequence of the result above is that, if indeed the $\Diamond$-free fragment of $IK$ is not finitely axiomatised, then it is separated from the $\Diamond$-free fragment of $CK + k_{4} + k_{5}$, and any such separation must make crucial use of $\vee$, cf. the blue arrow in Fig. 2.

4.2 On $\Diamond$-Normality and the Problem of $CK + k_{3} + k_{5}$

The $\Diamond$-free separation of $i K$ and $IK$ forces us to question some of the ‘canonical’ aspects of ‘$\Box$-only intuitionistic modal logic’ $i K$. Above all, it is not clear whether fixing $i K$ (or the $\Diamond$-free fragment of $CK$) forces, say, abnormality of the $\Diamond$; equivalently, does normality of the $\Diamond$, i.e. $k_{3} + k_{5}$, force more $\Diamond$-free theorems over $i K$ (or $CK$)? Let us point out that in the post [11] there was significant discussion about the status of $CK + k_{3} + k_{5}$, with no definitive resolution about its $\Diamond$-free fragment with respect to $i K , CK , IK$. The remainder of this paper is devoted to a resolution of this question; namely, $CK + k_{3} + k_{5}$ is indeed $\Diamond$-free conservative over $i K$, cf. Fig. 2.

Before turning to that, let us briefly discuss why the status of $CK + k_{3} + k_{5}$ is somewhat nontrivial. Recalling Remark 8, it would be natural to further generalise the calculus $\textsf{LCK}$ to a ‘multi-succedent’ version, allowing any number of formulas on the RHS, not just 1 (or 0 for $WK$). The RHS singleton restriction now only applies to the $\Box$ and $\rightarrow \text {-}r$ rules. The idea is that, while 0 formulas on the RHS corresponds to $k_{5}$, many could correspond to $k_{3}$. Indeed this seems promising in light of the following (cut-free) multi-succedent proofs of those axioms:

The calculus is hence readily seen to be sound for $CK +k_{3} +k_{5}$. However it does not enjoy cut-elimination, due to issues with commutative cases arising from the single succedent restriction on the $\Box$ rule and the $\rightarrow \text {-}r$ rule. In particular, while $CK + k_{3} + k_{5} \vdash \Diamond (A \vee (B \rightarrow C)) \rightarrow (\Diamond A \vee (\Box B \rightarrow \Diamond C))$, e.g. by the proof,

note that it has no cut-free such proof, by consideration of rule applications.

5 Nested Sequent Calculus for $CK + k_{3} + k_{5}$

In this section we will introduce a nested sequent calculus $\textsf{nJ}_{\Diamond ,\Box }$ for $CK + k_{3} + k_{5}$, by extending Fitting’s calculus for $IPL$ [16] by natural modal rules. We prove a cut-elimination result for $\textsf{nJ}_{\Diamond ,\Box }$, which will imply the $\Diamond$-free conservativity of $CK + k_{3} + k_{5}$ over $CK$. We shall mostly follow the notation employed by Fitting, but deviate in minor conventions to facilitate our ultimate cut-elimination result. All results are self-contained.

A (nested) sequent, written S etc., is an expression $\varGamma \Rightarrow X$ where $\varGamma$ is a set of formulas and X is a set of formulas and nested sequents. We interpret sequents by a formula translation: $fm (\varGamma \Rightarrow \varDelta , X) \quad :=\quad \bigwedge \varGamma \rightarrow \left( \bigvee \varDelta \vee \bigvee _{S\in X} fm (S) \right)$.

A (nested sequent) context, written $S[\, ]$, is defined as expected. Note that it is implicit in this notation that the context hole must only occur where a nested sequent may be placed to produce a correct nested sequent, i.e., for $S[\, ]$ a context and $S'$ a nested sequent, $S[S']$ is always a nested sequent.

Example 18

(Contexts). $A \Rightarrow B, (C,D \Rightarrow E,[\, ])$ is a context, but $A,[\, ] \Rightarrow B,C$ and $A \Rightarrow B, (C , [\, ] \Rightarrow D)$ are not.

We may also write contexts for sets (of nested sequents and formulas), e.g. $X[\, ]$, etc., where again X[S] must always be a correct set of nested sequents and formulas. A consequence of the definition of nested sequent is that we can safely substitute sets in place of context hole, i.e. if Y is a set of nested sequents and formulas then (X[Y] and) S[Y] is a (set of) nested sequent(s and formulas).

5.1 System $\textsf{nJ}_{\Diamond ,\Box }$

The system $\textsf{nJ}$ is given by the structural rules and (left and right) logical rules from Fig. 4. It is equivalent to the nested calculus given by Fitting in [16], but we shall not use this fact: its soundness and completeness for $IPL$ will be a consequence of later results. To define its extension by modalities, we must first generalise the usual notion of a modality distributing over a sequent:

Fig. 4.

System $\textsf{nJ}_{\Diamond ,\Box }$.

Definition 19

(Promotion). For sets X define $X^{\circ }$ by:

For (set-)contexts X[], we define $X^{\circ }[]$ the same way and by setting $[]^{\circ }:=[]$.

Remark 20

(Promotion and $\Diamond$-normality). The intention is that $X^{\circ }$ is a consequence of $\Diamond fm (X)$. The $\varnothing$ case is justified by $k_{5}$, while the ‘, ’ case is justified by $k_{3}$. The ‘$\Rightarrow$’ case is justified by the ‘Fischer Servi’ property: $\Diamond (A \rightarrow B) \rightarrow \Box A \rightarrow \Diamond B$. This is a consequence already of $CK$:

A right-, is a comma ‘, ’ on the RHS of some $\Rightarrow$ (immediately, not hereditarily). A sequent (or context) is right-,-free if it has no right-, .

Definition 21

The system $\textsf{nJ}_{\Diamond ,\Box }$ consists of all the rules in Fig. 4.

Example 22

Recall the formula $\Diamond (A \vee (B \rightarrow C)) \rightarrow (\Diamond A \vee (\Box B \rightarrow \Diamond C))$ from Subsect. 4.2, which is a consequence of $CK + k_{3} + k_{5}$ but has no cut-free proof in the ‘multi-succedent’ version of $\textsf{LCK}$. We here give a $\textsf{nJ}_{\Diamond ,\Box }$ proof of it:

We have coloured red the ‘principal’ part of an inference step. Note at the top the necessity of applying the $\Rightarrow$ rule before $\rightarrow \text {-}l$, bottom-up, in order to prove $\Rightarrow B\rightarrow C \Rightarrow A, (B\Rightarrow C)$.

The main result of this section is:

Theorem 23

(Soundness and completeness). $\textsf{nJ}_{\Diamond ,\Box }\vdash \Rightarrow A$ if and only if $CK + k_{3} + k_{5} \vdash A$.

To show the completeness (if) direction we will need to first give a simulation using a ‘cut’ rule, then prove cut-elimination. To avoid case explosion later in the presence of modal rules, it will facilitate our ultimate cut-elimination argument to consider a ‘context-joining’ cut, à la Tait. For this, we first need to generalise the usual notion of sequent union:

Definition 24

(Context joining). For contexts S[], $S'[]$ define $S[]\cdot S'[]$ by:

• ${[}{]}\cdot S[] := S[]$;

• $(\varGamma \Rightarrow X, S[])\cdot (\varGamma ' \Rightarrow X', S'[]) := \varGamma , \varGamma '\Rightarrow X,X', (S[]\cdot S'[])$

Note that, by a basic induction on the structure of contexts, we have that $\cdot$ is associative, commutative and idempotent. We shall sometimes write simply $(S\cdot S')[]$ for $(S[]\cdot S'[])$, as abuse of notation. We shall also sometimes extend this notation to set-contexts, $X[]\cdot X'[]$, by adding the clause $(X,Y[])\cdot (X',Y'[]) := X,X', (Y[]\cdot Y'[])$. From here the $cut$ rule is defined as:

(1)

5.2 Metalogical Results

By induction on the structure of $\textsf{nJ}_{\Diamond ,\Box }+ cut$ proofs it is routine to establish the ‘only if’ direction of our main result Theorem 23:

Proposition 25

(Soundness). If $\textsf{nJ}_{\Diamond ,\Box }+ cut \vdash S$ then $CK +k_{3} + k_{5} \vdash fm (S)$.

The most interesting case is the $\Diamond$ rule, which is justified by Remark 20. Among the non-modal rules the most interesting cases are the ‘switch’ rule $\Rightarrow$ and the branching rules, which make use of the following lemma:

Lemma 26

The following are intuitionistically valid:

$$ {\begin{array}{l} ((A\rightarrow B)\vee C) \rightarrow (A\rightarrow (B\vee C)) \\ ((A\vee B)\rightarrow C) \leftrightarrow ((A\rightarrow C) \wedge (B\rightarrow C)) \end{array} \qquad \begin{array}{l} (A\rightarrow (B\wedge C)) \leftrightarrow ((A\rightarrow B)\wedge (A\rightarrow C)) \\ (A\vee (B\wedge C))\leftrightarrow ((A\vee B) \wedge (A\vee C)) \end{array}} $$

Let us write $\Rightarrow ^n$ for $\overbrace{\Rightarrow \cdots \Rightarrow }^n$. Note that, if S is a nested sequent, then so is $\Rightarrow ^n S$, for all $n\ge 0$. We have a routine (cut-free) simulation of $CK$ in $\textsf{nJ}_{\Diamond ,\Box }$:

Lemma 27

(Simulation of $\textsf{LCK}$). If $\textsf{LCK}\vdash \varGamma \Rightarrow A$ then $\textsf{nJ}_{\Diamond ,\Box }\vdash \, \Rightarrow ^n \varGamma \Rightarrow A$ for all $n \ge 0$.

Proof

(sketch). The proof is by straightforward induction on the structure of a (cut-free) $\textsf{LCK}$ proof of $\varGamma \Rightarrow A$. Almost all rules of $\textsf{LCK}$ are essentially special cases of their analogues in $\textsf{nJ}_{\Diamond ,\Box }$; the only exception is the right implication rule, which is simulated as follows:⁴

Proposition 28

(Cut-completeness with cut). If $CK + k_{3} + k_{5} \vdash A$ then $\textsf{nJ}_{\Diamond ,\Box }+ cut \vdash \, \Rightarrow A$.

Proof

(sketch). By induction on an axiomatic $CK + k_{3} + k_{5}$ proof of A. In light of Lemma 27 above, and the presence of $cut$, it suffices to prove $k_{3}$ and $k_{5}$:

6 Cut-Elimination Argument

The goal of this section is to prove:

Theorem 29

(Cut-elimination). If $\textsf{nJ}_{\Diamond ,\Box }+ cut \vdash S$ then also $\textsf{nJ}_{\Diamond ,\Box }\vdash S$.

From here note that our main result follows immediately:

Proof

(of Theorem 23). Immediate from Theorem 29 above, Soundness (Proposition 25) and Completeness with cut (Proposition 28).

The size of a proof is its number of inference steps. The degree of a cut is the number of symbols in its cut-formula, i.e. the formula A distinguished in (1). Our ultimate argument for cut-elimination is based on a typical double induction:

Proof

(of Theorem 29, sketch). We proceed by induction on the multiset of cut-degrees in a proof. We start with a(ny) topmost cut, employing a subinduction on the size of the subproof rooting it, permuting the cut upwards in order to apply the subinductive hypothesis. At key cases the multiset of cut-degrees will decrease and we instead apply the main inductive hypothesis on the entire proof; sometimes we may need to first apply the subinductive hypothesis. In terms of the permutation strategy, we always permute cuts over non-modal rules (on either side) maximally, so that our modal cut-reductions only apply when the inference step immediately above each side of a cut is modal.

The next subsection is devoted to describing some of the cut-reductions. Before that let us give the desired consequence of cut-elimination for $\textsf{nJ}_{\Diamond ,\Box }$, namely the classification of the $\Diamond$-free fragment of $CK + k_{3} + k_{5}$, cf. Fig. 2:

Corollary 30

$CK + k_{3} + k_{5}$ is conservative over $i K$, over $\Diamond$-free formulas.

Proof

(sketch). If $CK + k_{3} + k_{5}$ proves a $\Diamond$-free formula A, then there is a $\textsf{nJ}_{\Diamond ,\Box }$ proof P of $\Rightarrow A$ by Theorem 23. By the subformula property, P must be $\Diamond$-free itself, so the only modal rule occurring in P is the $\Box$-rule, whose formula translation is derivable already in $i K$. (Note that the formula translation of $\Diamond$-free nested sequents is always $\Diamond$-free). All other rules are derivable already in $IPL$.

6.1 Cut-Reduction Cases (Non-modal)

To facilitate the description of the cut-reduction cases we will need to ‘bootstrap’ $\textsf{nJ}_{\Diamond ,\Box }$ somewhat. We say a rule r is size-preserving admissible for a system $\mathsf L$ if, whenever there is a proof in $\mathsf L+r$ of S, there is a proof in $\mathsf L$ of S of the same or smaller size.

Proposition 31

The following rules are size-preserving admissible for $\textsf{nJ}_{\Diamond ,\Box }$:

Thanks to the way we have presented our rules, almost all cut-reduction cases are ‘the same’ as those for usual sequent calculi for intuitionistic and/or modal logic, only under a sequent context. We highlight here some cases that need special attention.

For key cases, when the cut-formula is principal for a logical rule on both sides of a cut, the corresponding reduction is almost always the same as that for the usual (multi-succedent) sequent calculus for $IPL$, only under a sequent context. The only exception is for $\rightarrow$, since its right-introduction rule is different from that of the sequent calculus. The key case for $\rightarrow$ is:

Referring to our cut-elimination argument, note we must apply the subinductive hypothesis to the topmost cut before calling the main inductive hypothesis.

Any cut immediately preceded by an identity step (on either side) can be reduced to an identity step, eliminating the cut. Also all commutations of a cut above a logical rule are routine, as the $\Rightarrow$-depth of the cut-formula is not affected.

Almost all permutations when a cut is preceded by a structural step are routine. The only exception is a permutation over a $\Rightarrow$ step. Before we can present this we need to set up some notation. First, let us write $\Rightarrow ^{X[\, ]}$ for $\Rightarrow ^d$ where d is the $\Rightarrow$-depth of the hole $[\, ]$ in $X[\, ]$. I.e.,

We shall sometimes write $\Rightarrow ^X$ for $\Rightarrow ^{X[\, ]}$, as abuse of notation. By a straightforward induction on the structure of set-contexts we have that $\Rightarrow ^{X}[\, ]\cdot X[\, ] = X[\, ]$. Now we can give the critical $\Rightarrow$-permutation by:

Note the importance here of size-preserving admissibility of $\Rightarrow \text {-}i$, Proposition 31, in order to appeal to the subinductive hypothesis.

6.2 Cut-Reduction Cases (Modal)

Defining the modal cut-reductions is facilitated by the observation that $(S_0^{\circ }\cdot S_1^{\circ })[] = (S_0\cdot S_1)^{\circ }[]$, proved again by a straightforward induction on the structure of sequent-contexts. The case analysis for modal cut-reductions is routine but lengthy; all reductions allow immediate appeal to the (sub)inductive hypothesis:

• ($\Diamond$-$\Diamond$) If a cut is preceded on both sides by a $\Diamond$ step, then the cut-formula on the right must be the distinguished $\Diamond$-formula of the $\Diamond$ rule in Fig. 4. We employ a case analysis on the relative location of the distinguished $\Diamond$ formula and the cut formula on the left, but each situation is handled similarly. If, e.g., the distinguished $\Diamond$ formula and cut formula occur in parallel in the sequent context we have the following reduction:

  

• ($\Diamond$-$\Box$) It is not possible for a cut to be preceded by a $\Diamond$ step on the left and a $\Box$ step on the right, since the former has only $\Diamond$ formulas in positive positions and the latter has only $\Box$ formulas in negative positions.

• ($\Box$-$\Diamond$) If a cut is preceded by a $\Box$ rule on the left and a $\Diamond$ rule on the right then the cut-formula must be a $\Box$ formula, and so cannot be the distinguished $\Diamond$ formula of the $\Diamond$ step. We again employ a case analysis on the relative location of the distinguished $\Diamond$ formula and cut formula on the right, but each situation is handled similarly. If, e.g., the distinguished $\Diamond$ formula occurs (relatively) deeper than the cut formula, we have the following reduction:

  

• ($\Box$-$\Box$) If a cut is preceded on both sides by a $\Box$ rule, then the only possible reduction, due to right-, -freeness in the right premiss, is:

  

7 Conclusions

We showed that $i K$ and $CK$ are separated from $IK$ by their $\Diamond$-free theorems, and have moreover initiated a comparison of intuitionistic modal logics by their $\Diamond$-free fragments. In particular, we have verified using proof theoretic techniques that the extension of $i K$ by a normal $\Diamond$ is indeed conservative over $i K$, over $\Diamond$-free formulas. Again, our results are summarised in Fig. 2.

Our nested sequent system $\textsf{nJ}_{\Diamond ,\Box }$ is based on Fitting’s for $IPL$ in [16], but let us point out that he did not give a cut-elimination result. Naturally our cut-elimination result Theorem 29 also implies cut-elimination for the nested calculus $\textsf{nJ}$ for $IPL$. Let us emphasise that, just as $i K , CK , IK$ are proof-theoretically natural by the characterisations in Subsect. 2.1, so too is $CK +k_{3}+k_{5}$: it is just the extension of the calculus $\textsf{nJ}$ for $IPL$ by modal rules.

From here it would be fruitful to understand how to adequately extend (birelational) semantics for $CK$ to $CK + k_{3} + k_{5}$. This could also yield an alternative (and perhaps simpler) proof of completeness of $\textsf{nJ}_{\Diamond ,\Box }$ for $CK + k_{3} + k_{5}$.⁵ We have also not addressed the decidability of logics in this work, but let us point out that we believe that $CK + k_{3} +k_{5}$ might be proved decidable by eliminating $\Rightarrow \text {-}e$ in $\textsf{nJ}_{\Diamond ,\Box }$ and employing a basic loop checking argument.

There has been significant work on computational interpretations of $CK$ e.g. [1,2,3, 21, 27]. However, one shortfall of $CK$ here is that its interpretations do not lift to $K$ along the Gödel-Gentzen translation; while alternative double-negation translations are available, cf. [22], these do not seem robust against modest extensions, e.g. when including a global modality $\Box ^*$. On the other hand the fact that $IK$ validates Gödel-Gentzen, Theorem 12, suggests that it is better designed for computational interpretations, in particular for interpreting classical modal logic $K$. Under the standard translation, it would be interesting to classify the Curry-Howard interpretation of $IK$ as a suitable fragment of dependent type theory. Let us point out that Simpson already gives a termination and confluence proof for a version of intuitionistic natural deduction specialised to $IK$ in his thesis [33].