Intuitionistic Non-Normal Modal Logics: A general framework

TL;DR

This paper introduces a broad family of intuitionistic non-normal modal logics, providing axiomatizations, sequent calculi, and semantic models, extending existing systems like Constructive K and Dynamic Logic.

Contribution

It develops a general framework for intuitionistic non-normal modal logics, including monomodal and bimodal systems with new interaction semantics, and proves their decidability.

Findings

Defined a family of intuitionistic non-normal modal logics

Provided Hilbert axioms and cut-free sequent calculi

Established semantic neighborhood models for these logics

Abstract

We define a family of intuitionistic non-normal modal logics; they can bee seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain only one between Necessity and Possibility. We then consider the more important case of bimodal logics, which contain both modal operators. In this case we define several interactions between Necessity and Possibility of increasing strength, although weaker than duality. For all logics we provide both a Hilbert axiomatisation and a cut-free sequent calculus, on its basis we also prove their decidability. We then give a semantic characterisation of our logics in terms of neighbourhood models. Our semantic framework captures modularly not only our systems but also already known intuitionistic non-normal modal logics such as Constructive K (CK) and the propositional fragment of Wijesekera's Constructive Concurrent Dynamic Logic.

Equations

$$(\text{C◊})◊(A\vee B)\supset ◊A\vee ◊B$$

$$\square (A\wedge B)\supset \subset (\square A\wedge \square B)$$

$$\square A\supset \subset \neg ◊\neg A$$

Full text

1 Introduction

Both intuitionistic modal logic and non-normal modal logic have been studied for a long time. The study of modalities with an intuitionistic basis goes back to Fitch in the late 40s (Fitch [7]) and has led to an important stream of research. We can very schematically identify two traditions: so-called Intuitionistic modal logics versus Constructive modal logics. Intuitionistic modal logics have been systematised by Simpson [23], whose main goal is to define an analogous of classical modalities justified from an intuitionistic point of view. On the other hand, constructive modal logics are mainly motivated by their applications to computer science, such as the type-theoretic interpretations (Curry–Howard correspondence, typed lambda calculi), verification and knowledge representation,222For a recent survey see Stewart et al. [25] and references therein. but also by their mathematical semantics (Goldblatt [11]).

On the other hand, non-normal modal logics have been strongly motivated on a philosophical and epistemic ground. They are called “non-normal” as they do not satisfy all the axioms and rules of the minimal normal modal logic K. They have been studied since the seminal works of Scott, Lemmon, and Chellas ([22], [2], see Pacuit [21] for a survey), and can be seen as generalisations of standard modal logics. They have found an interest in several areas such as epistemic and deontic reasoning, reasoning about games, and reasoning about probabilistic notions such as “truth in most of the cases”.

Although the two areas have grown up seemingly without any interaction, it can be noticed that some intuitionistic or constructive modal logics investigated in the literature contain non-normal modalities. The prominent example is the logic CCDL proposed by Wijesekera [27], whose propositional fragment (that we call CCDLp) has been recently investigated by Kojima [13]. This logic has a normal $\Box$ modality and a non-normal $\Diamond$ modality, where $\Diamond$ does not distribute over the $\lor$, that is

[TABLE]

is not valid. The original motivation by Wijesekera comes from Constructive Concurrent Dynamic Logic, but the logic has also an interesting epistemic interpretation in terms of internal/external observers proposed by Kojima. A related system is Constructive K (CK), that has been proposed by Bellin et al. [1] and further investigated by Mendler and de Paiva [19], Mendler and Scheele [20]. This system not only rejects $\mathsf{C}_{\Diamond}$, but also its nullary version $\Diamond\bot\supset\bot$ ($\mathsf{N}_{\Diamond}$). In contrast all these systems assume a normal interpretation of $\Box$ so that

[TABLE]

is always assumed. A further example is Propositional Lax Logic (PLL) by Fairtlough and Mendler [4], an intuitionistic monomodal logic for hardware verification where the modality does not validate the rule of necessitation.

Finally, all intuitionistic modal logics reject the interdefinability of the two operators:

[TABLE]

and its boolean equivalents.

To the best of our knowledge, no systematic investigation of non-normal modalities with an intuitionistic base has been carried out so far. Our aim is to lay down a general framework which can accommodate in a uniform way intuitionistic counterparts of the classical cube of non-normal modal logics, as well as CCDLp and CK mentioned above. As we shall see, the adoption of an intuitionistic base leads to a finer analysis of non-normal modalities than in the classical case. In addition to the motivations for classical non-normal modal logics briefly recalled above, an intutionistic interpretation of non-normal modalities may be justified by more specific interpretations, of which we mention two:

• •

The deontic interpretation: The standard interpretation of deontic operators $\Box$ (Obligatory), $\Diamond$ (Permitted) is normal: but it has been known for a long time that the normal interpretation is problematic when dealing for instance with “Contrary to duty obligations".333For a survey on puzzles related to a normal interpretation of the deontic modalities see McNamara [18]. One solution is to adopt a non-normal interpretation, rejecting in particular the monotonicity principle (from $A\supset B$ is valid infer $\Box A\supset\Box B$). Moreover, a constructive reading of the deontic modalities would further reject their interdefinability: one may require that the permission of $A$ must be justified explicitly or positively (say by a proof from a corpus of norms) and not just established by the fact that $\neg A$ is not obligatory (see for instance the distinction between weak and strong permissions in von Wright [31]).

• •

The contextual interpretation: A contextual reading of the modal operators is proposed in Mendler and de Paiva [19]. In this interpretation $\Box A$ is read as “$A$ holds in all contexts” and $\Diamond A$ as “A holds in some context”. This interpretation invalidates $\mathsf{C}_{\Diamond}$, while retaining the distribution of $\Box$ over conjunction ($\mathsf{C}_{\Box}$). But this contextual interpretation is not the only possible one. We can interpret $\Box A$ as $A$ is “justified” (proved) in some context $c$, no matter what is meant by a context (for instance a knowledge base), and $\Diamond A$ as $A$ is “compatible” (consistent) with every context. With this interpretation both operators would be non-normal as they would satisfy neither $\mathsf{C}_{\Box}$, nor $\mathsf{C}_{\Diamond}$.

As we said, our aim is to provide a general framework for non-normal modal logics with an intuitionistic base. However, in order to identify and restrain the family of logics of interest, we adopt some criteria, which partially coincide with Simpson’s requirements (Simpson [23]):

• •

The modal logics should be conservative extensions of IPL.

• •

The disjunction property must hold.

• •

The two modalities should not be interdefinable.

• •

We do not consider systems containing the controversial $\mathsf{C}_{\Diamond}$.

Our starting point is the study of monomodal systems, which extend IPL with either $\Box$ or $\Diamond$, but not both. We consider the monomodal logics corresponding to the classical cube generated by the weakest logic E extended with conditions M, N, C (with the exception of $\mathsf{C}_{\Diamond}$). We give an axiomatic characterisation of these logics and equivalent cut-free sequent systems similar to the one by Lavendhomme and Lucas [15] for the classical case.

Our main interest is however in logics which contain both $\Box$ and $\Diamond$, and allow some form of interaction between the two. Their interaction is always weaker than interdefinability. In order to define logical systems we take a proof-theoretical perspective: the existence of a simple cut-free system, as in the monomodal case, is our criteria to identify meaningful systems. A system is retained if the combination of sequent rules amounts to a cut-free system.

It turns out that one can distinguish three degrees of interaction between $\Box$ and $\Diamond$, that are determined by answering to the question, for any two formulas $A$ and $B$:

under what conditions $\Box A$ and $\Diamond B$ are jointly inconsistent?

Since there are three degrees of interaction, even the weakest classical logic E has three intuitionistic counterparts of increasing strength. When combined with M, N, C properties of the classical cube, we end up with a family of 24 distinct systems, all enjoying a cut-free calculus and, as we prove, an equivalent Hilbert axiomatisation. This shows that intuitionistic non-normal modal logic allows for finer distinctions whence a richer theory than in the classical case.

The existence of a cut-free calculus for each of the logics has some important consequences: We can prove that all systems are indeed distinct, that all of them are “good” extensions of intuitionistic logic, and more importantly that all of them are decidable.

We then tackle the problem of giving a semantic characterisation of this family of logics. The natural setting is to consider an intuitionistic version of neighbourhood models for classical logics. Since we want to deal with the language containing both $\Box$ and $\Diamond$, we consider neighbourhood models containing two distinct neighbourhood functions $\mathcal{N}_{\Box}$ and $\mathcal{N}_{\Diamond}$. As in standard intuitionistic models, they also contain a partial order on worlds. Different forms of interaction between the two modal operators correspond to different (but natural) conditions relating the two neighbourhood functions. By considering further closure conditions of neighbourhoods, analogous to the classical case, we can show that this semantic characterises modularly the full family of logics. Moreover we prove, through a filtration argument, that most of the logics have the finite model property, thereby obtaining a semantic proof of their decidability.

It is worth noticing that in the (easier) case of intuitionistic monomodal logic with only $\Box$ a similar semantics and a matching completeness theorem have been given by Goldblatt [11]. More recently, Goldblatt’s semantics for the intuitionistic version of system E has been reformulated and extended to axiom T by Witczak [29].

But our neighbourhood models have a wider application than the characterisation of the family of logics mentioned above. We show that adding suitable interaction conditions between $\mathcal{N}_{\Box}$ and $\mathcal{N}_{\Diamond}$ we can capture CCDLp as well as CK. We show this fact first directly by proving that both CCDLp and CK are sound and complete with respect to our models satisfying an additional condition. We then prove the same result by relying on some pre-existing semantics of these two logics and by transforming models. In case of CCDLp, there exists already a characterisation of it in terms of neighbourhood models, given by Kojima [13], although the type of models is different, in particular Kojima’s models contain only one neighbourhood function.

The case of CK is more complicated, whence more interesting: this logic is characterised by a relational semantics defined in terms of Kripke models of a peculiar nature: they contain “fallible” worlds, i.e. worlds which force $\bot$. We are able to show directly that relational models can be transformed into our neighbourhood models satisfying a specific interaction condition and vice versa.

All in all, we get that the well-known CK can be characterised by neighbourhood models, after all rather standard structures, alternative to non-standard Kripke models with fallible worlds. This fact provides further evidence in favour of our neighbourhood semantics as a versatile tool to analyse intuitionistic non-normal modal logics.

2 Classical non-normal modal logics

2.1 Hilbert systems

Classical non-normal modal logics are defined on a propositional modal language $\mathcal{L}$ based on a set $Atm$ of countably many propositional variables. Formulas are given by the following grammar, where $p$ ranges over $Atm$:

$A::=p\mid\bot\mid A\land A\mid A\lor A\mid A\supset A\mid\Box A\mid\Diamond A$.

We use $A,B,C$ as metavariables for formulas of $\mathcal{L}$. $\top$, $\neg A$ and $A\supset\subset B$ are abbreviations for, respectively, $\bot\supset\bot$, $A\supset\bot$ and $(A\supset B)\land(B\supset A)$. We take both modal operators $\Box$ and $\Diamond$ as primitive (as well as all boolean connectives), as it will be convenient for the intuitionistic case. Their duality in classical modal logics is recovered by adding to any system one of the duality axioms $\mathsf{Dual_{\Box}}$ or $\mathsf{Dual_{\Diamond}}$ (Figure 1), which are equivalent in the classical setting.

The weakest classical non-normal modal logic E is defined in language $\mathcal{L}$ by extending classical propositional logic (CPL) with a duality axiom and rule $\mathsf{E_{\Box}}$, and it can be extended further by adding any combination of axioms $\mathsf{M}_{\Box}$, $\mathsf{C}_{\Box}$ and $\mathsf{N}_{\Box}$. We obtain in this way eight distinct systems (Figure 2), which compose the family of classical non-normal modal logics.

Equivalent axiomatisations for these systems are given by considering the modal axioms in the right-hand column of Figure 1($a$). Thus, logic E could be defined by extending CPL with axiom $\mathsf{Dual_{\Box}}$ and rule $\mathsf{E_{\Diamond}}$, and its extensions are given by adding combinations of axioms $\mathsf{M}_{\Diamond}$, $\mathsf{C}_{\Diamond}$ and $\mathsf{N}_{\Diamond}$.

It is worth recalling that axioms $\mathsf{M}_{\Box}$, $\mathsf{M}_{\Diamond}$ and $\mathsf{N}_{\Box}$ are syntactically equivalent with the rules $\mathsf{Mon_{\Box}}$, $\mathsf{Mon_{\Diamond}}$ and $\mathsf{Nec}$, respectively, and that axiom $\mathsf{K}_{\Box}$ is derivable from $\mathsf{M}_{\Box}$ and $\mathsf{C}_{\Box}$. As a consequence, we have that the top system MCN is equivalent to the weakest classical normal modal logic K.

2.2 Neighbourhood semantics

The standard semantics for classical non-normal modal logics is based on the so-called neighbourhood (or minimal, or Scott-Montague) models.

Definition 2.1**.**

A neighbourhood model is a triple $\mathcal{M}=\langle\mathcal{W},\mathcal{N},\mathcal{V}\rangle$, where $\mathcal{W}$ is a non-empty set, $\mathcal{N}$ is a neighbourhood function $\mathcal{W}\longrightarrow\mathcal{P}(\mathcal{P}(\mathcal{W}))$, and $\mathcal{V}$ is a valuation function $\mathcal{W}\longrightarrow Atm$. A neighbourhood model is supplemented, closed under intersection, or contains the unit, if $\mathcal{N}$ satisfies the following properties:

[TABLE]

The forcing relation $w\Vdash A$ is defined inductively as follows:

[TABLE]

where $[B]$ denotes the set $\{v\in\mathcal{W}\mid v\Vdash B\}$, called the truth set of $B$.

We can also recall that in the supplemented case, the forcing conditions for modal formulas are equivalent to the following ones:

[TABLE]

Theorem 2.1** (Chellas [2]).**

Logic E(M,C,N) is sound and complete with respect to neighbourhood models (which in addition are supplemented, closed under intersection and contain the unit).

3 Intuitionistic non-normal monomodal logics

Our definition of intuitionistic non-normal modal logics begins with monomodal logics, that is logics containing only one modality, either $\Box$ or $\Diamond$. We first define the axiomatic systems, and then present their sequent calculi.

Under “intuitionistic modal logics” we understand any modal logic L that extends intuitionistic propositional logic (IPL) and satisfies the following requirements:

• (R1)

L is conservative over IPL: its non-modal fragment coincides with IPL.

• (R2)

L satisfies the disjunction property: if $A\lor B$ is derivable, then at least one formula between $A$ and $B$ is also derivable.

3.1 Hilbert systems

From the point of view of axiomatic systems, two different classes of intuitionistic non-normal monomodal logics can be defined by analogy with the definition of classical non-normal modal logics (cf. Section 2). Intuitionistic modal logics are modal extensions of IPL, for which we consider the following axiomatisation:

[TABLE]

We define over IPL two families of intuitionistic non-normal monomodal logics, that depend on the considered modal operator, and are called therefore the $\Box$- and the $\Diamond$-family. The $\Box$-family is defined in language $\mathcal{L}_{\Box}:=\mathcal{L}\setminus\{\Diamond\}$ by adding to IPL the rule $\mathsf{E_{\Box}}$ and any combination of axioms $\mathsf{M}_{\Box}$, $\mathsf{C}_{\Box}$ and $\mathsf{N}_{\Box}$. The $\Diamond$-family is instead defined in language $\mathcal{L}_{\Diamond}:=\mathcal{L}\setminus\{\Box\}$ by adding to IPL the rule $\mathsf{E_{\Diamond}}$ and any combination of axioms $\mathsf{M}_{\Diamond}$ and $\mathsf{N}_{\Diamond}$. It is work remarking that we don’t consider intuitionistic non-normal modal logics containing axiom $\mathsf{C}_{\Diamond}$. We denote the resulting logics by, respectively, $\Box$-IE∗ and $\Diamond$-IE∗, where E∗ replaces any system of the classical cube (for $\Diamond$-logics, any system non containing $\mathsf{C}_{\Diamond}$).

Notice that, having rejected the definability of the lacking modality, $\Box$- and $\Diamond$-logics are distinct, as $\Box$ and $\Diamond$ behave differently. Moreover, as a consequence of the fact that the systems in the classical cube are pairwise non-equivalent, we have that the $\Box$-family contains eight distinct logics, while the $\Diamond$-family contains four distinct logics (something not derivable in a classical system is clearly not derivable in the corresponding intuitionistic system). It is also worth noticing that, as it happens in the classical case, axioms $\mathsf{M}_{\Box}$, $\mathsf{M}_{\Diamond}$ and $\mathsf{N}_{\Box}$ are interderivable, respectively, with rules $\mathsf{Mon_{\Box}}$, $\mathsf{Mon_{\Diamond}}$ and $\mathsf{Nec}$, and that $\mathsf{K}_{\Box}$ is derivable from $\mathsf{M}_{\Box}$ and $\mathsf{C}_{\Box}$ (as the standard derivations are intuitionistically valid).

3.2 Sequent calculi

We now present sequent calculi for intuitionistic non-normal monomodal logics. The calculi are defined as modal extensions of a given sequent calculus for IPL. We take $\mathsf{G3ip}$ as base calculus (Figure 4), and extend it with suitable combinations of the modal rules in Figure 5. The $\Box$-rules can be compared with the rules given in Lavendhomme and Lucas [15], where sequent calculi for classical non-normal modal logics are presented. However, our rules are slightly different as (i) they have a single formula in the right-hand side of sequents; and (ii) contexts are added to the left-hand side of sequents appearing in the conclusion. Restriction (i) is adopted in order to have single-succedent calculi (as $\mathsf{G3ip}$ is), while with (ii) we implicitly embed weakening in the application of the modal rules. We consider the sequent calculi to be defined by the modal rules that are added to $\mathsf{G3ip}$. The calculi are the following.

[TABLE]

Notice that - as in Lavendhomme and Lucas [15] - axiom $\mathsf{C}_{\Box}$ doesn’t have a corresponding sequent rule, but it is captured by modifying the rules $\mathsf{E_{\Box}^{seq}}$ and $\mathsf{M_{\Box}^{seq}}$. In particular, these rules are replaced by $\mathsf{E_{\Box}C^{seq}}$ and $\mathsf{M_{\Box}C^{seq}}$, respectively, that are the generalisations of $\mathsf{E_{\Box}^{seq}}$ and $\mathsf{M_{\Box}^{seq}}$ with $n$ principal formulas (instead of just one) in the left-hand side of sequents. Observe that $\mathsf{E_{\Box}C^{seq}}$ and $\mathsf{M_{\Box}C^{seq}}$ are non-standard, as they introduce an arbitrary number of modal formulas with a single application, and that $\mathsf{E_{\Box}^{seq}}$ has in addition an arbitrary number of premisses. An other way to look at $\mathsf{E_{\Box}C^{seq}}$ and $\mathsf{M_{\Box}C^{seq}}$ is to see them as infinite sets of rules, each set containing a standard rule for any $n\geq 1$. Under the latter interpretation the calculi are anyway non-standard as they are defined by infinite sets of rules.

We now prove the admissibility of some structural rules, and then show the equivalence between the sequent calculi and the Hilbert systems.

Proposition 3.1**.**

The following weakening and contraction rules are height-preserving admissible in any monomodal calculus:

$\Gamma\Rightarrow B$

\mathsf{L}$$\mathsf{wk}

$\Gamma,A\Rightarrow B$

  

$\Gamma\Rightarrow$

\mathsf{R}$$\mathsf{wk}

$\Gamma\Rightarrow A$

  

$\Gamma,A,A\Rightarrow B$

$\mathsf{ctr}$

$\Gamma,A\Rightarrow B$

.

Proof.

By induction on $n$, we show that whenever the premiss of an application of \mathsf{L}$$\mathsf{wk}, \mathsf{R}$$\mathsf{wk} or $\mathsf{ctr}$ has a derivation of height $n$, then its conclusion has a derivation of the same height. As usual, the proof considers the last rule applied in the derivation of the premiss (when the premiss is not an initial sequent). For rules of $\mathsf{G3ip}$ the proof is standard. For modal rules, left and right weakening are easily handled. For istance, the premiss $\Gamma\Rightarrow$ of \mathsf{R}$$\mathsf{wk} is necessarily derived by $\mathsf{N_{\Diamond}^{seq}}$. Then $\Gamma$ contains a formula $\Diamond B$ that is principal in the application of $\mathsf{N_{\Diamond}^{seq}}$, which in turn has $B\Rightarrow$ as premiss. By a different application of $\mathsf{N_{\Diamond}^{seq}}$ to $B\Rightarrow$ we can derive $\Gamma\Rightarrow A$ for any $A$.

The proof is also immediate for contraction, where the most interesting case is possibly when both occurrences of $A$ in the premiss $\Gamma,A,A\Rightarrow B$ of $\mathsf{ctr}$ are principal in the last rule applied in its derivation. In this case, the last rule is either $\mathsf{E_{\Box}C^{seq}}$ or $\mathsf{M_{\Box}C^{seq}}$. If it is $\mathsf{M_{\Box}C^{seq}}$, then $A\equiv\Box C$ for some $C$, and the sequent is derived from $D_{1},...,D_{n},C,C\Rightarrow$ for some $\Box D_{1},...,\Box D_{n}$ in $\Gamma$. By i.h. we can apply $\mathsf{ctr}$ to the last sequent and obtain $D_{1},...,D_{n},C\Rightarrow$, and then by $\mathsf{M_{\Box}C^{seq}}$ derive sequent $\Gamma,A\Rightarrow B$, which is the conclusion of $\mathsf{ctr}$ (the proof is analogous for $\mathsf{E_{\Box}C^{seq}}$). ∎

We now show that the cut rule

$\Gamma\Rightarrow A$         $\Gamma,A\Rightarrow B$

$\mathsf{Cut}$

$\Gamma\Rightarrow B$

is admissible in any monomodal calculus. The proof is based on the following notion of weight of formulas:

Definition 3.1** (Weight of formulas).**

Function $w$ assigning to each formula $A$ its weight $w(A)$ is defined as follows: $w(\bot)=0$; $w(p)=1$; $w(A\circ B)=w(A)+w(B)+1$ for $\circ\equiv\land,\lor,\supset$; and $w(\Box A)=w(\Diamond A)=w(A)+2$.

Observe that, given the present definition, $\neg A$ has a smaller weight than $\Box A$ and $\Diamond A$. Although irrelevant to the next theorem, this will be used in Section 4 for the proof of cut elimination in bimodal calculi.

Theorem 3.2**.**

Rule $\mathsf{Cut}$ is admissible in any monomodal calculus.

Proof.

Given a derivation of a sequent with some applications of $\mathsf{Cut}$, we show how to remove any such application and obtain a derivation of the same sequent without $\mathsf{Cut}$. The proof is by double induction, with primary induction on the weight of the cut formula and subinduction on the cut height. We recall that, for any application of $\mathsf{Cut}$, the cut formula is the formula which is deleted by that application, while the cut height is the sum of the heights of the derivations of the premisses of $\mathsf{Cut}$.

We just consider the cases in which the cut formula is principal in the last rule applied in the derivation of both premisses of $\mathsf{Cut}$. Moreover, we treat explicitly only the cases in which both premisses are derived by modal rules, as the non-modal cases are already considered in the proof of cut admissibility for $\mathsf{G3ip}$, and because modal and non-modal rules don’t interact in any relevant way.

$\bullet$ ($\mathsf{E_{\Box}C^{seq}}$; $\mathsf{E_{\Box}C^{seq}}$).  Let $\Gamma_{1}=A_{1},...,A_{n}$ and $\Gamma_{2}=C_{1},...,C_{m}$. We have the following situation:

$\Gamma_{1}\Rightarrow B$  $B\Rightarrow A_{1}$  …  $B\Rightarrow A_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2}\Rightarrow\Box B$

     

$B,\Gamma_{2}\Rightarrow D$  $D\Rightarrow B$  $D\Rightarrow C_{1}$  …  $D\Rightarrow C_{m}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box B,\Box\Gamma_{1},\Box\Gamma_{2}\Rightarrow\Box D$

$\mathsf{Cut}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2}\Rightarrow\Box D$

The proof is converted as follows, with several applications of $\mathsf{Cut}$ with $B$ as cut formula, hence with a cut formula of smaller weight. First we derive

$\Gamma_{1}\Rightarrow B$

$\mathsf{wk}$

$\Gamma_{1},\Gamma_{2}\Rightarrow B$

     

$B,\Gamma_{2}\Rightarrow D$

$\mathsf{wk}$

$B,\Gamma_{1},\Gamma_{2}\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Gamma_{1},\Gamma_{2}\Rightarrow D$

Then for any $1\leq i\leq n$, we derive

$D\Rightarrow B$       

$B\Rightarrow A_{i}$

$\mathsf{wk}$

$B,D\Rightarrow A_{i}$

$\mathsf{Cut}$

$D\Rightarrow A_{i}$

Finally we can apply $\mathsf{E_{\Box}C^{seq}}$ as follows

$\Gamma_{1},\Gamma_{2}\Rightarrow D$  $D\Rightarrow A_{1}$  …  $D\Rightarrow A_{n}$  $D\Rightarrow C_{1}$  …  $D\Rightarrow C_{m}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2}\Rightarrow\Box D$

$\bullet$ ($\mathsf{M_{\Box}C^{seq}}$; $\mathsf{M_{\Box}C^{seq}}$) is analogous to ($\mathsf{E_{\Box}C^{seq}}$; $\mathsf{E_{\Box}C^{seq}}$). ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{E_{\Box}^{seq}}$) and ($\mathsf{M_{\Box}^{seq}}$; $\mathsf{M_{\Box}^{seq}}$) are the particular cases where $n,m=1$.

$\bullet$ ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{E_{\Box}C^{seq}}$).  Let $\Gamma_{1}=B_{1},...,B_{n}$. The situation is as follows:

$\Rightarrow A$

$\mathsf{N_{\Box}^{seq}}$

$\Gamma,\Box\Gamma_{1}\Rightarrow\Box A$

     

$A,\Gamma_{1}\Rightarrow C$  $C\Rightarrow A$  $C\Rightarrow B_{1}$  …  $C\Rightarrow B_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box A,\Box\Gamma_{1}\Rightarrow\Box C$

$\mathsf{Cut}$

$\Gamma,\Box\Gamma_{1}\Rightarrow\Box C$

The proof is converted as follows, with an application of $\mathsf{Cut}$ on a cut formula of smaller weight.

$\Rightarrow A$

$\mathsf{wk}$

$\Gamma_{1}\Rightarrow A$

       $A,\Gamma_{1}\Rightarrow C$

$\mathsf{Cut}$

$\Gamma_{1}\Rightarrow C$

       $C\Rightarrow B_{1}$  …  $C\Rightarrow B_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1}\Rightarrow\Box C$

$\bullet$ ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{M_{\Box}C^{seq}}$) is analogous to ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{E_{\Box}C^{seq}}$). ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{E_{\Box}^{seq}}$) and ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{M_{\Box}^{seq}}$) are the particular cases where $n=1$.

$\bullet$ ($\mathsf{E_{\Diamond}^{seq}}$; $\mathsf{E_{\Diamond}^{seq}}$) and ($\mathsf{M_{\Diamond}^{seq}}$; $\mathsf{M_{\Diamond}^{seq}}$) are analogous to ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{E_{\Box}^{seq}}$) and ($\mathsf{M_{\Box}^{seq}}$; $\mathsf{M_{\Box}^{seq}}$), respectively.

$\bullet$ ($\mathsf{E_{\Diamond}^{seq}}$; $\mathsf{N_{\Diamond}^{seq}}$).  We have

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Diamond}^{seq}}$

$\Gamma,\Diamond A\Rightarrow\Diamond B$

     

$B\Rightarrow$

$\mathsf{N_{\Diamond}^{seq}}$

$\Gamma,\Diamond A,\Diamond B\Rightarrow C$

$\mathsf{Cut}$

$\Gamma,\Diamond A\Rightarrow C$

which become

$A\Rightarrow B$       

$B\Rightarrow$

$\mathsf{wk}$

$A,B\Rightarrow$

$\mathsf{Cut}$

$A\Rightarrow$

$\mathsf{N_{\Diamond}^{seq}}$

$\Gamma,\Diamond A\Rightarrow C$

$\bullet$ ($\mathsf{M_{\Diamond}^{seq}}$; $\mathsf{N_{\Diamond}^{seq}}$) is analogous to ($\mathsf{E_{\Diamond}^{seq}}$; $\mathsf{N_{\Diamond}^{seq}}$). ∎

As a consequence of the admissibility of $\mathsf{Cut}$ we obtain the equivalence between the sequent calculi and the axiomatic systems.

Proposition 3.3**.**

Let L be any intuitionistic non-normal monomodal logic. Then calculus G.L is equivalent to system L.

Proof.

The axioms and rules of L are derivable in G.L. For the axioms of IPL and mp we can consider their derivations in $\mathsf{G3ip}$, as G.L enjoys admissibility of $\mathsf{Cut}$. Here we show that any modal rule allows us to derive the corresponding axiom:

$\Rightarrow A\supset B$

$\mathsf{wk}$

$A\Rightarrow A\supset B$

       $A,A\supset B\Rightarrow B$

$\mathsf{Cut}$

$A\Rightarrow B$

     

$\Rightarrow B\supset A$

$\mathsf{wk}$

$B\Rightarrow B\supset A$

       $B,B\supset A\Rightarrow A$

$\mathsf{Cut}$

$B\Rightarrow A$

$\mathsf{E_{\Box}^{seq}}$

$\Box A\Rightarrow\Box B$

\mathsf{R}$$\mathsf{\supset}

$\Rightarrow\Box A\supset\Box B$

$A,B\Rightarrow A$         $A,B\Rightarrow B$

$\mathsf{R\land}$

$A,B\Rightarrow A\land B$

     

$A,B\Rightarrow A$

$\mathsf{L\land}$

$A\land B\Rightarrow A$

     

$A,B\Rightarrow B$

$\mathsf{L\land}$

$A\land B\Rightarrow B$

$\mathsf{E_{\Box}C^{seq}}$

$\Box A,\Box B\Rightarrow\Box(A\land B)$

$\mathsf{L\land}$

$\Box A\land\Box B\Rightarrow\Box(A\land B)$

\mathsf{R}$$\mathsf{\supset}

$\Rightarrow\Box A\land\Box B\supset\Box(A\land B)$

$\Rightarrow\top$

$\mathsf{N_{\Box}^{seq}}$

$\Rightarrow\Box\top$

$\bot\Rightarrow$

$\mathsf{N_{\Diamond}^{seq}}$

$\Diamond\bot\Rightarrow$

$\mathsf{R\neg}$

$\Rightarrow\neg\Diamond\bot$

$A,B\Rightarrow A$

$\mathsf{L\land}$

$A\land B\Rightarrow A$

$\mathsf{M_{\Box}^{seq}}$

$\Box(A\land B)\Rightarrow\Box A$

\mathsf{R}$$\mathsf{\supset}

$\Rightarrow\Box(A\land B)\supset\Box A$

$A\Rightarrow A$

$\mathsf{R\lor}$

$A\Rightarrow A\lor B$

$\mathsf{M_{\Diamond}^{seq}}$

$\Diamond A\Rightarrow\Diamond(A\lor B)$

\mathsf{R}$$\mathsf{\supset}

$\Rightarrow\Diamond A\supset\Diamond(A\lor B)$

Moreover, the rules of G.L are derivable in L. As before, it suffices to consider the modal rules. The derivations are in most cases straightforward, we just consider the following.

$\bullet$  If L contains $\mathsf{N}_{\Box}$, then $\mathsf{N_{\Box}^{seq}}$ is derivable. Assume $\vdash_{\textsf{L}}A$. Then by $\mathsf{Nec}$ (which is equivalent to $\mathsf{N}_{\Box}$), $\vdash_{\textsf{L}}\Box A$.

$\bullet$  If L contains $\mathsf{N}_{\Diamond}$, then $\mathsf{N_{\Diamond}^{seq}}$ is derivable. Assume $\vdash_{\textsf{L}}A\supset\bot$. Since $\vdash_{\textsf{L}}\bot\supset A$, by $\mathsf{E_{\Diamond}^{seq}}$, $\vdash_{\textsf{L}}\Diamond A\supset\Diamond\bot$. Then $\vdash_{\textsf{L}}\neg\Diamond\bot\supset\neg\Diamond A$, and, since $\vdash_{\textsf{L}}\neg\Diamond\bot$, we have $\vdash_{\textsf{L}}\neg\Diamond A$.

$\bullet$  If L contains $\mathsf{C}_{\Box}$, then $\mathsf{E_{\Box}C^{seq}}$ is derivable. Assume $\vdash_{\textsf{L}}A_{1}\land...\land A_{n}\supset B$ and $\vdash_{\textsf{L}}B\supset A_{i}$ for all $1\leq i\leq n$. Then $\vdash_{\textsf{L}}B\supset A_{1}\land...\land A_{n}$. By $\mathsf{E_{\Box}}$, $\vdash_{\textsf{L}}\Box(A_{1}\land...\land A_{n})\supset\Box B$. In addition, by several applications of $\mathsf{C}_{\Box}$, $\vdash_{\textsf{L}}\Box A_{1}\land...\land\Box A_{n}\supset\Box(A_{1}\land...\land A_{n})$. Therefore $\vdash_{\textsf{L}}\Box A_{1}\land...\land\Box A_{n}\supset\Box B$. ∎

4 Intuitionistic non-normal bimodal logics

In this section we present intuitionistic non-normal modal logics with both $\Box$ and $\Diamond$. In this case we first present their sequent calculi, and then give equivalent axiomatisations.

A simple way to define intuitionistic non-normal bimodal logics would be by considering the fusion of two monomodal logics that belong respectively to the $\Box$- and to the $\Diamond$-family. Given two logics $\Box$-IE∗ and $\Diamond$-IE∗, their fusion in language $\mathcal{L}_{\Box}\cup\mathcal{L}_{\Diamond}$ is the smallest bimodal logics containing $\Box$-IE∗ and $\Diamond$-IE∗ (for the sake of simplicity we can assume that $\mathcal{L}_{\Box}$ and $\mathcal{L}_{\Diamond}$ share the same set of propositional variables, and differ only with respect to $\Box$ and $\Diamond$). The resulting logic is axiomatised simply by adding to IPL the modal axioms and rules of $\Box$-IE∗, plus the modal axioms and rules of $\Diamond$-IE∗.

It is clear, however, that in the resulting systems the modalities don’t interact at all, as there is no axiom involving both $\Box$ and $\Diamond$. On the contrary, finding suitable interactions between the modalities is often the main issue when intuitionistic bimodal logics are concerned. In that case, by reflecting the fact that in IPL connectives are not interderivable, it is usually required that $\Box$ and $\Diamond$ are not dual. We take the lacking of duality as an additional requirement for the definition of intuitionistic non-normal bimodal logics:

• (R3)

$\Box$ and $\Diamond$ are not interdefinable.

In order to define intuitionistic non-normal bimodal logics by the axiomatic systems, we would need to select the axioms between a plethora of possible formulas satisfying (R3). If we look for instance at the literature on intuitionistic normal modal logics, we see that many different axioms have been considered, and the reasons for the specific choices are varied. We take therefore a different way, and define the logics starting with their sequent calculi. In particular we proceed as follows.

• (i)

Intuitionistic non-normal bimodal logics are defined by their sequent calculi. The calculi are conservative extensions of a given calculus for IPL, and have as modal rules some characteristic rules of intuitionistic non-normal monomodal logics, plus some rules connecting $\Box$ and $\Diamond$. In addition, we require that the $\mathsf{Cut}$ rule is admissible. As usual, this means that adding rule $\mathsf{Cut}$ to the calculus does not extend the set of derivable sequents.

• (ii)

To the purpose of defining the basic systems, we consider only interactions between $\Box$ and $\Diamond$ that can be seen as forms of “weak duality principles”. In order to satisfy (R3), we require that these interactions are strictly weaker than $\mathsf{Dual_{\Box}}$ and $\mathsf{Dual_{\Diamond}}$, in the sense that $\mathsf{Dual_{\Box}}$ and $\mathsf{Dual_{\Diamond}}$ must not be derivable in any corresponding system.

• (iii)

We will distinguish logics that are monotonic and logics that are non-monotonic. Moreover, the logics will be distinguished by the different strength of interactions between the modalities.

The above points are realised in practice as follows. As before, we take $\mathsf{G3ip}$ (Figure 4) as base calculus for intuitionistic logics. This is extended with combinations of the characteristic rules of intuitionistic non-normal monomodal logics in Figure 5. The difference is that now the calculi contain both some rules for $\Box$ and some rules for $\Diamond$. In order to distinguish monotonic and non-monotonic logics, we require that the calculi contain either both $\mathsf{E_{\Box}^{seq}}$ and $\mathsf{E_{\Diamond}^{seq}}$ (in this case the corresponding logic will be non-monotonic), or both $\mathsf{M_{\Box}^{seq}}$ and $\mathsf{M_{\Diamond}^{seq}}$ (corresponding to monotonic logics). In addition, the calculi will contain some of the interaction rules in Figure 6. Since the logics are also distinguished according to the different strenghts of the interactions between the modalities, we require that the calculi contain either both $\mathsf{weak_{a}^{seq}}$ and $\mathsf{weak_{b}^{seq}}$, or both $\mathsf{neg_{a}^{seq}}$ and $\mathsf{neg_{b}^{seq}}$, or $\mathsf{str^{seq}}$.

In the following we present the sequent calculi for intuitionistic non-normal bimodal logics obtained by following our methodology. After that, for each sequent calculus we present an equivalent axiomatisation.

4.1 Sequent calculi

In the first part, we focus on sequent calculi for logics containing only axioms between $\mathsf{M}_{\Box}$, $\mathsf{M}_{\Diamond}$, $\mathsf{N}_{\Box}$ and $\mathsf{N}_{\Diamond}$ (that is, we don’t consider axiom $\mathsf{C}_{\Box}$). The calculi are obtained by adding to $\mathsf{G3ip}$ (Figure 4) suitable combinations of the modal rules in Figures 5 and 6. Although in principle any combination of rules could define a calculus, we accept only those calculi that satisfy the restrictions explained above. This entails in particular the need of studying cut elimination. As usual, the first step to do towards the study of cut elimination is to prove the admissibility of the other structural rules.

Proposition 4.1**.**

Weakening and contraction are height-preserving admissible in any sequent calculus defined by a combination of modal rules in Figures 5 and 6 that satisfies the restrictions explained above.

Proof.

By extending the proof of Proposition 3.1 with the examination of the interaction rules in Figure 6. Due to their form, however, it is immediate to verify that if the premiss of $\mathsf{wk}$ or $\mathsf{ctr}$ is derivable by any interaction rule, then the conclusion is derivable by the same rule. ∎

We can now examine the admissibility of $\mathsf{Cut}$. As it is stated by the following theorem, following our methodology we obtain 12 sequent calculi for intuitionistic non-normal bimodal logics.

Theorem 4.2**.**

We let the sequent calculi be defined by the set of modal rules which are added to $\mathsf{G3ip}$. The $\mathsf{Cut}$ rule is admissible in the following calculi:

[TABLE]

Moreover, letting $\mathsf{G^{*}}$ be any of the previous calculi, $\mathsf{Cut}$ is admissible in

[TABLE]

Proof.

The structure of the proof is the same as the proof of Theorem 3.2. Again, we consider only the cases where the cut formula is principal in the last rule applied in the derivation of both premisses, with the further restriction that the last rules are modal ones.

The combinations between $\Box$-rules, or between $\Diamond$-rules, have been shown in the proof of Theorem 3.2. Here we consider the possible combinations of $\Box$- or $\Diamond$-rules with rules for interaction.

$\bullet$ ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{weak_{a}^{seq}}$).  We have

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Box}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow\Box B$

     

$\Rightarrow B$         $C\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Box A,\Box B,\Diamond C\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

which become

$\Rightarrow B$         $B\Rightarrow A$

$\mathsf{Cut}$

$\Rightarrow A$

       $C\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

$\bullet$ ($\mathsf{E_{\Diamond}^{seq}}$; $\mathsf{weak_{a}^{seq}}$).  We have

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Diamond}^{seq}}$

$\Gamma,\Diamond A,\Box C\Rightarrow\Diamond B$

     

$\Rightarrow C$         $B\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Diamond A,\Box C,\Diamond B\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Diamond A,\Box C\Rightarrow D$

which become

$\Rightarrow C$       

$A\Rightarrow B$         $B\Rightarrow$

$\mathsf{Cut}$

$A\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Diamond A,\Box C\Rightarrow D$

$\bullet$ ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{weak_{b}^{seq}}$).  We have

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Box}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow\Box B$

     

$B\Rightarrow$         $\Rightarrow C$

$\mathsf{weak_{b}^{seq}}$

$\Gamma,\Box A,\Box B,\Diamond C\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

which become

$A\Rightarrow B$         $B\Rightarrow$

$\mathsf{Cut}$

$A\Rightarrow$

       $\Rightarrow C$

$\mathsf{weak_{b}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

$\bullet$ ($\mathsf{E_{\Diamond}^{seq}}$; $\mathsf{weak_{b}^{seq}}$).  We have

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Diamond}^{seq}}$

$\Gamma,\Diamond A,\Box C\Rightarrow\Diamond B$

     

$C\Rightarrow$         $\Rightarrow B$

$\mathsf{weak_{b}^{seq}}$

$\Gamma,\Diamond A,\Box C,\Diamond B\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Diamond A,\Box C\Rightarrow D$

which become

$\Rightarrow C$       

$\Rightarrow B$         $B\Rightarrow A$

$\mathsf{Cut}$

$\Rightarrow A$

$\mathsf{weak_{b}^{seq}}$

$\Gamma,\Diamond A,\Box C\Rightarrow D$

$\bullet$ ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{neg_{a}^{seq}}$).  We have:

$A\Rightarrow B$         $B\Rightarrow A$

$\mathsf{E_{\Box}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow\Box B$

     

$B,C\Rightarrow$         $\neg B\Rightarrow C$

$\mathsf{neg_{a}^{seq}}$

$\Gamma,\Box A,\Box B,\Diamond C\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

which is converted into the following derivation:

$A\Rightarrow B$

$\mathsf{wk}$

$A,C\Rightarrow B$

     

$B,C\Rightarrow A$

$\mathsf{wk}$

$A,B,C\Rightarrow$

$\mathsf{Cut}$

$A,C\Rightarrow$

     

$B\Rightarrow A$

$\neg A\Rightarrow\neg B$

     

$\neg B\Rightarrow C$

$\mathsf{wk}$

$\neg A,\neg B\Rightarrow C$

$\mathsf{Cut}$

$\neg A\Rightarrow C$

$\mathsf{neg_{a}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

Observe that the former derivation has two application of $\mathsf{Cut}$, both of them with a cut formula of smaller weight as, in particular, $w(\neg B)<w(\Box B)$ (cf. Definition 3.1).

$\bullet$ ($\mathsf{E_{\Box}^{seq}}$; $\mathsf{str^{seq}}$) is analogous to the next case ($\mathsf{M_{\Box}^{seq}}$; $\mathsf{str^{seq}}$).

$\bullet$ ($\mathsf{M_{\Box}^{seq}}$; $\mathsf{str^{seq}}$).  We have:

$A\Rightarrow B$

$\mathsf{M_{\Box}^{seq}}$

$\Gamma,\Box A,\Diamond C\Rightarrow\Box B$

     

$B,C\Rightarrow$

$\mathsf{str^{seq}}$

$\Gamma,\Box A,\Box B,\Diamond C\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

which is converted into the following derivation:

$A\Rightarrow B$

$\mathsf{wk}$

$A,C\Rightarrow B$

     

$B,C\Rightarrow$

$\mathsf{wk}$

$A,B,C\Rightarrow$

$\mathsf{Cut}$

$A,C\Rightarrow$

$\mathsf{str}$

$\Gamma,\Box A,\Diamond C\Rightarrow D$

$\bullet$ ($\mathsf{N_{\Box}^{seq}}$; $\mathsf{str^{seq}}$).  We have

$\Rightarrow A$

$\mathsf{N_{\Box}^{seq}}$

$\Gamma,\Diamond B\Rightarrow\Box A$

     

$A,B\Rightarrow$

$\mathsf{str^{seq}}$

$\Gamma,\Box A,\Diamond B\Rightarrow C$

$\mathsf{Cut}$

$\Gamma,\Diamond B\Rightarrow C$

which become

$\Rightarrow A$

$\mathsf{wk}$

$B\Rightarrow A$

       $A,B\Rightarrow$

$\mathsf{Cut}$

$B\Rightarrow$

$\mathsf{N_{\Diamond}^{seq}}$

$\Gamma,\Diamond B\Rightarrow C$

∎

It is worth noticing that all cut-free calculi containing rule $\mathsf{N_{\Box}^{seq}}$ also contain rule $\mathsf{N_{\Diamond}^{seq}}$. In fact, combinations of rules containing $\mathsf{N_{\Box}^{seq}}$ and not $\mathsf{N_{\Diamond}^{seq}}$ would give calculi where the $\mathsf{Cut}$ rule is not admissible. This is due to the form of the interaction rules, that for instance allow us to derive the sequent $\Diamond\bot\Rightarrow$ using $\mathsf{Cut}$ and $\mathsf{N_{\Box}^{seq}}$. A possible derivation is the following:

$\Rightarrow\top$

$\mathsf{N_{\Box}^{seq}}$

$\Diamond\bot\Rightarrow\Box\top$

     

$\Rightarrow\top$         $\bot\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Box\top,\Diamond\bot\Rightarrow$

$\mathsf{Cut}$

$\Diamond\bot\Rightarrow$

Instead, sequent $\Diamond\bot\Rightarrow$ doesn’t have any cut-free derivation where $\mathsf{N_{\Diamond}^{seq}}$ is not applied, as no rule different from $\mathsf{N_{\Diamond}^{seq}}$ has $\Diamond\bot\Rightarrow$ in the conclusion. We will consider in Section 7 a calculus containing $\mathsf{N_{\Box}^{seq}}$ and not $\mathsf{N_{\Diamond}^{seq}}$. As we shall see, that calculus has interaction rules of a different form.

An additional remark concerns the possible choices of interaction rules in presence of $\mathsf{M_{\Box}^{seq}}$ and $\mathsf{M_{\Diamond}^{seq}}$. In particular, we notice that whenever we take $\mathsf{M_{\Box}^{seq}}$ and $\mathsf{M_{\Diamond}^{seq}}$, rule $\mathsf{str^{seq}}$ is the only interaction that gives cut-free calculi. It can be interesting to consider a case of failure of cut elimination when other interaction rules are considered.

Example 4.1**.**

Sequent $\Box\neg p,\Diamond(p\land q)\Rightarrow$ is derivable from $\mathsf{M_{\Box}^{seq}}$ + $\mathsf{neg_{a}^{seq}}$ + $\mathsf{neg_{b}^{seq}}$ + $\mathsf{Cut}$, but it is not derivable from $\mathsf{M_{\Box}^{seq}}$ + $\mathsf{neg_{a}^{seq}}$ + $\mathsf{neg_{b}^{seq}}$ without $\mathsf{Cut}$. A possible derivation is as follows:

$\neg p,p\land q\Rightarrow$

$\mathsf{R\neg}$

$\neg p\Rightarrow\neg(p\land q)$

$\mathsf{M_{\Box}^{seq}}$

$\Box\neg p\Rightarrow\Box\neg(p\land q)$

$\mathsf{wk}$

$\Box\neg p,\Diamond(p\land q)\Rightarrow\Box\neg(p\land q)$

     

$\neg(p\land q),p\land q\Rightarrow$         $\neg(p\land q)\Rightarrow\neg(p\land q)$

$\mathsf{neg_{b}^{seq}}$

$\Box\neg(p\land q),\Diamond(p\land q)\Rightarrow$

$\mathsf{wk}$

$\Box\neg(p\land q),\Box\neg p,\Diamond(p\land q)\Rightarrow$

$\mathsf{Cut}$

$\Box\neg p,\Diamond(p\land q)\Rightarrow$

Let us now try to derive bottom-up the sequent without using $\mathsf{Cut}$. As last rule we can only apply $\mathsf{neg_{a}^{seq}}$ or $\mathsf{neg_{b}^{seq}}$, as they are the only rules with a conclusion of the right form. In the first case the premisses would be $\neg p,p\land q\Rightarrow$, and $\neg\neg p\Rightarrow p\land q$; while in the second case the premisses would be $\neg p,p\land q\Rightarrow$, and $\neg p\Rightarrow\neg(p\land q)$. It is clear, however, that in both cases the second premiss is not derivable.

We now consider sequent calculi for logics containing axiom $\mathsf{C}_{\Box}$. As it happens in the case of calculi for monomodal logics, $\mathsf{C}_{\Box}$ is not captured by adding a specific rule, but we need instead to modify most of the modal rules already given. In addition to the previous modifications of $\mathsf{E_{\Box}^{seq}}$ and $\mathsf{M_{\Box}^{seq}}$, we now need to modify also the interaction rules. In particular, we must take their generalisations that allow to introduce $n$ boxed formulas by a single application (rules in Figure 7). Rule $\mathsf{weak_{a}^{seq}}$ is an exception as the boxed formula which is principal in the rule application occurs as unboxed in the right-hand side of the premiss, and therefore doesn’t need to be changed.

As before, it can be easily shown that weakening and contraction are height-preserving admissible.

Proposition 4.3**.**

Weakening and contraction are height-preserving admissible in any sequent calculus defined by a combination of modal rules in Figures 5 and 7 that satisfies our restrictions.

Following our methodology we obtain again 12 sequent calculi, as it is stated by the following theorem:

Theorem 4.4**.**

The $\mathsf{Cut}$ rule is admissible in the following calculi:

[TABLE]

Moreover, letting $\mathsf{GC}^{*}$ be any of the previuos calculi, $\mathsf{Cut}$ is admissible in

[TABLE]

Proof.

As before, we only show some relevant cases.

$\bullet$ ($\mathsf{E_{\Box}C^{seq}}$; $\mathsf{weak_{a}^{seq}}$).  Let $\Gamma_{1}$ be the multiset $A_{1},...,A_{n}$, and $\Box\Gamma_{1}$ be $\Box A_{1},...,\Box A_{n}$. We have:

$\Gamma_{1}\Rightarrow B$  $B\Rightarrow A_{1}$  …  $B\Rightarrow A_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Diamond C\Rightarrow\Box B$

     

$\Rightarrow B$         $C\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box B,\Diamond C\Rightarrow D$

$\mathsf{Cut}$

$\Gamma,\Box\Gamma_{1},\Diamond C\Rightarrow D$

which become

$\Rightarrow B$         $B\Rightarrow A_{1}$

$\mathsf{Cut}$

$\Rightarrow A_{1}$

       $C\Rightarrow$

$\mathsf{weak_{a}^{seq}}$

$\Gamma,\Box A_{1},\Box A_{2},...,\Box A_{n},\Diamond C\Rightarrow D$

$\bullet$ ($\mathsf{E_{\Box}C^{seq}}$; $\mathsf{neg_{b}C^{seq}}$).  Let $\Gamma_{1}=A_{1},...,A_{n}$ and $\Gamma_{2}=C_{1},...,C_{k}$. We have:

$\Gamma_{1}\Rightarrow B$  $B\Rightarrow A_{1}$  …  $B\Rightarrow A_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow\Box B$

     

$B,\Gamma_{2},D\Rightarrow$  $\neg B\Rightarrow D$  $\neg C_{1}\Rightarrow D$  …  $\neg C_{k}\Rightarrow D$

$\mathsf{neg_{b}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box B,\Box\Gamma_{2},\Diamond D\Rightarrow E$

$\mathsf{Cut}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow E$

which is converted as follows: First we derive sequent $\Gamma_{1},\Gamma_{2},D\Rightarrow$ and, for all $1\leq i\leq n$, sequent $\neg A_{i}\Rightarrow D$ as follows:

$\Gamma_{1}\Rightarrow B$

$\mathsf{wk}$

$\Gamma_{1},\Gamma_{2}\Rightarrow B$

     

$B,\Gamma_{2},D\Rightarrow$

$\mathsf{wk}$

$B,\Gamma_{1},\Gamma_{2},D\Rightarrow$

$\mathsf{Cut}$

$\Gamma_{1},\Gamma_{2},D\Rightarrow$

  

$B\Rightarrow A_{i}$

$\neg A_{i}\Rightarrow\neg B$

     

$\neg B\Rightarrow D$

$\mathsf{wk}$

$\neg A_{i},\neg B\Rightarrow D$

$\mathsf{Cut}$

$\neg A_{i}\Rightarrow D$

Then we can apply $\mathsf{neg_{b}C^{seq}}$:

$\Gamma_{1},\Gamma_{2},D\Rightarrow$  $\neg A_{1}\Rightarrow D$  …  $\neg A_{n}\Rightarrow D$  $\neg C_{1}\Rightarrow D$  …  $\neg C_{k}\Rightarrow D$

$\mathsf{neg_{b}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow E$

$\bullet$ ($\mathsf{E_{\Box}C^{seq}}$; $\mathsf{strC^{seq}}$).  Let $\Gamma_{1}=A_{1},...,A_{n}$ and $\Gamma_{2}=C_{1},...,C_{k}$. We have:

$\Gamma_{1}\Rightarrow B$  $B\Rightarrow A_{1}$  …  $B\Rightarrow A_{n}$

$\mathsf{E_{\Box}C^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow\Box B$

     

$B,\Gamma_{2},D\Rightarrow$

$\mathsf{strC^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box B,\Box\Gamma_{2},\Diamond D\Rightarrow E$

$\mathsf{Cut}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow E$

which become

$\Gamma_{1}\Rightarrow B$

$\mathsf{wk}$

$\Gamma_{1},\Gamma_{2},D\Rightarrow B$

     

$B,\Gamma_{2},D\Rightarrow$

$\mathsf{wk}$

$\Gamma_{1},B,\Gamma_{2},D\Rightarrow$

$\mathsf{Cut}$

$\Gamma_{1},\Gamma_{2},D\Rightarrow$

$\mathsf{strC^{seq}}$

$\Gamma,\Box\Gamma_{1},\Box\Gamma_{2},\Diamond D\Rightarrow E$

$\bullet$ ($\mathsf{M_{\Box}C^{seq}}$; $\mathsf{strC^{seq}}$) is similar to the previous case. ∎

Notably, the cut-free calculi in Theorem 4.4 are the $\mathsf{C}_{\Box}$-versions of the cut-free calculi in Theorem 4.4. This means that, once the interaction rules are opportunely modified, the generalisation of the rules to $n$ principal formulas doesn’t give problems with respect to cut elimination.

We have also seen that rule $\mathsf{weak_{a}^{seq}}$ doesn’t need to be changed. Instead, if we don’t modify the other interaction rules we obtain calculi in which $\mathsf{Cut}$ is not eliminable, as it is shown by the following example.

Example 4.2**.**

Sequent $\Box p,\Box\neg p,\Diamond\top\Rightarrow$ is derivable by $\mathsf{M_{\Box}C^{seq}}$ + $\mathsf{weak_{b}^{seq}}$ + $\mathsf{Cut}$, but is not derivable by $\mathsf{M_{\Box}C^{seq}}$ + $\mathsf{weak_{b}^{seq}}$ without $\mathsf{Cut}$. The derivation is as follows:

$p,\neg p\Rightarrow\bot$

$\mathsf{M_{\Box}C^{seq}}$

$\Diamond\top,\Box p,\Box\neg p\Rightarrow\Box\bot$

     

$\bot\Rightarrow$         $\Rightarrow\top$

$\mathsf{weak_{b}^{seq}}$

$\Box p,\Box\neg p,\Box\bot,\Diamond\top\Rightarrow$

$\mathsf{Cut}$

$\Box p,\Box\neg p,\Diamond\top\Rightarrow$

Without $\mathsf{Cut}$ the sequent is instead not derivable, as the only applicable rule would be $\mathsf{weak_{b}^{seq}}$, but neither $p$ nor $\neg p$ is a contradiction.

4.2 Hilbert systems

For each sequent calculus we now define an equivalent Hilbert system. To this purpose, in addition the formulas in Figure 1, we also consider the axioms and rules in Figure 4.2. As before, the Hilbert systems are defined by the set of modal axioms and rules that are added to IPL. The systems are axiomatised as follows.