# A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus

Philippe Balbiani, Han Gao, Cigdem Gencer, Nicola Olivetti

► To cite this version:

Philippe Balbiani, Han Gao, Cigdem Gencer, Nicola Olivetti. A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus. 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), Feb 2024, Naples, Italy. pp.1–21, 10.4230/LIPIcs.CSL.2024.13 . hal-04457356

HAL Id: hal-04457356

https://amu.hal.science/hal-04457356v1

Submitted on 14 Feb 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
A Natural Intuitionistic Modal Logic:
Axiomatization and Bi-nested Calculus

Philippe Balbiani ☐

CNRS-INPT-UT3, IRIT, Toulouse, France

Han Gao ☐

Aix Marseille University, CNRS, LIS, Marseille, France

Çiğdem Gencer ☐

CNRS-INPT-UT3, IRIT, Toulouse, France

Nicola Olivetti ☐

Aix Marseille University, CNRS, LIS, Marseille, France

Abstract

We introduce **FIK**, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it.

**2012 ACM Subject Classification** Theory of computation → Modal and temporal logics; Theory of computation → Proof theory

**Keywords and phrases** Intuitionistic Modal Logic, Axiomatization, Completeness, Sequent Calculus.

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2024.

# 1 Introduction

Intuitionistic modal logic (**IML**) has a long history, starting from the pioneering work by Fitch [14] in the late 40's and Prawitz [22] in the 60's. Along the time, two traditions emerged that led to the study of two different families of systems. The first tradition, called *intuitionistic modal logics*, has been introduced by Fischer Servi [11, 12, 13], Plotkin and Stirling [21] and then systematized by Simpson [23]. Its main goal is to define an analogous of classical modalities justified from an intuitionistic meta-theory. The basic modal logic in this tradition, **IK**, is intended to be the intuitionistic counterpart of the minimal normal modal logic **K**. The second tradition leads to so-called *constructive modal logics* that are mainly motivated by their applications in computer science such as type-theoretic interpretations, verification and knowledge representation (contextual reasoning). This second tradition has been developed independently, first by Wijesekera [24] who proposed the system **CCDL** (Constructive Concurrent Dynamic logic), and then by Bellin, De Paiva, and Ritter [3], among others who proposed the logic **CK** (Constructive **K**) as the basic system for a constructive account of modality.

But putting aside the historical perspective, we can consider naively the following question: how can we build "from scratch" an **IML**? Since both modal logic and intuitionistic logic enjoy Kripke semantics, we can think of combining them together in order to define an intuitionistic modal logic. The simplest proposal is to consider Kripke models equipped with two relations, $\leq$ for intuitionistic implication and *R* for modalities. Propositional intuitionistic connectives (in particular implication) have their usual interpretations. We request that every valid formula or rule scheme of propositional intuitionistic logic **IPL** is also valid in **IML**. To reach this goal, we must ensure the *hereditary property*, which means

<figure><img src="image_2.png" /></figure>
XX:2 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

for any formula A, if A is forced by a world, it will also be forced also by all its uppers worlds, namely:

if $x \Vdash A$ and $x \le y$ then also $y \Vdash A$.

Thus the question becomes how to define modalities in order to ensure this property. The simplest solution is to build the hereditary property in the forcing conditions for $\square$ and $\diamond$:

(1) $x \Vdash \square A$ iff for all $x'$ with $x' \ge x$, for all $y$ with $Rx'y$ it holds $y \Vdash A$ and

(1') $x \Vdash \diamond A$ iff for all $x'$ with $x' \ge x$, there exists $y$ with $Rx'y$ s.t. $y \Vdash A$.

Observe that the definition of $\square A$ is reminiscent of the definition of $\forall$ in intuitionistic first-order logic. This logic is nothing else than the propositional part of Wijeskera's **CCDL** mentioned above and is *non-normal* as it does not contain all formulas of the form

$$ (DP) \diamond(A \lor B) \supset \diamond A \lor \diamond B. $$

Moreover, the logic does not satisfy the maximality criteria, one of the criteria stated by Simpson [23, Chapter 3] for a "good" **IML** since by adding any classical principle to it, we cannot get the classical normal modal logic **K**. In addition, **CCDL** has also been criticized for being *too strong*, as it still satisfies the *nullary* $\diamond$ distribution: $\diamond \perp \supset \perp$. By removing this last axiom, the constructive modal logic **CK** is obtained.

However, the opposite direction is also possible: we can make local the definition of $\diamond$ (pursuing the analogy with $\exists$ in intuitionistic first-order logic **FOIL**) exactly as in classical **K**, that is:

(2) $x \Vdash \diamond A$ iff there exists $y$ with $Rxy$ s.t. $y \Vdash A$.

In this way we recover $\diamond(A \lor B) \supset \diamond A \lor \diamond B$, making the logic *normal*. But there is a price to pay: nothing ensures that the hereditary property holds for $\diamond$-formulas. In order to solve this problem, we need to postulate some frame conditions. The most natural (and maybe the weakest) condition is simply that if $x' \ge x$ and $x$ has an *R*-accessible $y$ then also $x'$ must have an *R*-accessible $y'$ which refines $y$, which means $y' \ge y$. This condition is called *Forward Confluence* in [2]. It is not new as it is also called (F1) by Simpson [23, Chapter 3] and together with another frame conditions (F2) characterizes the very well-known system **IK** by Fischer-Servi and Simpson. Although from a meta-theoretical point of view **IK** can be justified by its standard translation in first-order intuitionistic logic, it does not seem to be the minimal system allowing the definition of modalities as in (1) and (2) above.

This paper attempts to fill the gap by studying a weaker logic whose forcing conditions are just (1) and (2) above and we assume *only* Forward Confluence. We call this logic **FIK** for *forward confluenced IK*. As far as we know, this logic has never been studied before. And we think it is well worth being studied: it seems to be the minimal logic defined by bi-relational models with forcing conditions (1) and (2) which preserves intuitionistic validity.

We first give a sound and complete Hilbert axiomatization of **FIK**. We show that **FIK** finds its place in the **IML**/constructive family: it is strictly stronger than **CCDL** (whence than **CK**) and strictly weaker than **IK**. At the same time **FIK** seems acceptable to be regarded as an **IML** since it satisfies all criteria proposed by Simpson, including the one about maximality: by adding any classical principle to **FIK**, we get classical normal modal logic **K**. All in all **FIK** seems to be a respectable intuitionistic modal logic and is a kind of "third way" between intuitionistic **IK** and constructive **CCDL/CK**.

We then investigate **FIK** from a proof-theoretic viewpoint. We propose a nested sequent calculus $C_{FIK}$ which makes use of two kinds of nestings: one for representing $\ge$-upper worlds
and the other for R-related worlds. A nested sequent calculus for (first-order) intuitionistic logic that makes use of the first type of nesting has been proposed in [15], so that our calculus can be seen as an extension of the propositional part of it. More recently in [8], the authors present a sequent calculus with the same kind of nesting to capture the IML logic given by $CCDL + (DP)^1$.

As mentioned, our calculus contains a double type of nesting. The use of this double nesting is somewhat analogous to the labelled calculus proposed in [19] which introduces the two relations on labels in the syntax. However, the essential ingredient of the calculus $C_{FIK}$ is the interaction rule between the two kinds of nested sequents that captures the specific Forward Confluence condition.

We prove that the calculus $C_{FIK}$ provides a decision procedure for the logic FIK. In addition, since the rules of $C_{FIK}$ are invertible, we show that from a single failed derivation under a suitable strategy, it is possible to extract a finite countermodel of the formula or sequent at the root of the derivation. This result allows us to obtain a constructive proof of the finite model property, which means if a formula is not valid then it has a finite countermodel.

## 2 A natural intuitionistic modal logic

Firstly, we present the syntax and semantics of forward confluenced intuitionistic modal logic FIK. Secondly, we present an axiom system and we prove its soundness and completeness. Thirdly, we discuss whether FIK satisfies the properties that are expected from intuitionistic modal logics.

**► Definition 1 (Formulas).** The set $\mathcal{L}$ of all formulas (denoted A, B, etc.) is generated by the following grammar: $A ::= p | \bot | \top | (A \land A) | (A \lor A) | (A \supset A) | \Box A | \Diamond A$ where p ranges over a countable set of atomic propositions At. We omit parentheses for readability. For all formulas A, we write $\neg A$ instead of $A \supset \bot$. For all formulas A, B, we write $A \equiv B$ instead of $(A \supset B) \land (B \supset A)$. The size of a formula A is denoted $|A|$.

**► Definition 2 (Bi-relational model).** A bi-relational model is a quadruple $\mathcal{M} = (W, \leq, R, V)$ where W is a nonempty set of worlds, $\leq$ is a pre-order on W, R is a binary relation on W and V : W $\to \wp(At)$ is a valuation on W satisfying the following hereditary condition:

$$ \forall x, y \in W, (x \leq y \Rightarrow V(x) \subseteq V(y)). $$

The triple $(W, \leq, R)$ is called a frame. For all $x, y \in W$, we write $x \geq y$ instead of $y \leq x$. Moreover, we say "y is a successor of x" when Rxy.

It is worth mentioning that an upper world of a successor of a world is not necessarily a successor of an upper world of that world. However, from now on in this paper, we only consider models $\mathcal{M} = (W, \leq, R, V)$ that satisfy the following condition called Forward Confluence as in [2]:

$$ (\mathbf{FC}) \quad \forall x, y \in W, (\exists z \in W, (x \geq z \ \& \ Rzy) \Rightarrow \exists t \in W, (Rxt \ \& \ t \geq y)). $$

**► Definition 3 (Forcing relation).** Let $\mathcal{M} = (W, \leq, R, V)$ be a bi-relational model and $w \in W$. The forcing conditions are the usual ones for atomic propositions and for formulas constructed by means of the connectives $\bot, \top, \land$ and $\lor$. For formulas constructed by means of the connectives $\supset, \sqsubseteq$ and $\diamond$, the forcing conditions are as follows:

<footnote n="1">¹ A calculus for IK with the same kind of nesting was also preliminarily considered in [?]</footnote>
XX:4 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

1

M, w ⊨ B ⊃ C iff for all w' ∈ W with w ≤ w' and M, w' ⊨ B, M, w' ⊨ C;

M, w ⊨ □B iff for all w', v' ∈ W with w ≤ w' and Rw'v', v' ⊨ B;

M, w ⊨ ◊B iff there exists v ∈ W with Rvv and M, v ⊨ B.

We also abbreviate M, w ⊨ A as w ⊨ A if the model is clear from the context.

**Proposition 4.** Let (W, ≤, R, V) be a bi-relational model. For all formulas A in L and for all x, y ∈ W with x ≤ y, x ⊨ A implies y ⊨ A.

Proposition 4 is proved by induction on the size of A using (FC) for the case of A = ◊B.

**Definition 5 (Validity).** A formula A in L is valid, denoted ▽ A, if for any bi-relational model M and any world w in it, M, w ⊨ A. Let **FIK** be the set of all valid formulas.

Obviously, **FIK** contains all standard axioms of **IPL**. Moreover, **FIK** is closed with respect to the following inference rules:

$$ \frac{p \supset q, p}{q} (\mathbf{MP}) \quad \frac{p}{\Box p} (\mathbf{NEC}) $$

Finally, **FIK** contains the following formulas:

$$ (\mathbf{K}_{\square}) \Box (p \supset q) \supset (\Box p \supset \Box q), $$

$$ (\mathbf{K}_{\diamond}) \Box (p \supset q) \supset (\diamond p \supset \diamond q), $$

$$ (\mathbf{N}) \neg \diamond \perp, $$

$$ (\mathbf{DP}) \diamond (p \lor q) \supset \diamond p \lor \diamond q, $$

$$ (\mathbf{wCD}) \Box (p \lor q) \supset ((\diamond p \supset \Box q) \supset \Box q). $$

We only show the validity of (wCD). Suppose ▷ (p ∨ q) ⊃ ((◊p ⊃ □q) ⊃ □q). Hence, there exists a model (W, ≤, R, V) and w ∈ W such that w ⊨ □(p ∨ q), w ⊨ ◊p ⊃ □q and w ▷□q. Thus, let u, v ∈ W be such that w ≤ u, Ruv and v ▷□q. Since w ⊨ □(p ∨ q), v ⊨ p ∨ q. Since v ▷□q, v ⊨ p. Since Ruv, u ⊨ ◊p. Since w ⊨ ◊p ⊃ □q and w ≤ u, u ⊨ ◊p ⊃ □q. Since u ⊨ ◊p, u ⊨ □q. Since Ruv, v ⊨ q: a contradiction.

**Definition 6 (Axiom system).** Let $\mathbf{D}_{\mathbf{FIK}}$ be the Hilbert-style axiom system consisting of all standard axioms of IPL, the inference rules (MP) and (NEC) and the formulas $(\mathbf{K}_{\square})$, $(\mathbf{K}_{\diamond})$, $(\mathbf{N})$, $(\mathbf{DP})$ and $(\mathbf{wCD})$ considered as axioms. Derivations are defined as usual. For all formulas A, we write $\vdash A$ when A is $\mathbf{D}_{\mathbf{FIK}}$-derivable. The set of all $\mathbf{D}_{\mathbf{FIK}}$-derivable formulas will also be denoted $\mathbf{D}_{\mathbf{FIK}}$.

The formulas $(\mathbf{K}_{\square})$, $(\mathbf{K}_{\diamond})$, $(\mathbf{DP})$ and $(\mathbf{N})$ are not new, seeing that they have already been used by many authors as axioms in multifarious variants of IML. As for the formula (wCD), as far as we are aware, it is used here for the first time as an axiom of an IML variant. Indeed, (wCD) is derivable in IK. Moreover, it is a weak form of the *Constant Domain axiom (CD)* : □(p ∨ q) ⊃ ◊p ∨ □q used in [2]. In other respect, (wCD) is derivable in IK, whereas it is not derivable in CCDL/CK. As for the IK axiom (◊p ⊃ □q) ⊃ □(p ⊃ q), it is not in **FIK** as it will be also constructively shown by using the calculus presented in next section. Therefore, we get $CK \subset CCDL \subset FIK \subset IK$. We can consider also the logic CCDL + (DP) (= CK + (N) + (DP)) recently studied in [8], according to the results in that paper, we get that CCDL + (DP) ⊂ FIK.

**Theorem 7 (Soundness).** $\mathbf{D}_{\mathbf{FIK}} \subseteq \mathbf{FIK}$, i.e. for all formulas A, if $\vdash A$ then $\vdash A$.
Theorem 7 can be proved by induction on the length of the derivation of A. Later, we will prove the converse inclusion (Completeness) saying that **FIK** ⊆ **D**<sub>FIK</sub>. At the heart of our proof of completeness, will be the concept of theory.

**Definition 8 (Theories).** A theory is a set of formulas containing $\mathbf{D}_{\mathbf{FIK}}$ and closed with respect to $\mathbf{MP}$. A theory $\Gamma$ is proper if $\perp \notin \Gamma$. A proper theory $\Gamma$ is prime if for all formulas $A, B$, if $A \lor B \in \Gamma$ then either $A \in \Gamma$, or $B \in \Gamma$. For all theories $\Gamma$ and for all formulas $A$, let $\Gamma + A = \{B \in \mathcal{L} : A \supset B \in \Gamma\}$ and $\Box\Gamma = \{A \in \mathcal{L} : \Box A \in \Gamma\}$.

Obviously, $\mathbf{D}_{\mathbf{FIK}}$ is the least theory and $\mathcal{L}$ is the greatest theory. Moreover, for all theories $\Gamma$, $\Gamma$ is proper if and only if $\Gamma \neq \mathcal{L}$ if and only if $\diamond \perp \notin \Gamma$.

**Lemma 9.** For all theories $\Gamma$ and for all formulas $A$, (i) $\Gamma + A$ is the least theory containing $\Gamma$ and $A$; (ii) $\Gamma + A$ is proper if and only if $\neg A \notin \Gamma$; (iii) $\Box\Gamma$ is a theory.

Lemma 9 can be proved by using standard axioms of **IPL**, inference rules (**MP**) and (**NEC**) and axiom $\mathbf{K}_{\square}$.

**Lemma 10 (Lindenbaum's Lemma).** Let $A$ be a formula. If $A \notin \mathbf{D}_{\mathbf{FIK}}$ then there exists a prime theory $\Gamma$ such that $A \notin \Gamma$.

**Definition 11 (Canonical model).** Let $\bowtie$ be the binary relation between sets of formulas such that for all sets $\Delta, \Lambda$ of formulas, $\Delta \bowtie \Lambda$ iff for all formulas $B$, the following conditions hold: (i) if $\Box B \in \Delta$ then $B \in \Lambda$ and (ii) if $B \in \Lambda$ then $\diamond B \in \Delta$.

Let $(W_c, \leq_c, R_c)$ be the frame such that $W_c$ is the set of all prime theories, $\leq_c$ is the inclusion relation on $W_c$ and $R_c$ is the restriction of $\bowtie$ to $W_c$. For all $\Gamma, \Delta \in W_c$, we write "$\Gamma \supseteq_c \Delta$" instead of "$\Delta \leq_c \Gamma$". Let $V_c : W_c \to \wp(At)$ be the valuation on $W_c$ such that for all $\Gamma$ in $W_c$, $V_c(\Gamma) = \Gamma \cap At$.

By Theorem 7, $\perp \notin \mathbf{D}_{\mathbf{FIK}}$. Hence, by Lemma 10, $W_c$ is nonempty.

**Lemma 12.** $(W_c, \leq_c, R_c, V_c)$ satisfies the frame condition (**FC**).

The proof of the completeness will be based on the following lemmas.

**Lemma 13 (Existence Lemma).** Let $\Gamma$ be a prime theory. Let $B, C$ be formulas.

1. If $B \supset C \notin \Gamma$ then there exists a prime theory $\Delta$ such that $\Gamma \subseteq \Delta$, $B \in \Delta$ and $C \notin \Delta$,

2. if $\Box B \notin \Gamma$ then there exists prime theories $\Delta, \Lambda$ such that $\Gamma \subseteq \Delta$, $\Delta \bowtie \Lambda$ and $B \notin \Lambda$,

3. if $\diamond B \in \Gamma$ then there exists a prime theory $\Delta$ such that $\Gamma \bowtie \Delta$ and $B \in \Delta$.

**Lemma 14 (Truth Lemma).** For all formulas $A$ and for all $\Gamma \in W_c$, $A \in \Gamma$ if and only if $\Gamma \models A$.

The proof of Lemma 14 can be done by induction on the size of $A$. The case when $A$ is an atomic proposition is by definition of $V_c$. The cases when $A$ is of the form $\perp$, $\top$, $B \wedge C$ and $B \vee C$ are as usual. The cases when $A$ is of the form $B \supset C$, $\Box B$ and $\diamond B$ use the Existence Lemma.

As for the proof of Theorem 15, it can be done by contraposition. Indeed, if $\not\models A$ then by Lemma 10, there exists a prime theory $\Gamma$ such that $A \notin \Gamma$. Thus, by Lemma 14, $\Gamma \not\models A$. Consequently, $\models A$.

**Theorem 15 (Completeness).** $\mathbf{FIK} \subseteq \mathbf{D}_{\mathbf{FIK}}$, i.e. for all formulas $A$, if $\models A$ then $\vdash A$.
XX:6 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

As mentioned above, there exists many variants of **IML**. Therefore, one may ask how
natural is the variant we consider here. Simpson [23, Chapter 3] discusses the formal features
that might be expected of an **IML L**:

$(C_1)$ **L** is conservative over **IPL**,

$(C_2)$ **L** contains all substitution instances of **IPL** and is closed under (**MP**),

$(C_3)$ for all formulas $A, B$, if $A \lor B$ is in **L** then either $A$ is in **L**, or $B$ is in **L**,

$(C_4)$ the addition of the law of excluded middle to $\mathbf{L}$ yields modal logic $\mathbf{K}$,

$(C_5)$ □ and ◊ are independent in $\mathbf{L}$.

The fact that $\mathbf{D}_{\text{FIK}}$ satisfies features $(C_1)$ and $(C_2)$ is an immediate consequence of Theorems 7 and 15. The fact that $\mathbf{D}_{\text{FIK}}$ satisfies feature $(C_3)$ will be proved in Section 3. Concerning feature $(C_4)$, let $\mathbf{D}_{\text{FIK}}^+$ be the Hilbert-style axiom system consisting of $\mathbf{D}_{\text{FIK}}$ plus the law $p \lor \neg p$ of excluded middle. The set of all $\mathbf{D}_{\text{FIK}}^+$-derivable formulas will also be denoted $\mathbf{D}_{\text{FIK}}^+$. Obviously, $\mathbf{D}_{\text{FIK}}^+$ contains all substitution instances of $\mathbf{CPL}$ and is closed under (MP). Moreover, it contains all substitution instances of $(\mathbf{K}_{\square})$ and is closed under (NEC). Therefore, in order to prove that $\mathbf{D}_{\text{FIK}}$ satisfies feature $(C_4)$, it suffices to prove

► **Lemma 16.** $\diamond p \equiv \neg\Box\neg p$ is in $\mathbf{D}_{\text{FIK}}^{+}$.

The fact that $\mathbf{D}_{\text{FIK}}$ satisfies feature $(C_5)$ is a consequence of

► **Lemma 17.** Let $p$ be an atomic proposition. There exists no $\Box$-free $A$ such that $\Box p \equiv A$ is in $\mathbf{D}_{\text{FIK}}$ and there exists no $\Diamond$-free $A$ such that $\Diamond p \equiv A$ is in $\mathbf{D}_{\text{FIK}}$.

Consequently, $\mathbf{D}_{\text{FIK}}$ can be considered as a natural intuitionistic modal logic.

3 A bi-nested sequent calculus

In this section, we present a bi-nested calculus for **FIK**. The calculus is two-sided and it makes use of two kinds of nestings, also called blocks $\langle\cdot\rangle$ and $[\cdot]$. The former is called an *implication* block and the latter a *modal* block. The intuition is that implication blocks correspond to upper worlds while modal blocks correspond to *R*-successors in a bi-relational model. The calculus we present is a conservative extension (with some notational change) of the nested sequent calculus for **IPL** presented in [15].

► **Definition 18 (Bi-nested sequent).** A bi-nested sequent *S* is defined as follows:

■ ⇒ is a bi-nested sequent (the empty sequent);

■ Γ ⇒ $B_1, \dots, B_k, [S_1], \dots, [S_m], \langle T_1 \rangle, \dots, \langle T_n \rangle$ is a bi-nested sequent if $S_1, \dots, S_m, T_1, \dots, T_n$ are bi-nested sequents where $m, n \ge 0$, and Γ is a finite (possibly empty) multi-set of formulas and $B_1, \dots, B_k$ are formulas.

We use $S, T$ to denote bi-nested sequents and to simplify wording we will call bi-nested
sequents simply by sequents in the rest of this paper. We denote by $|S|$ the size of a sequent
$S$ intended as the length of $S$ as a string of symbols.

As usual with nested calculi, we need the notion of context in order to specify the rules,
as they can be applied to sequents occurring inside other sequents. A *context* is of the form
$G\{\},$ in which $G$ is a part of a sequent, $\{\cdot\}$ is regarded as a placeholder that needs to be
filled by another sequent in order to complete $G$. $G\{S\}$ is the sequent obtained by replacing
the occurrence of the symbol $\{\}$ in $G\{\}$ by the sequent $S$.
**► Definition 19 (Context).** A context $G\{\}$ is inductively defined as follows:

- $\{\}$ is a context (the empty context).

- if $\Gamma \Rightarrow \Delta$ is a sequent and $G'\{\}$ is a context then $\Gamma \Rightarrow \Delta$, $\langle G'\{\} \rangle$ is a context.

- if $\Gamma \Rightarrow \Delta$ is a sequent and $G'\{\}$ is a context then $\Gamma \Rightarrow \Delta$, $[G'\{\}]$ is a context.

For example, given a context $G\{\} = A \wedge B, \Box C \Rightarrow \langle \Box A \Rightarrow [\Rightarrow B] \rangle, [\{\}]$ and a sequent $S = A \Rightarrow \Delta, [C \Rightarrow B]$, we have $G\{S\} = A \wedge B, \Box C \Rightarrow \langle \Box A \Rightarrow [\Rightarrow B] \rangle, [A \Rightarrow \Delta, [C \Rightarrow B]]$.

The two types of blocks interact by the (inter) rule. In order to define this rule, we need the following:

**► Definition 20 (\*-operator).** Let $\Lambda \Rightarrow \Theta$ be a sequent, we define $\Theta^*$ as follows:

- $\Theta^* = \emptyset$ if $\Theta$ is $[\cdot]$-free;

- $\Theta^* = [\Phi_1 \Rightarrow \Psi_1^*], \dots, [\Phi_k \Rightarrow \Psi_k^*]$ if $\Theta = \Theta_0, [\Phi_1 \Rightarrow \Psi_1], \dots, [\Phi_k \Rightarrow \Psi_k]$ and $\Theta_0$ is $[\cdot]$-free.

By definition, given a sequent $\Lambda \Rightarrow \Theta$, $\Theta^*$ is a multi-set of modal blocks.

Denote the sequent $G\{S\}$ in the previous example for context by $\Lambda \Rightarrow \Theta$, then by definition, we can see $\Lambda \Rightarrow \Theta^* = A \wedge B, \Box C \Rightarrow [A \Rightarrow [C \Rightarrow]].$

Now we can give a bi-nested sequent calculus for **FIK** as follows.

**► Definition 21.** The calculus $C_{FIK}$ is given in Figure 1.

Axioms:

$$ \frac{\overline{G\{\Gamma, \perp \Rightarrow \Delta\}} (\perp_L)}{\overline{G\{\Gamma \Rightarrow \top, \Delta\}} (\top_R)} \quad \frac{\overline{G\{\Gamma, p \Rightarrow \Delta, p\}} (\mathrm{id})}{\overline{G\{\Gamma, \Gamma' \Rightarrow \Delta, \Gamma'' \Rightarrow \Delta\}}} $$

Logical rules:

$$ \frac{\overline{G\{A, B, \Gamma \Rightarrow \Delta\}} (\wedge_L)}{\overline{G\{A \wedge B, \Gamma \Rightarrow \Delta\}} (\wedge_R)} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, A\}} \quad \overline{G\{\Gamma \Rightarrow \Delta, B\}} (\wedge_R)}{\overline{G\{\Gamma \Rightarrow \Delta, A \wedge B\}} (\wedge_L)} $$

$$ \frac{\overline{G\{\Gamma, A \Rightarrow \Delta\}} \quad \overline{G\{\Gamma, B \Rightarrow \Delta\}} (\vee_L)}{\overline{G\{\Gamma, A \vee B \Rightarrow \Delta\}} (\vee_R)} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, A, B\}}}{\overline{G\{\Gamma \Rightarrow \Delta, A \vee B\}} (\vee_L)} $$

$$ \frac{\overline{G\{\Gamma, A \supset B \Rightarrow A, \Delta\}} \quad \overline{G\{\Gamma, B \Rightarrow \Delta\}} (\supset_L)}{\overline{G\{\Gamma, A \supset B \Rightarrow \Delta\}} (\supset_R)} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, \langle A \Rightarrow B \rangle\}} (\supset_R)}{\overline{G\{\Gamma \Rightarrow \Delta, A \supset B\}} (\supset_L)} $$

Modal rules:

$$ \frac{\overline{G\{\Gamma, \Box A \Rightarrow \Delta, [\Sigma, A \Rightarrow \Pi]\}} (\Box_L)}{\overline{G\{\Gamma, \Box A \Rightarrow \Delta, [\Sigma \Rightarrow \Pi]\}} (\Box_R)} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, \langle \Rightarrow [A] \rangle\}} (\Box_R)}{\overline{G\{\Gamma \Rightarrow \Delta, \Box A\}} (\Box_L)} $$

$$ \frac{\overline{G\{\Gamma \Rightarrow \Delta, [A \Rightarrow \}} (\diamond_L)}{\overline{G\{\Gamma, \diamond A \Rightarrow \Delta\}} (\diamond_R)} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, \diamond A, [\Sigma \Rightarrow \Pi, A]\}}}{\overline{G\{\Gamma \Rightarrow \Delta, \diamond A, [\Sigma \Rightarrow \Pi]\}} (\diamond_L) $$

Transferring and interactive rules:

$$ \frac{\overline{G\{\Gamma, \Gamma' \Rightarrow \Delta, \langle \Gamma', \Sigma \Rightarrow \Pi \rangle\}} (\text{trans})}{\overline{G\{\Gamma, \Gamma' \Rightarrow \Delta, \langle \Sigma \Rightarrow \Pi \rangle\}} (\text{inter})} \quad \frac{\overline{G\{\Gamma \Rightarrow \Delta, \langle \Sigma \Rightarrow \Pi, [\Lambda \Rightarrow \Theta^*] \rangle, [\Lambda \Rightarrow \Theta]\}} (\text{inter})}{\overline{G\{\Gamma \Rightarrow \Delta, \langle \Sigma \Rightarrow \Pi \rangle, [\Lambda \Rightarrow \Theta]\}} (\text{trans})} $$

<caption>Figure 1 $C_{FIK}$</caption>
We show that the calculus $C_{FIK}$ enjoys the disjunctive property, which means if $A \lor B$ is provable, then either $A$ or $B$ is provable. This fact is an immediate consequence of the following lemma. Its general form is due to the fact that backwards expansion of a sequent with empty antecedent will (only) treat/introduce formulas and implication blocks in the consequent.

**Lemma 25.** Suppose that a sequent $S = \Rightarrow A_1, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle$ is provable in $C_{FIK}$, where the $A_i$'s are formulas. Then either for some $A_i$, $\Rightarrow A_i$ is provable in $C_{FIK}$ or for some $G_j$, $\Rightarrow \langle G_j \rangle$ is provable in $C_{FIK}$.

Since $\Rightarrow A \lor B$ is provable if and only if $\Rightarrow A, B$ from the lemma we immediately obtain:

**Proposition 26.** For any formulas $A, B$, if $\Rightarrow A \lor B$ is provable in $C_{FIK}$, then either $\Rightarrow A$ or $\Rightarrow B$ is provable.

By the soundness and completeness of $C_{FIK}$ with respect to $FIK$ proved in the following, we will conclude that the logic $FIK$ enjoys the disjunctive property.

Next, we prove the soundness of the calculus $C_{FIK}$. To achieve this aim, we need to define the semantic interpretation of sequents, whence their validity. We first extend the forcing relation $\Vdash$ to sequents and blocks therein.

**Definition 27.** Let $\mathcal{M} = (W, \leq, R, V)$ be a bi-relational model and $x \in W$. The relation $\Vdash$ is extended to sequents as follows:

$$ 
\begin{array}{l}
\mathcal{M}, x \Vdash \emptyset \\
\mathcal{M}, x \Vdash [T] \text{ if for every } y \text{ with } Rxy, \mathcal{M}, y \Vdash T \\
\mathcal{M}, x \Vdash \langle T \rangle \text{ if for every } x' \text{ with } x \leq x', \mathcal{M}, x' \Vdash T \\
\mathcal{M}, x \Vdash \Gamma \Rightarrow \Delta \text{ if either } \mathcal{M}, x \Vdash \emptyset \text{ for some } A \in \Gamma \text{ or } \mathcal{M}, x \Vdash \emptyset \text{ for some } O \in \Delta
\end{array}
$$

We say $S$ is valid in $\mathcal{M}$ iff $\forall w \in W$, we have $\mathcal{M}, w \Vdash S$. $S$ is valid iff it is valid in every bi-relational model.

Whenever the model $\mathcal{M}$ is clear, we omit it and write simply $x \Vdash \emptyset$ for any object $O$, which can be a formula, a sequent or a block. Moreover, given a sequent $S = \Gamma \Rightarrow \Delta$, we write $x \Vdash \Delta$ if there is an $O \in \Delta$ s.t. $x \Vdash \emptyset$ and write $x \Vdash \Delta$ if the previous condition does not hold.

The following lemma gives a semantic meaning to the $*$-operation used in (inter).

**Lemma 28.** Let $\mathcal{M} = (W, \leq, R, V)$ be a bi-relational model and $x, x' \in W$ with $x \leq x'$. Let $S = \Gamma \Rightarrow \Delta$ be any sequent, if $x \Vdash \Delta$ then $x' \Vdash \Delta^*$.

In order to prove soundness we first show that the all rules are *forcing-preserving*.

**Lemma 29.** Given a model $\mathcal{M} = (W, \leq, R, V)$ and $x \in W$, for any rule (r) of the form $\frac{G\{S_1\} \quad G\{S_2\}}{G\{S\}}$ or $\frac{G\{S_1\}}{G\{S\}}$, if $x \Vdash G\{S_i\}$, then $x \Vdash G\{S\}$.

Proof of this lemma proceeds by induction on the structure of the context $G\{\}$. The base of the induction (that is $G = \emptyset$) is the important one, we check rule by rule and in the case of (inter) we make use of Lemma 28.

By Lemma 29, the soundness of $C_{FIK}$ is proved as usual by a straightforward induction on the length of derivations.

**Theorem 30 (Soundness).** If a sequent $S$ is provable in $C_{FIK}$, then it is valid.
## 4 Termination and completeness for C<sub>FIK</sub>

In this section, we provide a terminating proof-search procedure based on $C_{FIK}$, whence a decision procedure for FIK; it will then be used to prove that $C_{FIK}$ is complete with respect to FIK bi-relational semantics. Here is a roadmap: first we introduce a set-based variant of the calculus where all rules are cumulative (or kleen'ed), in the sense that principal formulas are kept in the premises. With this variant, we formulate saturation conditions on a sequent associated to each rule. Saturation conditions are needed for both termination and completeness: they are used to prevent "redundant" application of the rules as the source of non-termination. In the meantime saturation conditions also ensure that a saturated sequent satisfies the truth conditions specified by the semantics (which is presented in the truth lemma), so it can be seen as a countermodel.

The reformulation of the calculus by means of set-based sequents is motivated as usual by the following consideration: while multisets are the natural data-structure for any proof-system (at least with commutative $\wedge$, $\vee$), set-based sequents are needed to bound the size of sequents occurring in a derivation in terms of subsets of subformulas of the formula or sequent at the root of the derivation (see for instance [6]).

Thus, by first we present $CC_{FIK}$, a variant of $C_{FIK}$ where sequents are set-based rather than multi-set based and the rules are cumulative.

**Definition 31.** $CC_{FIK}$ acts on set-based sequents, where a set-based sequent $S = \Gamma \Rightarrow \Delta$ is defined as in definition 18, but $\Gamma$ is a set of formulas and $\Delta$ is a set of formulas and/or blocks (containing set-based sequents). The rules are as follows:

- It contains the rules $(\perp_L)$, $(\top_R)$, $(id)$, $(\Box_L)$, $(\Diamond_R)$, $(trans)$ and $(inter)$ of $C_{FIK}$.

- $(\supset_R)$ is replaced by the two rules:

$$ \text{if } A \in \Gamma \quad \frac{G\{\Gamma \Rightarrow \Delta, A \supset B, B\}}{G\{\Gamma \Rightarrow \Delta, A \supset B\}} (\supset'_{R_1}) \qquad \text{if } A \notin \Gamma \quad \frac{G\{\Gamma \Rightarrow \Delta, A \supset B, \langle A \Rightarrow B \rangle\}}{G\{\Gamma \Rightarrow \Delta, A \supset B\}} (\supset'_{R_2}) $$

- The other rules in $C_{FIK}$ are modified by keeping the principal formula in the premises. For example, the cumulative versions of $(\wedge_L)$, $(\supset_L)$, $(\Box_R)$ and $(\Diamond_L)$ are:

$$ \frac{G\{A, B, A \wedge B, \Gamma \Rightarrow \Delta\}}{G\{A \wedge B, \Gamma \Rightarrow \Delta\}} (\wedge'_L) \qquad \frac{G\{\Gamma, A \supset B \Rightarrow A, \Delta\} \quad G\{\Gamma, A \supset B, B \Rightarrow \Delta\}}{G\{\Gamma, A \supset B \Rightarrow \Delta\}} (\supset'_L) $$

$$ \frac{G\{\Gamma \Rightarrow \Delta, \Box A, \langle \Rightarrow [\Rightarrow A] \rangle\}}{G\{\Gamma \Rightarrow \Delta, \Box A\}} (\Box'_R) \qquad \frac{G\{\Gamma, \Diamond A \Rightarrow \Delta, [A \Rightarrow]\}}{G\{\Gamma, \Diamond A \Rightarrow \Delta\}} (\Diamond'_L) $$

The following proposition is a consequence of the admissibility of weakening and contraction $C_{FIK}$ (whole proof is standard).

**Proposition 32.** A sequent S is provable in $C_{FIK}$ if and only if S is provable in $CC_{FIK}$.

From now on we consider $CC_{FIK}$. We introduce the notion of structural inclusion between sequents. It is used in the definition of saturation conditions as well as the model construction presented at the end of the section.

**Definition 33** (Structural inclusion $\subseteq^S$). Let $\Gamma_1 \Rightarrow \Delta_1, \Gamma_2 \Rightarrow \Delta_2$ be two sequents. $\Gamma_1 \Rightarrow \Delta_1$ is said to be structurally included in $\Gamma_2 \Rightarrow \Delta_2$, denoted as $\Gamma_1 \Rightarrow \Delta_1 \subseteq^S \Gamma_2 \Rightarrow \Delta_2$, if:
- $\Gamma_1 \subseteq \Gamma_2$ and ;

- for each $[\Lambda_1 \Rightarrow \Theta_1] \in \Delta_1$, there exists $[\Lambda_2 \Rightarrow \Theta_2] \in \Delta_2$ such that $\Lambda_1 \Rightarrow \Theta_1 \subseteq^S \Lambda_2 \Rightarrow \Theta_2$.

It is easy to see that $\subseteq^S$ is reflexive and transitive; moreover if $\Gamma_1 \Rightarrow \Delta_1 \subseteq^S \Gamma_2 \Rightarrow \Delta_2$, then $\Gamma_1 \subseteq \Gamma_2$.

We define now the saturation conditions associated to each rule of $CC_{FIK}$.

**► Definition 34 (Saturation conditions).** Let $\Gamma \Rightarrow \Delta$ be a sequent where $\Gamma$ is a set of formulas and $\Delta$ is a set of formulas and blocks. Saturation conditions associated to a rule in the calculus are given as below.

$(\bot_L) \bot \notin \Gamma.$

$(\top_R) \top \notin \Delta.$

(id) At $\cap (\Gamma \cap \Delta)$ is empty.

$(\wedge_R) \text{ If } A \wedge B \in \Delta, \text{ then } A \in \Delta \text{ or } B \in \Delta.$

$(\wedge_L) \text{ If } A \wedge B \in \Gamma, \text{ then } A \in \Gamma \text{ and } B \in \Gamma.$

$(\vee_R) \text{ If } A \vee B \in \Delta, \text{ then } A \in \Delta \text{ and } B \in \Delta.$

$(\vee_L) \text{ If } A \vee B \in \Gamma, \text{ then } A \in \Gamma \text{ or } B \in \Gamma.$

$(\supset_R) \text{ If } A \supset B \in \Delta, \text{ then either } A \in \Gamma \text{ and } B \in \Delta, \text{ or there is } \langle\Sigma \Rightarrow \Pi\rangle \in \Delta \text{ with } A \in \Sigma \text{ and } B \in \Pi.$

$(\supset_L) \text{ If } A \supset B \in \Gamma, \text{ then } A \in \Delta \text{ or } B \in \Gamma.$

$(\Box_R) \text{ If } \Box A \in \Delta, \text{ then either there is } [\Lambda \Rightarrow \Theta] \in \Delta \text{ with } A \in \Theta, \text{ or there is } \langle\Sigma \Rightarrow [\Lambda \Rightarrow \Theta], \Pi\rangle \in \Delta \text{ with } A \in \Theta.$

$(\Box_L) \text{ If } \Box A \in \Gamma \text{ and } [\Sigma \Rightarrow \Pi] \in \Delta, \text{ then } A \in \Sigma.$

$(\diamond_R) \text{ If } \diamond A \in \Delta \text{ and } [\Sigma \Rightarrow \Pi] \in \Delta, \text{ then } A \in \Pi.$

$(\diamond_L) \text{ If } \diamond A \in \Gamma, \text{ then there is } [\Sigma \Rightarrow \Pi] \in \Delta \text{ with } A \in \Sigma.$

(trans) If $\Delta$ is of form $\Delta', \langle\Sigma \Rightarrow \Pi\rangle$, then $\Gamma \subseteq \Sigma$.

(inter) If $\Delta$ is of form $\Delta', \langle\Sigma \Rightarrow \Pi\rangle$, $[\Lambda \Rightarrow \Theta]$, then there is $[\Phi \Rightarrow \Psi] \in \Pi$ with $\Lambda \Rightarrow \Theta \subseteq^S \Phi \Rightarrow \Psi$.

Concerning (inter)-saturation, observe that $\Lambda \Rightarrow \Theta \subseteq^S \Lambda \Rightarrow \Theta^*$, thus this condition generalizes the expansion produced by the (inter)-rule.

**► Proposition 35.** Let $\Gamma \Rightarrow \Delta$ be a sequent saturated with respect to both (trans) and (inter). If $\langle\Sigma \Rightarrow \Pi\rangle \in \Delta$, then $\Gamma \Rightarrow \Delta \subseteq^S \Sigma \Rightarrow \Pi$.

In order to define a terminating proof-search procedure based on $CC_{FIK}$ (like for any calculus with cumulative rules), as usual we say that the backward application of a rule (R) to a sequent $S$ is redundant if $S$ satisfies the corresponding saturation condition for that application of (R) and we impose the following constraints:

(i) *No rule is applied to an axiom and*

(ii) *No rule is applied redundantly.*

However the above restrictions are not sufficient to ensure the termination of the procedure as the following example shows.

**► Example 36.** Let us consider the sequent $S = \Box a \supset \bot, \Box b \supset \bot \Rightarrow p$, where we abbreviate by $\Gamma$ the antecedent of $S$. Consider the following derivation, we only show the leftmost
XX:12 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

5

branch (the others succeed), we collapse some steps:

$$ \frac{\vdots}{(3) \Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a], \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle} $$

$$ \frac{\vdots}{(2) \Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a], \langle \Rightarrow [\Rightarrow b] \rangle \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle} (\Box_R) $$

$$ \frac{(1) \Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a] \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle}{\Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow [\Rightarrow a] \rangle, \langle \Gamma \Rightarrow [\Rightarrow b] \rangle} (\supset_L) \times 4 $$

$$ \frac{\Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow [\Rightarrow a] \rangle, \langle \Gamma \Rightarrow [\Rightarrow b] \rangle}{\Gamma \Rightarrow p, \Box a, \Box b, \langle \Rightarrow [\Rightarrow a] \rangle, \langle \Rightarrow [\Rightarrow b] \rangle} (\text{trans}) \times 2 $$

$$ \frac{\Gamma \Rightarrow p, \Box a, \Box b}{\Gamma \Rightarrow p} (\Box_R) \times 2 $$

Observe that in the first implication block of sequent (1) ($\Box_R$) can only be applied to $\Box b$, creating the nested block $\langle \Rightarrow [\Rightarrow b] \rangle$ in (2), as it satisfies the saturation condition for $\Box a$. This block will be further expanded to $\langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle$ in (3) that satisfies the saturation condition for $\Box b$, but not for $\Box a$, whence it will be further expanded, and so on. Thus the branch does not terminate.

In order to deal with this case of non-termination, intuitively we need to block the expansion of a sequent that occurs nested in another sequent whenever the former has already been expanded and the latter is "equivalent" to the former, in a sense that we will define. To accomplish this purpose we need to introduce a few notions.

**Definition 37** ($\in^{\langle \cdot \rangle}, \in^{[\cdot]}, \in^{+}$-relation). Let $\Gamma_1 \Rightarrow \Delta_1, \Gamma_2 \Rightarrow \Delta_2$ be two sequents. We denote $\Gamma_1 \Rightarrow \Delta_1 \in_0^{\langle \cdot \rangle} \Gamma_2 \Rightarrow \Delta_2$ if $\langle \Gamma_1 \Rightarrow \Delta_1 \rangle \in \Delta_2$. Let $\in^{\langle \cdot \rangle}$ be the transitive closure of $\in_0^{\langle \cdot \rangle}$. Relations $\in_0^{[\cdot]}$ and $\in^{[\cdot]}$ for modal blocks are defined similarly. Let $\in_0^+ = \in_0^{\langle \cdot \rangle} \cup \in_0^{[\cdot]}$ and finally let $\in^+$ be the reflexive-transitive closure of $\in_0^+$.

Observe that $S' \in^+ S$ is the same as: for some context $G$, $S = G\{S'\}$.

We introduce the operator $\sharp$ (to be compared with $*$ of Definition 20). Its purpose is to remove implication blocks from a sequent and retain all other formulas.

**Definition 38** ($\sharp$-operator). Let $\Lambda \Rightarrow \Theta$ be a sequent. We define $\Theta^\sharp$ as follows: (i) $\Theta^\sharp = \Theta$ if $\Theta$ is block-free; (ii) $\Theta^\sharp = \Theta_0^\sharp$, $[\Phi \Rightarrow \Psi^\sharp]$ if $\Theta = \Theta_0$, $[\Phi \Rightarrow \Psi]$; (iii) $\Theta^\sharp = \Theta_0^\sharp$ if $\Theta = \Theta_0$, $\langle \Phi \Rightarrow \Psi \rangle$.

As an example let $\Delta = b, [c \Rightarrow d, [e \Rightarrow f], \langle g \Rightarrow h \rangle], \langle t \Rightarrow [p \Rightarrow q] \rangle, [m \Rightarrow n]$, then $\Delta^\sharp = b, [c \Rightarrow d, [e \Rightarrow f]], [m \Rightarrow n]$, while $\Delta^* = [c \Rightarrow [e \Rightarrow]], [m \Rightarrow]$.

Intuitively, if a sequent $S = \Lambda \Rightarrow \Theta$ describes a model rooted in $S$ and specifies formulas forced and not forced in $S$, then $\Lambda \Rightarrow \Theta^\sharp$, describes the chains of R-related worlds to $S$ by specifying all formulas forced and not forced in each one of them, but ignores upper worlds in the pre-order, the latter being represented by implication blocks.

We use the $\sharp$-operator to define an equivalence relation between sequents. The equivalence relation will be used to detect loops in a derivation as in the example above.

**Definition 39** (Block-equivalence). Let $S_1, S_2$ be two sequents where $S_1 = \Gamma_1 \Rightarrow \Delta_1, S_2 = \Gamma_2 \Rightarrow \Delta_2$. We say $S_1$ is block-equivalent to $S_2$, denoted as $S_1 \simeq S_2$, if $\Gamma_1 = \Gamma_2$ and $\Delta_1^\sharp = \Delta_2^\sharp$.

In order to define a proof-search procedure, we divide rules of $CC_{\text{FIK}}$ into three groups and define correspondingly three levels of saturation.
(R1) basic rules: all propositional and modal rules except ($\supset_R$) and ($\Box_R$);

(R2) rules that transfer formulas and blocks into implication blocks: (trans) and (inter);

(R3) rules that create implication blocks: ($\Box_R$) and ($\supset_R$).

**► Definition 40 (Saturation).** Let $S = \Gamma \Rightarrow \Delta$ be a sequent and not an axiom. S is called:

- R1-saturated if $\Gamma \Rightarrow \Delta^\sharp$ satisfies all the saturation conditions of R1 rules;

- R2-saturated if S is R1-saturated and S satisfies saturation conditions of R2 rules for blocks $S_1 \in \mathring{\{\gamma\}}$ S and $S_2 \in \{\gamma\}$ S.

- R3-saturated if S is R2-saturated and S satisfies saturation conditions of R3 rules for formulas $\Box A, B \supset C \in \Delta$.

We can finally define when a sequent is blocked, the intention is that it will not be expanded anymore by the proof-search procedure.

**► Definition 41 (Blocked sequent).** Given a sequent $S$ and $S_1, S_2 \in S$, with $S_1 = \Gamma_1 \Rightarrow \Delta_1, S_2 = \Gamma_2 \Rightarrow \Delta_2$. We say $S_2$ is blocked by $S_1$ in $S$, if $S_1$ is R3-saturated, $S_2 \in \mathring{\{\gamma\}}$ $S_1$ and $S_1 \simeq S_2$. We say that a sequent $S'$ is blocked in $S$ if there exists $S_1 \in S$ such that $S'$ is blocked by $S_1$ in $S$.

Observe that if $S$ is finite, then for any $S' \in S$ checking whether $S'$ is blocked in $S$ can be effectively decided. We will say just that $S'$ is blocked when $S$ is clear.

**► Example 42.** We reconsider the example 36. The sequent (3) will be further expanded to

$$ (4) \quad \Gamma \Rightarrow p, \Box a, \Box b, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a] \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a] \rangle^{(ii)} \rangle^{(i)}, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle $$

We have marked by (i) and (ii) the relevant blocks. Observe that the sequent $S_2 = \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a]$ in the block marked (ii) is blocked by the sequent $S_1 = \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a], \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a] \rangle$ marked (i), since $S_1$ is R3-saturated, $S_2 \in \mathring{\{\gamma\}}$ $S_1$ and $S_1 \simeq S_2$, as in particular ($\Box a, \Box b, [\Rightarrow a], \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow b] \rangle, \langle \Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a] \rangle$)$^\sharp$ = ($\Gamma \Rightarrow \Box a, \Box b, [\Rightarrow a]$)$^\sharp$.

We finally define three global saturation conditions.

**► Definition 43 (Global saturation).** Let $S$ be a sequent and not an axiom. $S$ is called :

- global-R1-saturated if for each $T \in S$, $T$ is either R1-saturated or blocked;

- global-R2-saturated if for each $T \in S$, $T$ is either R2-saturated or blocked;

- global-saturated if for each $T \in S$, $T$ is either R3-saturated or blocked.

In order to specify the proof-search procedure, we make use of three sub-procedures that extend a given derivation $\mathcal{D}$ by expanding a leaf $S$, each procedure applies rules non-redundantly to some $T := \Gamma \Rightarrow \Delta \in S$, that we recall it means that $S = \mathcal{G}\{T\}$, for some context $G$. We define :

1. $\text{EXP1}(\mathcal{D}, S, T) = \mathcal{D}'$ where $\mathcal{D}'$ is the extension of $\mathcal{D}$ obtained by applying R1 rules to every formula in $\Gamma \Rightarrow \Delta^\sharp$.

2. $\text{EXP2}(\mathcal{D}, S, T) = \mathcal{D}'$ where $\mathcal{D}'$ is the extension of $\mathcal{D}$ obtained by applying R2-rules to blocks $\langle T_i \rangle, [T_j] \in \Delta$.

3. $\text{EXP3}(\mathcal{D}, S, T) = \mathcal{D}'$ where $\mathcal{D}'$ is the extension of $\mathcal{D}$ obtained by applying R3-rules to formulas $\Box A, A \supset B \in \Delta$.
XX:14 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

6

The three procedures are used as macro-steps in the proof search procedure defined
next. We are going to prove that the three sub-procedures terminate, this is stated in
proposition 46 below. Namely the claim is obvious for **EXP2**(*D*, *S*, *T*), **EXP3**(*D*, *S*, *T*) as
only finitely many blocks or formulas in *T* are processed. For **EXP1**(*D*, *S*, *T*), the claim
is less obvious, since the rules are applied also deeply in Γ ⇒ Δ<sup>‡</sup>. However, notice that
**EXP1** only applies the rules (both L and R) for ∧, ∨, ◊ and ⊃<sub>L</sub>, □<sub>L</sub> and ignores implication
blocks, thus **EXP1**(*D*, *S*, *T*) produces exactly the same expansion of *D* that we would obtain
by the same rules of a nested sequent calculus for classical modal logic **K** and we know
that it terminates (see [6], Lemma 7). However, in order to give a proof of the claim for
**EXP1**(*D*, *S*, *T*) we introduce the following definition.

**Definition 44.** *Given a sequent S, the tree T<sub>S</sub> is defined as follows: (i) the root of T<sub>S</sub> is S; (ii) if S<sub>1</sub> ∈<sub>0</sub><sup>[-]</sup> S<sub>2</sub>, then S<sub>1</sub> is a child of S<sub>2</sub>.*

We denote the height of $\mathcal{T}_S$ as $h(\mathcal{T}_S)$. It is easy to verify that $h(\mathcal{T}_S) \leq \mathrm{md}(S)$. Moreover we denote by $\mathrm{Sub}(A)$ the set of subformulas of a formula $A$ and for a sequent $S = \Gamma \Rightarrow \Delta$ we use the corresponding notations $\mathrm{Sub}(\Gamma)$, $\mathrm{Sub}(\Delta)$, $\mathrm{Sub}(S)$. Finally, we recall that $\mathrm{Card}(\mathrm{Sub}(S)) = O(|S|)$.

By estimating the size of the tree associated to a sequent, we can get the following *rough*
bound of the size of any sequent occurring in a derivation by R1-rules.

**Proposition 45.** Let $\mathcal{Do}$ be a derivation with root a non-axiomatic sequent $T = \Gamma \Rightarrow \Delta$
obtained by applying R1-rules to $\Gamma \Rightarrow \Delta^\sharp$, then any $T'$ occurring in $\mathcal{Do}$ has size $O(|T|^{|T|+1})$.

We can now prove proposition 46.

**Proposition 46.** *Given a finite derivation *D*, a finite leaf *S* of *D* and *T* ∈<sup>+</sup> *S*, then each *EXP1*(*D*, *S*, *T*), *EXP2*(*D*, *S*, *T*), *EXP3*(*D*, *S*, *T*) terminates by producing a finite expansion of *D* where all sequents in it are finite.*

**Proof.** We only prove the claim for **EXP1**(*D*, *S*, *T*), the other cases being obvious. To this
purpose we show that any derivation *Do*, with root Γ ⇒ Δ‡ and generated by R1-rules,
is finite. Then the claim follows since **EXP1**(*D*, *S*, *T*) is obtained simply by "appending"
*Do* to *D*, where we replace every sequent *T'* in *Do* by *G{**T'***}, as *S* = *G{**T*}*.
In order to
prove that *Do* is finite, notice that (i) all R1-rules are at most binary, (ii) the length of a
branch of *Do* is bounded by the size of the maximal sequent that can occur in it because of
non-redundancy restriction. But by proposition 45, every sequent *T'* in *Do* has a bounded
size (namely *O*(*|*T*|*|T|*<sup>+</sup>)), whence we get a bound on the length of any branch of *Do*. In
conclusion *Do* is a finitely-branching tree, whose branches have a finite length, whence it is
finite.
◀

We present below the proof-search procedure PROCEDURE(*A*), that given an input
formula *A* it returns either a proof of *A* or a finite derivation tree in which all non-axiomatic
leaves are global-saturated.

An important property of the proof-search procedure is that saturation and blocking are
preserved through sequent expansion, in other words they are *invariant* of the repeat loop of
the procedure.

**Lemma 47 (Invariant).** Let *S* be a leaf of a derivation *D* with root ⇒ *A*:
<caption>■ Algorithm 1 PROCEDURE(A)</caption>

Input: $D_0 := \Rightarrow A$
1 initialization $D := D_0$;
2 repeat
3   if all the leaves of $D$ are axiomatic then
4     return "PROVABLE" and $D$
5   else if all the non-axiomatic leaves of $D$ are global-saturated then
6     return "UNPROVABLE" and $D$
7   else
8     for all non-axiomatic leaves $S$ of $D$ that are not global-saturated
9       if $S$ is global-R2-saturated then
10        for all $T \in S$ such that $T$ is a $\in^{(\cdot)}$-minimal and not R3-saturated, check
11        whether $T$ is blocked in $S$, if not, let $D = \text{EXP3}(D, S, T)$
12      else if $S$ is global-R1-saturated then
13        for all $T \in S$ that is not R2-saturated, let $D = \text{EXP2}(D, S, T)$
14      else
15    for all $T \in S$ that is not R1-saturated let $D = \text{EXP1}(D, S, T)$
until FALSE;

1. Let $T \in S$, where $T = \Gamma \Rightarrow \Delta$, for every rule (R) if T satisfies the R-saturation condition on some formulas $A_i$ and/or blocks $\langle T_j \rangle$, $[T_k]$ before the execution of (the body of) the repeat loop (lines 3-14), then T satisfies the R-condition on the involved $A_i$, $\langle T_j \rangle$, $[T_k]$ after the execution of it.

2. Let $T \in S$, if T is blocked in S before the execution of (the body of) the repeat loop, then it is still so after it.

The last ingredient in order to prove termination is that in a derivation of a formula A there can be only finitely many non-blocked sequents.

**► Lemma 48.** Given a formula A, let $Seq(A)$ be the set of sequents that may occur in any possible derivation with root $\Rightarrow A$. Let $Seq(A)/\simeq$ be the quotient of $Seq(A)$ with respect to block-equivalence $\simeq$ as defined in Definition 39. Then $Seq(A)/\simeq$ is finite.

Intuitively, the termination of the procedure is based on the following argument: the procedure cannot run forever by building an infinite derivation. The reason is that the built derivation cannot contain any infinite branch, because (i) once that a sequent satisfies a saturation condition for a rule R, further expansions of it will still satisfy that condition (whence not reconsidered for the application of R), (ii) if a sequent is blocked, further application or rules cannot "unblock" it, (iii) the number of non-equivalent, whence unblocked sequents is finite.

**► Theorem 49 (Termination).** Let A be a formula. Proof-search for the sequent $\Rightarrow A$ terminates with a finite derivation in which any leaf is either an axiom or global-saturated.

[NICOLA: Add HERE a comment about DEPTH-FIRST and BREADTH FIRST PROCEDURE]

Next, we prove the completeness of $CC_{\text{FIK}}$. We show that given a finite global-saturated leaf $S$ of the derivation $D$ produced by `PROCEDURE(A)`, then we can define a countermodel $\mathcal{M}_S$ for $A$, as follows:
XX:16 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

7

► **Definition 50.** The model $\mathcal{M}_S = (W_S, \leq_S, R_S, V_S)$ determined by $S$ is defined as follows:

- $W_S = \{x_{\Phi \Rightarrow \Psi} | \Phi \Rightarrow \Psi \in \mathcal{P}^+ S\}$.

- the relation $\leq_S$, for $x_{S_1}, x_{S_2} \in W_S$ is defined by $x_{S_1} \leq_S x_{S_2}$ if $S_1 \subseteq_S S_2$.

- The accessibility relation $R_S$, for $x_{S_1}, x_{S_2} \in W_S$, is defined by $R_S x_{S_1} x_{S_2}$ if $S_2 \in_S^{|]} S_1$.

- For the valuation $V_S$, for each $x_{\Phi \Rightarrow \Psi} \in W_S$, let $V_S(x_{\Phi \Rightarrow \Psi}) = \{p \mid p \in \Phi\}$.

Obviously $\mathcal{M}_S$ is finite; each world in $W_S$ corresponds to either a R3-saturated or a blocked sequent, that is nonetheless saturated with respect to (inter) and (trans). Moreover, if $x_{\Gamma \Rightarrow \Delta'}, \langle \Sigma \Rightarrow \Pi \rangle \in W_S$ then $x_{\Sigma \Rightarrow \Pi} \in W_S$, and $x_{\Gamma \Rightarrow \Delta'}, \langle \Sigma \Rightarrow \Pi \rangle \leq_S x_{\Sigma \Rightarrow \Pi}$. By the property of structural inclusion $\subseteq_S$, we have that $\leq_S$ is a pre-order.

► **Proposition 51.** $\mathcal{M}_S$ satisfies the hereditary property (HP) and forward confluence (FC).

► **Lemma 52 (Truth Lemma).** Let $S$ be a global-saturated sequent and $\mathcal{M}_S$ be defined as above. (a). If $A \in \Phi$, then $\mathcal{M}_S, x_{\Phi \Rightarrow \Psi} \Vdash A$; (b). If $A \in \Psi$, then $\mathcal{M}_S, x_{\Phi \Rightarrow \Psi} \Vdash A$.

From the truth lemma we immediately obtain the completeness of $\mathbf{CC}_{\mathbf{FIK}}$.

► **Theorem 53.** For any formula $A \in \mathcal{L}$, if $\Vdash A$, then $\Rightarrow A$ is provable in $\mathbf{CC}_{\mathbf{FIK}}$.

► **Example 54.** We show how to build a countermodel of the formula $(\diamond p \supset \Box q) \supset \Box (p \supset q)$ by $\mathbf{CC}_{\mathbf{FIK}}$ (because of space limit, we omit the steps of the derivation). Ignoring the first step, a derivation is initialized with $\diamond p \supset \Box q \Rightarrow \Box (p \supset q)$. By backward application of the rules, one branch of the derivation ends up with the the saturated sequent $S_0$:

$$S_0 = \diamond p \supset \Box q \Rightarrow \diamond p, \Box (p \supset q), \langle \diamond p \supset \Box q \Rightarrow \diamond p, [\Rightarrow p \supset q, \langle p \Rightarrow q \rangle, p] \rangle \quad \text{and let:}$$

$$S_1 = \diamond p \supset \Box q \Rightarrow \diamond p, [\Rightarrow p \supset q, \langle p \Rightarrow q \rangle, p] \quad S_2 = \Rightarrow p \supset q, \langle p \Rightarrow q \rangle, p \quad S_3 = p \Rightarrow q$$

We then get the model $M_{S_0} = (W, \leq, R, V)$ where $W = \{x_{S_0}, x_{S_1}, x_{S_2}, x_{S_3}\}$, $x_{S_0} \leq x_{S_1}$, $x_{S_2} \leq x_{S_0}$, $x_{S_2} \leq x_{S_3}$, $Rx_{S_1}x_{S_2}$, and $V(x_{S_0}) = V(x_{S_1}) = V(x_{S_2}) = \emptyset$ and $V(x_{S_3}) = \{p\}$. It is easy to see that $x_{S_0} \Vdash (\diamond p \supset \Box q) \supset \Box (p \supset q)$.

► **Example 55.** This example shows that the $\diamond$-free fragment of **FIK** is weaker than the same fragment of **IK**. Let us consider the formula $\neg\neg\Box\neg p \supset \Box\neg p$ presented in [8], which is provable in **IK**. On the other hand if we build a derivation with root $\Rightarrow ((\Box(p \supset \bot) \supset \bot) \supset \Box(p \supset \bot))$, we generate the saturated sequent $S_0 = F \Rightarrow \Box(p \supset \bot)$, $G, \langle S_1 \rangle, \langle S_6 \rangle$, where $F = (\Box(p \supset \bot) \supset \bot) \supset \bot$ and $G = \Box(p \supset \bot) \supset \bot$, and
$$S_1 = F \Rightarrow G, [\Rightarrow \langle p \supset \bot \rangle], \langle S_4 \rangle, \quad S_4 = F, \Box(p \supset \bot) \Rightarrow \bot, G, [p \supset \bot \Rightarrow p], \\ S_6 = F, \Box(p \supset \bot) \Rightarrow \bot, G.$$
Further let $S_2 = \langle p \supset \bot \rangle$, $S_3 = p \supset \bot$, $S_5 = p \supset \bot \Rightarrow p$.

We get the model $M_{S_0} = (W, \leq, R, V)$ where $W = \{x_{S_0}, \dots, x_{S_6}\}$, $x_{S_0} \leq x_{S_1}, x_{S_0} \leq x_{S_6}, x_{S_1} \leq x_{S_4}, x_{S_6} \leq x_{S_4}, x_{S_2} \leq x_{S_3}, x_{S_2} \leq x_{S_5}, x_{S_2} \leq x_{S_0}$, $Rx_{S_1}x_{S_2}$, $Rx_{S_4}x_{S_5}$, $V(x_{S_i}) = \emptyset$ for $i \neq 3$ and $V(x_{S_3}) = \{p\}$. It is easy to see that $x_{S_0} \Vdash \Box(p \supset \bot)$, as $x_{S_0} \leq x_{S_1} Rx_{S_3}$ and $x_{S_3} \Vdash p$; moreover $x_{S_0} \Vdash F$ since $x_{S_5} \Vdash p \supset \bot$, whence $x_{S_4} \Vdash \Box(p \supset \bot)$ and $\forall y \geq x_{S_0} \cdot y \leq x_{S_4}$. Observe that $M$ satisfies (FC), the only worlds which are concerned are $x_{S_1}, x_{S_2}, x_{S_4}, x_{S_5}$.
# 5 Conclusion and future work

We have proposed **FIK**, a natural variant of Intuitionistic modal logic characterized by forward confluent bi-relational models. **FIK** is intermediate between constructive modal logic **CK** and intuitionistic modal logic **IK** and it satisfies all the expected criteria for **IML**. We have presented a sound and complete axiomatization of it and a bi-nested calculus $C_{FIK}$ which provides a decision procedure together with a finite countermodel extraction.

There are many topics for further research. First we may study extensions of **FIK** with the standard axioms from the modal cube. To obtain decidability and terminating proof systems for transitive logics (eg. K4 axiom) might be difficult and it may be worthwhile to study an embedding of the nested sequent calculus into a labelled calculus and adapt the techniques and results of [?]. More generally we can study extensions of **FIK** whose accessibility relation is defined by Horn properties: perhaps the nested sequent calculi can be obtained by means of the refinement technique proposed in [?].

Moreover we can consider other bi-relational frame conditions relating the pre-order and the accessible (including the one for **IK**) and see how they can be captured uniformly in Bi-nested calculi with suitable "interaction rules".

## Acknowledgement

This paper is originated from a discussion started by Anupam Das and Sonia Marin in the proof theory blog (see the link https://prooftheory.blog/2022/08/19/), we are grateful to them, as well as to all other contributors to the discussion. In particular Example 24 was reported in the blog by Alex Simpson, who had learnt it in 1996 by Carsten Grefe in private communication. Example 55 was suggested first by Anupam Das and Sonia Marin in the blog. Finally we thank the reviewers for their very helpful criticisms and insightful remarks.

## Appendix

This Appendix includes the proofs of some of our results. Some of these proofs are relatively simple and we have included them here just for the sake of the completeness.

**Lemma 12.** ($W_c, \leq_c, R_c, V_c$) satisfies the frame condition (**FC**).

*Proof.* Let $\Gamma, \Delta, \Lambda \in W_c$ be such that $\Gamma \geq_c \Delta$ and $\Delta R_c \Lambda$. Hence, $\Gamma \supseteq \Delta$ and $\Delta \bowtie \Lambda$. Let $A_1, A_2, \dots$ be an enumeration of $\square \Gamma$ and $B_1, B_2, \dots$ be an enumeration of $\Lambda$. Obviously, for all $n \in \mathbb{N}$, $\square(A_1 \wedge \dots \wedge A_n) \in \Gamma$ and $B_1 \wedge \dots \wedge B_n \in \Lambda$. Since $\Delta \bowtie \Lambda$, for all $n \in \mathbb{N}$, $\diamond(B_1 \wedge \dots \wedge B_n) \in \Delta$. For all $n \in \mathbb{N}$, let $\Theta_n = \mathbf{D}_{\mathbf{FIK}} + A_1 \wedge \dots \wedge A_n \wedge B_1 \wedge \dots \wedge B_n$. Obviously, $(\Theta_n)_{n \in \mathbb{N}}$ is a chain of theories such that $\bigcup \{\Theta_n : n \in \mathbb{N}\} \supseteq \Lambda$.

We claim that for all formulas $C$, if $\square C \in \Gamma$ then $C \in \bigcup \{\Theta_n : n \in \mathbb{N}\}$. If not, there exists a formula $C$ such that $\square C \in \Gamma$ and $C \notin \bigcup \{\Theta_n : n \in \mathbb{N}\}$. Thus, $C \in \square \Gamma$. Consequently, let $n \in \mathbb{N}$ be such that $A_n = C$. Hence, $A_1 \wedge \dots \wedge A_n \wedge B_1 \wedge \dots \wedge B_n \to C$ is in $\mathbf{D}_{\mathbf{FIK}}$. Thus, $C \in \Theta_n$. Consequently, $C \in \bigcup \{\Theta_n : n \in \mathbb{N}\}$: a contradiction. Hence, for all formulas $C$, if $\square C \in \Gamma$ then $C \in \bigcup \{\Theta_n : n \in \mathbb{N}\}$.

We claim that for all formulas $C$, if $C \in \bigcup \{\Theta_n : n \in \mathbb{N}\}$ then $\diamond C \in \Gamma$. If not, there exists $n \in \mathbb{N}$ and there exists a formula $C$ such that $C \in \Theta_n$ and $\diamond C \notin \Gamma$. Thus, $A_1 \wedge \dots \wedge A_n \wedge B_1 \wedge \dots \wedge B_n \to C$ is in $\mathbf{D}_{\mathbf{FIK}}$. Consequently, $B_1 \wedge \dots \wedge B_n \to (A_1 \wedge \dots \wedge A_n \to C)$ is in $\mathbf{D}_{\mathbf{FIK}}$. Hence, $\diamond(B_1 \wedge \dots \wedge B_n) \supset \diamond(A_1 \wedge \dots \wedge A_n \supset C)$ is in $\mathbf{D}_{\mathbf{FIK}}$. Since $\diamond(B_1 \wedge \dots \wedge B_n) \in \Delta$, $\diamond(A_1 \wedge \dots \wedge A_n \supset C) \in \Delta$. Since $\Gamma \supseteq \Delta$, $\diamond(A_1 \wedge \dots \wedge A_n \supset C) \in \Gamma$.
XX:18 A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

⁸

Thus, □(A₁ ∧ ... ∧ Aₙ) ⊃ ◊C ∈ Γ. Since □(A₁ ∧ ... ∧ Aₙ) ∈ Γ, ◊C ∈ Γ: a contradiction. Consequently, for all formulas C, if C ∈ ⋃{Θₙ : n ∈ N} then ◊C ∈ Γ.

Let $\mathcal{S} = \{\Theta : \Theta \text{ is a theory such that (1) } \Gamma \bowtie \Theta \text{ and (2) } \Theta \supseteq \Lambda\}$. Obviously, ⋃{Θₙ : n ∈ N} ∈ S. Hence, S is nonempty. Moreover, for all nonempty chains (Πᵢ)ᵢ∈I of elements of S, ⋃{Πᵢ : i ∈ I} is an element of S. Thus, by Zorn's Lemma, S possesses a maximal element Θ. Consequently, Θ is a theory such that Γ ⋊ Θ and Θ ⊇ Λ. Hence, it only remains to be proved that Θ is proper and prime.

We claim that Θ is proper. If not, ⊥ ∈ Θ. Since Γ ⋊ Θ, ◊⊥ ∈ Γ: a contradiction. Thus, Θ is proper.

We claim that Θ is prime. If not, there exists formulas C, D such that C ∨ D ∈ Θ, C ∉ Θ and D ∉ Θ. Consequently, by the maximality of Θ in S, Θ + C ∉ S and Θ + D ∉ S. Hence, there exists a formula E such that E ∈ Θ + C and ◊E ∉ Γ and there exists a formula F such that F ∈ Θ + D and ◊F ∉ Γ. Thus, C ⊃ E ∈ Θ and D ⊃ F ∈ Θ. Consequently, C ∨ D ⊃ E ∨ F ∈ Θ. Since C ∨ D ∈ Θ, E ∨ F ∈ Θ. Since Γ ⋊ Θ, ◊(E ∨ F) ∈ Γ. Hence, either ◊E ∈ Γ, or ◊F ∈ Γ: a contradiction. Thus, Θ is prime. ◀

**Lemma 13.** Let Γ be a prime theory. Let B, C be formulas.

1. If $B \supset C \notin \Gamma$ then there exists a prime theory $\Delta$ such that $\Gamma \subseteq \Delta$, $B \in \Delta$ and $C \notin \Delta$,

2. if □B ∉ Γ then there exists prime theories Δ, Λ such that Γ ⊆ Δ, Δ ⋊ Λ and B ∉ Λ,

3. if ◊B ∈ Γ then there exists a prime theory Δ such that Γ ⋊ Δ and B ∈ Δ.

**Proof.** Case of $\supset$. Suppose $B \supset C \notin \Gamma$. Let $S = \{\Delta : \Delta$ is a theory such that (1) $\Gamma \subseteq \Delta$, (2) $B \in \Delta$ and (3) $C \notin \Delta\}$.

Since $B \supset C \notin \Gamma$, $C \notin \Gamma + B$. Hence, $\Gamma + B \in S$. Thus, S is nonempty. Moreover, for all nonempty chains $(\Delta_i)_{i \in I}$ of elements of $S$, ⋃{$\Delta_i : i \in I$} is an element of $S$. Consequently, by Zorn's Lemma, $S$ possesses a maximal element $\Delta$. Hence, $\Delta$ is a theory such that $\Gamma \subseteq \Delta$, $B \in \Delta$ and $C \notin \Delta$.

Thus, it only remains to be proved that $\Delta$ is proper and prime.

We claim that $\Delta$ is proper. If not, $\Delta = \mathcal{L}$. Consequently, $C \in \Delta$: a contradiction. Hence, $\Delta$ is proper.

We claim that $\Delta$ is prime. If not, there exists formulas $D, E$ such that $D \vee E \in \Delta$, $D \notin \Delta$ and $E \notin \Delta$. Thus, by the maximality of $\Delta$ in $S$, $\Delta + D \notin S$ and $\Delta + E \notin S$. Consequently, $C \in \Delta + D$ and $C \in \Delta + E$. Hence, $D \supset C \in \Delta$ and $E \supset C \in \Delta$. Thus, $D \vee E \supset C \in \Delta$. Since $D \vee E \in \Delta$, $C \in \Delta$: a contradiction. Consequently, $\Delta$ is prime.

**Case of** □. Suppose □B ∉ Γ. Let $S = \{\Delta : \Delta$ is a theory such that (1) $\Gamma \subseteq \Delta$ and (2) □B ∉ Δ\}$.

Since □B ∉ Γ, Γ ∈ S. Hence, S is nonempty. Moreover, for all nonempty chains (Δᵢ)ᵢ∈I of elements of S, ⋃{Δᵢ : i ∈ I} is an element of S. Thus, by Zorn's Lemma, S possesses a maximal element Δ. Consequently, Δ is a theory such that Γ ⊆ Δ and □B ∉ Δ.

We claim that $\Delta$ is proper. If not, $\Delta = \mathcal{L}$. Hence, □B ∈ Δ: a contradiction. Thus, $\Delta$ is proper.

We claim that $\Delta$ is prime. If not, there exists formulas C, D such that C ∨ D ∈ Δ, C ∉ Δ and D ∉ Δ. Consequently, by the maximality of $\Delta$ in S, $\Delta + C \notin S$ and $\Delta + D \notin S$. Hence, □B ∈ Δ + C and □B ∈ Δ + D. Thus, C ⊃ □B ∈ Δ and D ⊃ □B ∈ Δ. Consequently, C ∨ D ⊃ □B ∈ Δ. Since C ∨ D ∈ Δ, □B ∈ Δ: a contradiction. Hence, $\Delta$ is prime.

We claim that for all formulas C, if C ∨ B ∈ □Δ then ◊C ∈ Δ. If not, there exists a formula C such that C ∨ B ∈ □Δ and ◊C ∉ Δ. Thus, by the maximality of Δ in S, Δ + ◊C ∉ S. Consequently, □B ∈ Δ + ◊C. Hence, ◊C ⊃ □B ∈ Δ. Since C ∨ B ∈ □Δ,
$\Box(C \lor B) \in \Delta$. Since $\diamond C \supset \Box B \in \Delta$, $\Box B \in \Delta$: a contradiction. Thus, for all formulas $C$, if $C \lor B \in \Box \Delta$ then $\diamond C \in \Delta$.

Let $\mathcal{T} = \{\Lambda : \Lambda$ is a theory such that (1) $\Box \Delta \subseteq \Lambda$, (2) for all formulas $C$, if $C \lor B \in \Lambda$ then $\diamond C \in \Delta$ and (3) $B \notin \Lambda$\}.

Since $\Box B \notin \Delta$, $B \notin \Box \Delta$. Consequently, $\Box \Delta \in \mathcal{T}$. Hence, $\mathcal{T}$ is nonempty. Moreover, for all nonempty chains $(\Lambda_i)_{i \in I}$ of elements of $\mathcal{T}$, $\bigcup \{\Lambda_i : i \in I\}$ is an element of $\mathcal{T}$. Thus, by Zorn's Lemma, $\mathcal{T}$ possesses a maximal element $\Lambda$. Consequently, $\Lambda$ is a theory such that $\Box \Delta \subseteq \Lambda$, for all formulas $C$, if $C \lor B \in \Lambda$ then $\diamond C \in \Delta$ and $B \notin \Lambda$.

Hence, it only remains to be proved that $\Lambda$ is proper and prime and $\Delta \succcurlyeq \Lambda$.

We claim that $\Lambda$ is proper. If not, $\Lambda = \mathcal{L}$. Thus, $B \in \Lambda$: a contradiction. Consequently, $\Lambda$ is proper.

We claim that $\Lambda$ is prime. If not, there exists formulas $C, D$ such that $C \lor D \in \Lambda$, $C \notin \Lambda$ and $D \notin \Lambda$. Hence, by the maximality of $\Lambda$ in $\mathcal{T}$, $\Lambda + C \notin \mathcal{T}$ and $\Lambda + D \notin \mathcal{T}$. Thus, either there exists a formula $E$ such that $E \lor B \in \Lambda + C$ and $\diamond E \notin \Delta$, or $B \in \Lambda + C$ and either there exists a formula $F$ such that $F \lor E \in \Lambda + D$ and $\diamond F \notin \Delta$, or $B \in \Lambda + D$. Consequently, we have to consider the following 4 cases.

(1) Case “there exists a formula $E$ such that $E \lor B \in \Lambda + C$ and $\diamond E \notin \Delta$ and there exists a formula $F$ such that $F \lor B \in \Lambda + D$ and $\diamond F \notin \Delta$”: Hence, $C \supset E \lor B \in \Lambda$ and $D \supset F \lor B \in \Lambda$. Thus, $C \lor D \supset E \lor F \lor B \in \Lambda$. Since $C \lor D \in \Lambda$, $E \lor F \lor B \in \Lambda$. Consequently, $\diamond (E \lor F) \in \Delta$. Hence, either $\diamond E \in \Delta$, or $\diamond F \in \Delta$: a contradiction.

(2) Case “there exists a formula $E$ such that $E \lor F \in \Lambda + C$ and $\diamond E \notin \Delta$ and $B \in \Lambda + D$”: Thus, $C \supset E \lor B \in \Lambda$ and $D \supset B \in \Lambda$. Consequently, $C \lor D \supset E \lor B \in \Lambda$. Since $C \lor D \in \Lambda$, $E \lor B \in \Lambda$. Hence, $\diamond E \in \Delta$: a contradiction.

(3) Case “$B \in \Lambda + C$ and there exists a formula $F$ such that $F \lor B \in \Lambda + D$ and $\diamond F \notin \Delta$”: Thus, $C \supset B \in \Lambda$ and $D \supset F \lor B \in \Lambda$. Consequently, $C \lor D \supset F \lor B \in \Lambda$. Since $C \lor D \in \Lambda$, $F \lor B \in \Lambda$. Hence, $\diamond F \in \Delta$: a contradiction.

(4) Case “$B \in \Lambda + C$ and $B \in \Lambda + D$”: Thus, $C \supset B \in \Lambda$ and $D \supset B \in \Lambda$. Consequently, $C \lor D \supset B \in \Lambda$. Since $C \lor D \in \Lambda$, $B \in \Lambda$: a contradiction.

Hence, $\Lambda$ is prime.

We claim that $\Delta \succcurlyeq \Lambda$. If not, there exists a formula $C$ such that $C \in \Lambda$ and $\diamond C \notin \Delta$. Thus, $C \lor B \in \Lambda$. Consequently $\diamond C \in \Delta$: a contradiction. Hence, $\Delta \succcurlyeq \Lambda$.

**Case of $\diamond$**. Suppose $\diamond B \in \Gamma$. Let $S = \{\Delta : \Delta$ is a theory such that (1) for all formulas $C$, if $C \in \Delta$ then $\diamond C \in \Gamma$ and (2) $B \in \Delta$\}.

We claim that $\Box \Gamma + B \in S$. If not, there exists a formula $C$ such that $C \in \Box \Gamma + B$ and $\diamond C \notin \Gamma$. Hence, $B \supset C \in \Box \Gamma$. Thus, $\Box (B \supset C) \in \Gamma$. Consequently, $\diamond B \supset \diamond C \in \Gamma$. Since $\diamond B \in \Gamma$, $\diamond C \in \Gamma$: a contradiction. Hence, $\Box \Gamma + B \in S$. Thus, $S$ is nonempty. Moreover, for all nonempty chains $(\Delta_i)_{i \in I}$ of elements of $S$, $\bigcup \{\Delta_i : i \in I\}$ is an element of $S$. Consequently, by Zorn's Lemma, $S$ possesses a maximal element $\Delta$. Hence, $\Delta$ is a theory such that for all formulas $C$, if $C \in \Delta$ then $\diamond C \in \Gamma$ and $B \in \Delta$.

Thus, it only remains to be proved that $\Delta$ is proper and prime and $\Gamma \succcurlyeq \Delta$.

We claim that $\Delta$ is proper. If not, $\bot \in \Delta$. Consequently, $\diamond \bot \in \Gamma$: a contradiction. Hence, $\Delta$ is proper.

We claim that $\Delta$ is prime. If not, there exists formulas $C, D$ such that $C \lor D \in \Delta$, $C \notin \Delta$ and $D \notin \Delta$. Thus, by the maximality of $\Delta$ in $S$, $\Delta + C \notin S$ and $\Delta + D \notin S$. Consequently, there exists a formula $E$ such that $E \in \Delta + C$ and $\diamond E \notin \Gamma$ and there exists a formula $F$ such that $F \in \Delta + D$ and $\diamond F \notin \Gamma$. Hence, $C \supset E \in \Delta$ and $D \supset F \in \Delta$. Thus, $C \lor D \supset E \lor F \in \Delta$. Since $C \lor D \in \Delta$, $E \lor F \in \Delta$. Consequently, $\diamond (E \lor F) \in \Gamma$. Hence, either $\diamond E \in \Gamma$, or $\diamond F \in \Gamma$: a contradiction. Thus, $\Delta$ is prime.
We claim that $\Gamma \bowtie \Delta$. If not, there exists a formula $C$ such that $\Box C \in \Gamma$ and $C \notin \Delta$. Consequently, by the maximality of $\Delta$ in $S$, $\Delta + C \notin S$. Hence, there exists a formula $D$ such that $D \in \Delta + C$ and $\diamond D \notin \Gamma$. Thus, $C \supset D \in \Delta$. Consequently, $\diamond (C \supset D) \in \Gamma$. Since $\Box C \in \Gamma$, $\diamond D \in \Gamma$: a contradiction. Hence, $\Gamma \bowtie \Delta$.

◀

**Lemma 14.** For all formulas $A$ and for all $\Gamma \in W_c$, $A \in \Gamma$ if and only if $\Gamma \models A$.

*Proof.* By induction on $A$. We only consider the following 3 cases.

(1) Case “there exists formulas $B, C$ such that $A = B \supset C$”: Let $\Gamma \in W_c$. From left to right, suppose $B \supset C \in \Gamma$ and $\Gamma \not\models B \supset C$. Hence, there exists $\Delta \in W_c$ such that $\Gamma \leq_c \Delta$, $\Delta \models B$ and $\Delta \not\models C$. Thus, $\Gamma \subseteq \Delta$. Moreover, by induction hypothesis, $B \in \Delta$ and $C \notin \Delta$. Since $B \supset C \in \Gamma$, $B \supset C \in \Delta$. Since $B \in \Delta$, $C \in \Delta$: a contradiction. From right to left, suppose $\Gamma \models B \supset C$ and $B \supset C \notin \Gamma$. Consequently, by Lemma 13, there exists a prime theory $\Delta$ such that $\Gamma \subseteq \Delta$, $B \in \Delta$ and $C \notin \Delta$. Hence, $\Gamma \leq_c \Delta$. Moreover, by induction hypothesis, $\Delta \models B$ and $\Delta \not\models C$. Thus, $\Gamma \not\models B \supset C$: a contradiction.

(2) Case “there exists a formula $B$ such that $A = \Box B$”: Let $\Gamma \in W_c$. From left to right, suppose $\Box B \in \Gamma$ and $\Gamma \not\models \Box B$. Thus, there exists $\Delta$, $\Lambda \in W_c$ such that $\Gamma \leq_c \Delta$, $\Delta R_c \Lambda$ and $\Lambda \not\models B$. Consequently, $\Gamma \subseteq \Delta$ and $\Delta \bowtie \Lambda$. Moreover, by induction hypothesis, $B \notin \Lambda$. Since $\Box B \in \Gamma$, $B \in \Lambda$: a contradiction. From right to left, suppose $\Gamma \models \Box B$ and $\Box B \notin \Gamma$. Hence, by Lemma 13, there exists prime theories $\Delta$, $\Lambda$ such that $\Gamma \subseteq \Delta$, $\Delta \bowtie \Lambda$ and $B \notin \Lambda$. Thus, $\Gamma \leq_c \Delta$ and $\Delta R_c \Lambda$. Moreover, by induction hypothesis, $\Lambda \not\models B$. Consequently, $\Gamma \not\models \Box B$: a contradiction.

(3) Case “there exists a formula $B$ such that $A = \diamond B$”: Let $\Gamma \in W_c$. From left to right, suppose $\diamond B \in \Gamma$ and $\Gamma \not\models \diamond B$. Consequently, by Lemma 13, there exists a prime theory $\Delta$ such that $\Gamma \bowtie \Lambda$ and $B \in \Delta$. Hence, $\Gamma R_c \Delta$. Moreover, by induction hypothesis, $\Delta \models B$. Thus, $\Gamma \models \diamond B$: a contradiction. From right to left, suppose $\Gamma \models \diamond B$ and $\diamond B \notin \Gamma$. Consequently, there exists $\Delta \in W_c$ such that $\Gamma R_c \Delta$ and $\Delta \models B$. Hence, $\Gamma \bowtie \Delta$. Moreover, by induction hypothesis, $B \in \Delta$. Since $\diamond B \notin \Gamma$, $B \notin \Delta$: a contradiction.

◀

**Lemma 16.** $\diamond p \equiv \neg \Box \neg p$ is in $\mathbf{D}_{\mathbf{FIK}}^+$.

*Proof.* (1) Obviously, $\neg p \supset (p \supset \bot)$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Hence, using (NEC) and $(K_\Box)$, $\Box \neg p \supset \Box (p \supset \bot)$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Thus, $\diamond p \supset \neg \Box \neg p \vee \Box (p \supset \bot)$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Consequently, using $(K_\diamond)$, $\diamond p \supset \neg \Box \neg p \vee \diamond \bot$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Since $\neg \diamond \bot$ is in $\mathbf{D}_{\mathbf{FIK}}^+$, $\diamond p \supset \neg \Box \neg p$ is in $\mathbf{D}_{\mathbf{FIK}}^+$.

(2) Obviously, $p \vee \neg p$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Hence, using (NEC), $\Box (p \vee \neg p)$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Since using $(wCD)$, $\Box (p \vee \neg p) \supset ((\diamond p \supset \Box \neg p) \supset \Box \neg p)$ is in $\mathbf{D}_{\mathbf{FIK}}^+$, $(\diamond p \supset \Box \neg p) \supset \Box \neg p$ is in $\mathbf{D}_{\mathbf{FIK}}^+$. Thus, $\neg \Box \neg p \supset \diamond p$ is in $\mathbf{D}_{\mathbf{FIK}}^+$.

◀

**Lemma 17.** Let $p$ be an atomic proposition. There exists no $\Box$-free $A$ such that $\Box p \equiv A$ is in $\mathbf{D}_{\mathbf{FIK}}$ and there exists no $\diamond$-free $A$ such that $\diamond p \equiv A$ is in $\mathbf{D}_{\mathbf{FIK}}$.

*Proof.* (1) For the sake of the contradiction, suppose there exists a $\Box$-free formula $A$ such that $\Box p \equiv A$ is in $\mathbf{D}_{\mathbf{FIK}}$. Without loss of generality, we may assume that $p$ is the only atomic proposition that may occur in $A$. Since $\Box p \equiv A$ is in $\mathbf{D}_{\mathbf{FIK}}$, by Theorem 7, $\models \Box p \equiv A$. Let $(W, \leq, R, V)$ be the bi-relational model defined by $W = \{a, b, c, d\}$, $a \leq c$, $b \leq d$, $aRb$, $aRd$, $cRd$ and $V(p) = \{d\}$. By induction on the $\Box$-free formula $B$, the reader may easily verify that $M, a \models B$ if and only if $M, c \models B$. Since $A$ is $\Box$-free, $M, a \models A$ if and only if $M, c \models A$. Since $\models \Box p \equiv A$, $M, a \models \Box p$ if and only if $M, c \models \Box p$. This contradicts the facts that $M, a \not\models \Box p$ and $M, c \models \Box p$.
(2) For the sake of the contradiction, suppose there exists a $\Diamond$-free formula $A$ such that $\Diamond p \equiv A$ is in $\mathbf{D}_{\text{FIK}}$. Without loss of generality, we may assume that $p$ is the only atomic proposition that may occur in $A$. Since $\Diamond p \equiv A$ is in $\mathbf{D}_{\text{FIK}}$, by Theorem 7, $\Vdash \Diamond p \equiv A$. Let $(W, \leq, R, V)$ be the bi-relational model defined by $W = \{a, b, c, d\}$, $a \leq c$, $b \leq d$, $aRb$, $cRb$, $cRd$ and $V(p) = \{d\}$. By induction on the $\Diamond$-free formula $B$, the reader may easily verify that $M, a \Vdash B$ if and only if $M, c \Vdash B$. Since $A$ is $\Diamond$-free, $M, a \Vdash A$ if and only if $M, c \Vdash A$. Since $\Vdash \Diamond p \equiv A$, $M, a \Vdash \Diamond p$ if and only if $M, c \Vdash \Diamond p$. This contradicts the facts that $M, a \Vdash \Diamond p$ and $M, c \Vdash \Diamond p$. $\blacksquare$

**Lemma 25.** Suppose that a sequent $S = \Rightarrow A_1, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle$ is provable in $\mathbf{C}_{\text{FIK}}$, where $A_i$'s are formulas. Then either for some $A_i$, $\Rightarrow A_i$ is provable in $\mathbf{C}_{\text{FIK}}$ or for some $G_j$, $\Rightarrow \langle G_j \rangle$ is provable in $\mathbf{C}_{\text{FIK}}$.

**Proof.** By induction on the height of a proof of $S$. If $S$ is an axiom, then some $\Rightarrow \langle G_j \rangle$ must be an axiom. Otherwise $S$ it is obtained by applying a rule to some $A_i$ or to some $\langle G_j \rangle$. In the first case, suppose that $S$ is derived by applying a rule to $A_1$ (to simplifying indexing). We only illustrate two cases: let $A_1 = B \wedge C$, then we have

$$ \frac{\Rightarrow B, A_2, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle \quad \Rightarrow C, A_2, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle}{\Rightarrow B \wedge C, A_2, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle} $$

By induction hypothesis on the first premise either form some $A_i$ ($i = 2, \dots, m$) $\Rightarrow A_i$ is derivable or some $\langle G_j \rangle$ is derivable and we are done: otherwise $\Rightarrow B$ must be derivable; in this case by induction hypothesis on the second premise $\Rightarrow C$ must be derivable; then we conclude by an application of $(\wedge_R)$. Suppose that $A_1 = \Box B$ and is derived by

$$ \frac{\Rightarrow A_2, \dots, A_m, \langle \Rightarrow [\Rightarrow B] \rangle, \langle G_1 \rangle, \dots, \langle G_n \rangle}{\Rightarrow \Box B, A_2, \dots, A_m, \langle G_1 \rangle, \dots, \langle G_n \rangle} $$

By induction hypothesis, as before either form some $A_i$ ($i = 2, \dots, m$), $\Rightarrow A_i$ is derivable or some $\langle G_j \rangle$ is derivable and we are done; otherwise $\Rightarrow \langle \Rightarrow [\Rightarrow B] \rangle$ and by an application of $(\Box_R)$ we conclude. If $S$ is derived by applying a rule to some $\Rightarrow \langle G_j \rangle$ the reasoning is the same. $\blacksquare$

**Proposition 26.** For any formulas $A, B$, if $\Rightarrow A \vee B$ is provable in $\mathbf{C}_{\text{FIK}}$, then either $\Rightarrow A$ or $\Rightarrow B$ is provable.

**Proof.** Let $\Rightarrow A \vee B$ be provable in $\mathbf{C}_{\text{FIK}}$. Then it must be derived by $(\vee_R)$ from $\Rightarrow A, B$ and then we apply the previous lemma. $\blacksquare$

**Lemma 28.** Let $M = (W, \leq, R, V)$ be a bi-relational model and $x, x' \in W$ with $x \leq x'$. Let $S = \Gamma \Rightarrow \Delta$ be any sequent, if $x \Vdash \Delta$ then $x' \Vdash \Delta^*$.

**Proof.** By induction on the structure of $\Delta^*$. If $\Delta^* = \emptyset$ it follows by definition. Otherwise $\Delta^* = [\Phi_1 \Rightarrow \Psi_1^*], \dots, [\Phi_k \Rightarrow \Psi_k^*]$ where $\Delta = \Delta_0, [\Phi_1 \Rightarrow \Psi_1], \dots, [\Phi_k \Rightarrow \Psi_k]$ and $\Delta_0$ is $[\cdot]$-free. By hypothesis $x \Vdash \Delta$, thus $x \Vdash [\Phi_i \Rightarrow \Psi_i]$ for $i = 1, \dots, k$. Therefore there are $y_1, \dots, y_k$ with $Rxy_i$ for $i = 1, \dots, k$ such that $y_i \Vdash \Phi_i \Rightarrow \Psi_i$. This means that (a) $y_i \Vdash C$ for every $C \in \Phi_i$ and (b) $y_i \Vdash \Psi_i$. By (FC) property there are $y'_1, \dots, y'_k$ such that $Rx'y'_i$ and $y'_i \geq y_i$ for $i = 1, \dots, k$. By (a) it follows that (c) $y'_i \Vdash C$ for every $C \in \Phi_i$; moreover by induction hypothesis it follows that (d) $y'_i \Vdash \Psi_i^*$. Thus from (c) and (d) we have $y'_i \Vdash \Phi_i \Rightarrow \Psi_i^*$, whence $x' \Vdash [\Phi_i \Rightarrow \Psi_i^*]$ for $i = 1, \dots, k$, which means that $x' \Vdash \Delta^*$. $\blacksquare$
**Lemma 29.** Given a model $\mathcal{M} = (W, \leq, R, V)$ and $x \in W$, for any rule (r) of the form $\frac{G\{S_1\} G\{S_2\}}{G\{S\}}$ or $\frac{G\{S_1\}}{G\{S\}}$, if $x \models G\{S_i\}$, then $x \models G\{S\}$.

**Proof.** We proceed by induction on the structure of the context $G\{\}$. ■

(base of the induction) $G\{\} = \emptyset$. We check rule by rule. As an example, we consider $(\Box_R)$ and (inter) rules, the other cases are similar or simpler and are left to the reader. For $(\Box_R)$, suppose by absurdity that $x \models \Gamma \Rightarrow \Delta$, $\langle\Rightarrow [\Rightarrow B]\rangle$ but $x \nvdash \Gamma \Rightarrow \Delta, \Box B$. It follows that: $x \models A$ for every $A \in \Gamma$, $x \nvdash \Delta$, (i) $x \nvdash \Box B$, (ii) $x \models \langle\Rightarrow [\Rightarrow B]\rangle$. From (i) it follows that there is $x_1 \geq x$ and $y_1$, with $Rx_1y_1$ such that $y_1 \nvdash B$. From (ii) it follows that for all $x' \geq x$ and for all $y$ with $Rx'y$, it holds $y \models B$, thus taking $x' = x_1$ and $y = y_1$ we have a contradiction.

For (inter) suppose by absurdity that $x \models \Gamma \Rightarrow \Delta$, $\langle\Sigma \Rightarrow \Pi, [\Lambda \Rightarrow \Theta^*]\rangle$, $[\Lambda \Rightarrow \Theta]$ but $x \nvdash \Gamma \Rightarrow \Delta$, $\langle\Sigma \Rightarrow \Pi\rangle$, $[\Lambda \Rightarrow \Theta]$. It follows that (i) $x \nvdash \langle\Sigma \Rightarrow \Pi\rangle$, (ii) $x \nvdash [\Lambda \Rightarrow \Theta]$, but (iii) $x \models \langle\Sigma \Rightarrow \Pi, [\Lambda \Rightarrow \Theta^*]\rangle$. By (i) there is $x_1 \geq x$, such that $x_1 \nvdash \Sigma \Rightarrow \Pi$, by (ii) there is $y$ with $Rxy$ such that (iv) $y \nvdash \Lambda \Rightarrow \Theta$. By (FC) condition, there is $y_1$ such that $Rx_1y_1$ and $y_1 \geq y$. By (iii), it follows $x_1 \models \Sigma \Rightarrow \Pi, [\Lambda \Rightarrow \Theta^*]$ whence (v) $y_1 \models \Lambda \Rightarrow \Theta^*$. By (iv) we have that $y \models B$ for every $B \in \Lambda$ and $y \nvdash \Theta$. Since $y_1 \geq y$, we have that also $y_1 \models B$ for every $B \in \Lambda$, so that by (v) it must be $y_1 \models \Theta^*$. Thus we have $y_1 \geq y$, $y \nvdash \Theta$, and $y_1 \models \Theta^*$, by the previous lemma we have a contradiction.

(inductive step) Let $G\{\} = \Gamma \Rightarrow \Delta, \langle G'\{\}\rangle$. Let us consider for instance a rule $\frac{G\{S_1\} G\{S_2\}}{G\{S\}}$. Suppose that $x \models G\{S_1\}$ and $x \models G\{S_2\}$. This means that $x \models \Gamma \Rightarrow \Delta, \langle G'\{S_1\}\rangle$ and $x \models \Gamma \Rightarrow \Delta, \langle G'\{S_2\}\rangle$. We prove that $x \models \Gamma \Rightarrow \Delta, \langle G'\{S\}\rangle$. If $x \nvdash B$ for some $B \in \Gamma$, or $x \models O$ for some $O \in \Delta$ we are done. Otherwise, it must be $x \models \langle G'\{S_1\}\rangle$ and $x \models \langle G'\{S_2\}\rangle$. From this it follows that for all $x' \geq x$, we have $x' \models G'\{S_1\}$ and $x' \models G'\{S_2\}$, by induction hypothesis we get $x' \models G'\{S\}$ and the conclusion follows. The case $G\{\} = \Gamma \Rightarrow \Delta, [G'\{\}]$ is similar. ■

<figure><img src="image_3.png" /></figure>

**Proposition 35.** Let $\Gamma \Rightarrow \Delta$ be a sequent saturated with respect to both (trans) and (inter). If $\Delta$ is of form $\Delta', \langle\Sigma \Rightarrow \Pi\rangle$, then $\Gamma \Rightarrow \Delta \subseteq^S \Sigma \Rightarrow \Pi$.

**Proof.** We show this by induction on the structure of $\Delta'$. ■

**Base case** Assume $\Delta'$ is $[\cdot]$-free, then according to Definition 33, it suffices to check $\Gamma \subseteq \Sigma$. Since $\Delta', \langle\Sigma \Rightarrow \Pi\rangle$ is saturated, by the saturation condition associated with (trans), we see that $\Gamma \subseteq \Sigma$.

**Inductive step** Assume $\Delta'$ contains $[\cdot]$ blocks, take an arbitrary $[\Phi \Rightarrow \Psi]$ from it. Then $\Delta$ can be written explicitly as $\Delta'', \langle\Sigma \Rightarrow \Pi'\rangle, [\Phi \Rightarrow \Psi]$. By the saturation condition associated with (inter), there is a modal block occurring in $\Pi$ of form $\Omega \Rightarrow \Xi$ s.t. $\Phi \Rightarrow \Psi \subseteq^S \Omega \Rightarrow \Xi$. $\Sigma \Rightarrow \Pi$ can be written explicitly as $\Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]$, and further $\Gamma \Rightarrow \Delta$ is $\Gamma \Rightarrow \Delta'', \langle\Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]\rangle, [\Phi \Rightarrow \Psi]$. Recall the whole sequent $\Gamma \Rightarrow \Delta$ is saturated with both (trans) and (inter), so is $\Gamma \Rightarrow \Delta'', \langle\Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]\rangle$. By IH, we see that $\Gamma \Rightarrow \Delta'', \langle\Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]\rangle \subseteq^S \Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]$. Since $[\Phi \Rightarrow \Psi]$ is arbitrary, by Definition 33, we see that $\Gamma \Rightarrow \Delta'', \langle\Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]\rangle, [\Phi \Rightarrow \Psi] \subseteq^S \Sigma \Rightarrow \Pi', [\Omega \Rightarrow \Xi]$ as well.

As a result, we conclude $\Gamma \Rightarrow \Delta \subseteq^S \Sigma \Rightarrow \Pi$. ■

<figure><img src="image_4.png" /></figure>
**Proposition 45.** Let $\mathcal{D}$o be a derivation with root a non-axiomatic sequent $T = \Gamma \Rightarrow \Delta$
obtained by applying R1-rules to $\Gamma \Rightarrow \Delta^\sharp$, then any $T'$ occurring in $\mathcal{D}$o has size $O(|T|^{\lvert T \rvert+1})$.

**Proof.** Let $T'$ be any sequent occurring in $\mathcal{D}o$ We first prove that $md(T') = md(T)$.
This is proved by induction on the depth of $T'$ in $\mathcal{D}o$: the base is $T' = T$, whence
trivial; for the inductive step let the claim holds for the conclusion of a rule (R), we
prove that it holds for its premise(s), one of which is $T'$. As an example we show the
case of $(\Box_L)$. Let $T_1 = \Sigma, \Box A \Rightarrow \Pi, [\Phi \Rightarrow \Psi]$, so that $T' = \Sigma, \Box A \Rightarrow \Pi, [\Phi, A \Rightarrow \Psi]$. We have that $md(T_1) = \max(\max(\mathcal{T}(\Sigma), \mathcal{T}(A) + 1), \mathcal{T}(\Pi), \max(\mathcal{T}(\Phi), \mathcal{T}(\Psi)) + 1) = \max(\mathcal{T}(\Sigma), \mathcal{T}(A) + 1, \mathcal{T}(\Pi), \mathcal{T}(\Phi) + 1, \mathcal{T}(\Psi) + 1) = \max(\max(\mathcal{T}(\Sigma), \mathcal{T}(A) + 1), \mathcal{T}(\Pi), \max(\mathcal{T}(\Phi), \mathcal{T}(\Psi), A) + 1) = \mathcal{T}(T')$. The other cases are similar.

Let $\mathcal{T}_{T'}$ be the tree associated to $T'$. By the previous claim, we have $h(\mathcal{T}_{T'}) = md(T') = md(T) \le |T|$. Moreover, each node $N$ of $\mathcal{T}_{T'}$, is a pair of sets formulas belonging to $\mathrm{Sub}(T') \subseteq \mathrm{Sub}(T)$ whence $|N| \le 2 \times |T|$. Finally each node $N$ has as children either $[\cdot]$-blocks inherited from the root $T$, whose number is $\le |T|$, or created by subformulas $\diamond B \in \mathrm{Sub}(T') \subseteq \mathrm{Sub}(T)$, whence their number is again $\le |T|$. In conclusion we have that $\mathcal{T}_{T'}$ is a tree of height $md(T) = O(|T|)$ where each node has size $O(|T|)$ and has $O(|T|)$ children, whence $\mathrm{Card}(\mathcal{T}_{T'}) = O(|T|^{\lvert T \rvert})$ so that $|T'| = O(|T|) \times O(|T|^{\lvert T \rvert}) = O(|T|^{\lvert T \rvert+1})$ $\quad \blacksquare$

**Lemma 47.** Given a sequent *S* occurring as a leaf of a derivation *D* with root ⇒ *A*:

1. Let $T \in \mathcal{S}$, where $T = \Gamma \Rightarrow \Delta$, for every rule (R) if $T$ satisfies the R-saturation condition on some formulas $A_i$ and/or blocks $\langle T_j \rangle$, $[T_k]$ *before* the execution of (the body of) the repeat loop (lines 3-14), then $T$ satisfies the R-condition on the involved $A_i$, $\langle T_j \rangle$, $[T_k]$ *after* the execution of it.

2. Let $T \in \mathcal{S}$, if $T$ is blocked in $S$ *before* the execution of (the body of) the repeat loop, then it is still so *after* it.

**Proof.** Concerning 1. it is obvious for all rules (R) except for (trans) and (inter) as the calculus is cumulative. Concerning (trans): suppose $T = \Gamma \Rightarrow \Delta' \langle \Sigma \Rightarrow \Pi \rangle$ and $\Gamma \subseteq \Sigma$ *before* the execution of repeat loop, we can suppose that $T$ satisfies this condition because of a previous execution of the repeat loop of Procedure (as the root of $\mathcal{D}$ does not satisfies it): namely by **EXP2** executed in line 12. Thus $T$ is already R1-saturated, and this implies that $\Gamma$ cannot be expanded anymore, no matter which rules are applied to $\Sigma \Rightarrow \Pi$, whence the inclusion $\Gamma \subseteq \Sigma$ will always hold, in particular after the execution of the repeat loop. The reasoning for (inter)-rule is similar: the inclusion $\Lambda \Rightarrow \Theta \subseteq \mathcal{S} \Phi \Rightarrow \Psi$ involved in the saturation condition will be preserved for the same reason (in particular because $\Lambda \Rightarrow \Theta$ is R1-saturated).

Concerning 2. the procedure checks whether $T$ is blocked in $S$ at line 10, this means
that (i) $S$ is already global R2 saturated (whence also $T$), (ii) $T$ is blocked in $S$ by some
$S_1 \in \mathcal{S} \in S$ in $S$, (iii) because of $\in^{(\cdot)}$-minimality, for all $S' \in \mathcal{S} \in S$, such that $T \in^{(\cdot)} S'$, we have
that $S'$ is R3-saturated, thus no rule can further modify neither $S'$, nor $T$ (nor $S_1$) during
the execution of (the body of) the procedure. Thus $T$ will be still blocked in $S$ after it. ◀

**Lemma 48.** Given a formula *A*, let *Seq*(*A*) be the set of sequents that may occur in any possible derivation with root ⇒ *A*. Let *Seq*(*A*)/*≈* be quotient of *Seq*(*A*) with respect to block-equivalence ≈ as defined in Definition 39. Then *Seq*(*A*)/*≈* is finite.

**Proof.** First observe that block-equivalence $\approx$ is defined by means of the $\sharp$-images of two sequents, thus it suffices to show that the set $\Phi_A := \{\Gamma \Rightarrow \Delta^\sharp | \Gamma \Rightarrow \Delta \in \mathrm{Seq}(A)\}$ is finite. By proposition 45 we know that every sequent $\Gamma \Rightarrow \Delta^\sharp \in \Phi_A$ has a bounded size, (namely
11

$O(|A|^{|A|+1})$. Moreover observe that $Sub(\Gamma \Rightarrow \Delta^\sharp) \subseteq Sub(A)$. Thus there may be only finitely-many distinct $\Gamma \Rightarrow \Delta^\sharp$, that is $\Phi_A$ is finite. ◀

**Theorem 49.** Let $A$ be a formula. Proof-search for the sequent $\Rightarrow A$ terminates with a finite derivation in which any leaf is either an axiom or global-saturated.

**Proof.** (Sketch) We prove that PROCEDURE($A$) terminates producing a finite derivation, in this case all leaves are axioms or global-saturated. A non-axiomatic leaf $S$ is necessarily global-saturated, otherwise $S$ would be further expanded in Step 8 of PROCEDURE($A$) and it would not be a leaf. Thus it suffices to prove that the procedure produces a finite derivation. Let $\mathcal{D}$ be built by PROCEDURE($A$). First we claim that all branches of $\mathcal{D}$ are finite. Suppose for the sake of a contradiction that $\mathcal{D}$ contains an infinite branch $\mathcal{B} = S_0, \dots, S_i, \dots$, with $S_0 = \Rightarrow A$. The branch is generated by applying repeatedly $\mathbf{EXP1}(\cdot)$, $\mathbf{EXP2}(\cdot)$ and $\mathbf{EXP3}(\cdot)$ to each $S_i$ (or more precisely to some $T_i \in^+ S_i$). Since each one of these sub-procedures terminates, the three of them must infinitely alternate on the branch. By (invariant) Lemma, if $T_i \in^+ S_i$ satisfies a saturation condition for a rule (R) or is blocked in ($S_i$) it will remain so in all $S_j$ with $j > i$. That is to say, further steps in the branch cannot "undo" a fulfilled saturation condition or "unblock" a blocked sequent. We can conclude that the branch must contain infinitely many phases of $\mathbf{EXP3}(\cdot)$ each time applied to an unblocked sequent in some $S_i$. This entails that $\mathcal{B}$ contains infinitely many sequents that are not $\simeq$-equivalent, but this contradicts previous lemma 48. Thus each branch of the derivation $\mathcal{D}$ built by PROCEDURE($A$) is finite. To conclude the proof, just observe that $\mathcal{D}$ is a tree whose branches have a finite length and is finitely branching (namely each node/sequent has at most 2 successors, as the rules of $\mathbf{CC}_{\mathbf{FIK}}$ are at most binary), therefore $\mathcal{D}$ is finite. ◀

**Proposition 51.** The countermodel $\mathcal{M}_S$ determined by a global-saturated $S$ is a bi-relational model satisfying the hereditary property(HP) and forward confluence(FC).

**Proof.** In the following proof, we abbreviate $R_S, \le_S$ as $R$ and $\le$ respectively for readability.

For (HP), take arbitrary $x_{S_1}, x_{S_2} \in W_S$ with $x_{S_1} \le x_{S_2}$. Suppose $S_1, S_2$ are of form $\Gamma_1 \Rightarrow \Delta_1$ and $\Gamma_2 \Rightarrow \Delta_2$ respectively, then $\Gamma_1 \Rightarrow \Delta_1 \subseteq^S \Gamma_2 \Rightarrow \Delta_2$. By definition, it follows $\Gamma_1 \subseteq \Gamma_2$. As $V_S(x_{S_1}) = \{p \mid p \in \Gamma_1\}$ and $V_S(x_{S_2}) = \{p \mid p \in \Gamma_2\}$, we have $V_S(x_{S_1}) \subseteq V_S(x_{S_2})$.

For (FC), take arbitrary $x_{\Gamma \Rightarrow \Delta}, x_{\Sigma \Rightarrow \Pi}, x_{\Lambda \Rightarrow \Theta} \in W_S$ with $x_{\Gamma \Rightarrow \Delta} \le x_{\Sigma \Rightarrow \Pi}$ and $Rx_{\Gamma \Rightarrow \Delta}x_{\Lambda \Rightarrow \Theta}$, our goal is to find some $x_0 \in W_S$ s.t. both $x_{\Lambda \Rightarrow \Theta} \le x_0$ and $Rx_{\Sigma \Rightarrow \Pi}x_0$ hold. Since $Rx_{\Gamma \Rightarrow \Delta}x_{\Lambda \Rightarrow \Theta}$, by the definition of $R$, we see that $[\Lambda \Rightarrow \Theta] \in \Delta$ and hence $\Gamma \Rightarrow \Delta$ can be written explicitly as $\Gamma \Rightarrow \Delta'$, $[\Lambda \Rightarrow \Theta]$. Meanwhile, since $x_{\Gamma \Rightarrow \Delta} \le x_{\Sigma \Rightarrow \Pi}$, by the definition of $\le$, we have $\Gamma \Rightarrow \Delta'$, $[\Lambda \Rightarrow \Theta] \subseteq^S \Sigma \Rightarrow \Pi$. By the definition of structural inclusion, there is a block $[\Phi \Rightarrow \Psi] \in \Pi$ s.t. $\Lambda \Rightarrow \Theta \subseteq^S \Phi \Rightarrow \Psi$, and then $\Sigma \Rightarrow \Pi$ can be written explicitly as $\Sigma \Rightarrow \Pi'$, $[\Phi \Rightarrow \Psi]$. Since $\Phi \Rightarrow \Psi \in^+ \Sigma \Rightarrow \Pi \in^+ S$ and $\in^+$ is transitive, we see that $x_{\Phi \Rightarrow \Psi} \in W_S$ as well. Take $x_{\Phi \Rightarrow \Psi}$ to be $x_0$, by the construction of $\mathcal{M}_S$, it follows directly $x_{\Lambda \Rightarrow \Theta} \le x_0$ and $Rx_{\Sigma \Rightarrow \Pi}x_0$. ◀

**Lemma 52.** Let $S$ be a global-saturated sequent and $\mathcal{M}_S$ be defined as above. (a). If $A \in \Phi$, then $\mathcal{M}_S, x_{\Phi \Rightarrow \Psi} \models A$; (b). If $A \in \Psi$, then $\mathcal{M}_S, x_{\Phi \Rightarrow \Psi} \not\models A$.

**Proof.** We prove the lemma by induction on the complexity of $A$. For convenience, we abbreviate $x_{\Phi \Rightarrow \Psi}, \le_S, R_S, W_S$ as $x, \le, R, W$ respectively in the following proof.

- $A$ is of form $p, \perp, \top, B \lor C, B \land C$. These cases are similar and relatively trivial, here we only give the proof for $B \land C$ as an example. Recall that both R3-saturated and blocked
sequents are already R1-saturated, so it is not necessary to distinguish the cases whether $\Phi \Rightarrow \Psi$ is blocked or not.

For (a), let $B \wedge C \in \Phi$. By saturation we have that both $B, C \in \Phi$. Thus by IH, we have $x \Vdash B$ and $x \Vdash C$, whence $x \Vdash B \wedge C$.

For (b), let $B \wedge C \in \Psi$. By saturation either $B \in \Psi$ or $C \in \Psi$. Thus by IH either $x \Vdash B$ and $x \Vdash C$ hold. In both cases we get $x \Vdash B \wedge C$.

- $A$ is of form $B \supset C$. For (a), let $B \supset C \in \Phi$. Assume for the sake of a contradiction that $x \nVdash B \supset C$. Then there exists a world $x_0 = x_{\Sigma \to \Pi} \in W_S$, with $x \le x_0$ such that $x_0 \Vdash B$ and $x_0 \nVdash C$. By IH, we have $B \notin \Pi$ and $C \notin \Sigma$. Meanwhile, since $\Sigma \Rightarrow \Pi$ satisfies the saturation condition associated with $(\supset_L)$ (no matter whether is blocked or not), either $B \in \Pi$ or $C \in \Sigma$, and we have a contradiction.

For (b), let $B \supset C \in \Psi$. We distinguish whether $\Phi \Rightarrow \Psi$ is blocked sequent or not. Assume first that $\Phi \Rightarrow \Psi$ is not blocked, then it satisfies one of the two saturation conditions associated with $(\supset_R)$ for $B \supset C$:

(1). $B \in \Phi$ and $C \in \Psi$. In this case by IH, it follows $x \Vdash B$ and $x \nVdash C$. By reflexivity $x \le x$, we conclude $x \Vdash B \supset C$.

(2). there is a block $\langle \Lambda \Rightarrow \Theta \rangle \in \Psi$ s.t. $B \in \Lambda$ and $C \in \Theta$. By saturation (and Proposition 35), we have $\Phi \Rightarrow \Psi \subseteq^S \Lambda \Rightarrow \Theta$, whence $x \le x_{\Lambda \to \Theta}$. Since $B \in \Lambda$ and $C \in \Theta$, by IH, we have $x_{\Lambda \to \Theta} \Vdash B$ and $x_{\Lambda \to \Theta} \nVdash C$, thus $x \Vdash B \supset C$.

Assume now that $\Phi \Rightarrow \Psi$ is blocked and it does not satisfy the previous condition (1), otherwise we conclude the proof as before. By definition, there is an unblocked sequent $\Sigma \Rightarrow \Pi \in \Sigma^+$ s.t. $\Phi \Rightarrow \Psi$ is blocked by it. Then we have $\Sigma \Rightarrow \Pi \simeq \Phi \Rightarrow \Psi$, which implies $\Pi^\sharp = \Psi^\sharp$, thus also $B \supset C \in \Pi$. Observe that $\Sigma \Rightarrow \Pi \simeq \Phi \Rightarrow \Psi$ implies $\Phi \Rightarrow \Psi \subseteq^S \Sigma \Rightarrow \Pi$ hold, thus (*) $x \le x_{\Sigma \to \Pi}$ by model construction. Given that $\Sigma \Rightarrow \Pi$ is R3-saturated, it already satisfies the saturation condition associated with $(\supset_R)$ for $B \supset C$. Since $\Sigma \Rightarrow \Pi \simeq \Phi \Rightarrow \Psi$, we get that $\Sigma \Rightarrow \Pi$ does not satisfy condition (1), thus it satisfies condition (2), that is there is there is a block $\langle \Lambda \Rightarrow \Theta \rangle \in \Pi$ such that $B \in \Lambda$ and $C \in \Theta$. We have $\Sigma \Rightarrow \Pi \subseteq^S \Lambda \Rightarrow \Theta$, whence $x_{\Sigma \to \Pi} \le x_{\Lambda \to \Theta}$ so that by (*) and transitivity also $x \le x_{\Lambda \to \Theta}$. Then we proceed as in case (2) above.

- $A$ is of form $\Box B$. For (a), let $\Box B \in \Phi$. Similar as the ($\supset$)-case, $\Phi \Rightarrow \Psi$ satisfies the saturation condition associated with ($\Box_R$) for $\Box B$ regardless of whether the sequent itself is blocked or not. Assume for the sake of a contradiction that $x \nVdash \Box B$. Then there exists $x_{\Sigma \to \Pi}, x_{\Lambda \to \Theta}$ denoted as $x_1, x_2$ s.t. $x \le x_1, Rx_1x_2$ and $x_2 \nVdash B$. By IH we see that $B \notin \Lambda$. Meanwhile, according to the model construction, we see that $\Phi \Rightarrow \Psi \subseteq^S \Sigma \Rightarrow \Pi$ and $[\Lambda \Rightarrow \Theta] \in \Pi$. Moreover we have $\Phi \subseteq \Sigma$, thus $\Box B \in \Sigma$ as well. Also, since $\Sigma \Rightarrow \Pi$ is of form $\Sigma \Rightarrow \Pi', [\Lambda \Rightarrow \Theta]$, by the saturation condition associated with ($\Box_L$), we have $B \in \Lambda$, which leads to a contradiction.

For (b), let $\Box B \in \Psi$. We distinguish whether $\Phi \Rightarrow \Psi$ is blocked or not. Assume that $\Phi \Rightarrow \Psi$ is not blocked, then it satisfies the one of the two saturation conditions associated with ($\Box_R$) for $\Box B$:

(1). there is a block $[\Lambda \Rightarrow \Theta] \in \Psi$ with $B \in \Theta$. By IH, we have $x_{\Lambda \to \Theta} \nVdash B$. By reflexivity $x \le x$ and model construction $Rx x_{\Lambda \to \Theta}$, so that $x \nVdash \Box B$.

(2). there is a block $\langle \Omega \Rightarrow [\Lambda \Rightarrow \Theta], \Xi \rangle \in \Psi$ with $B \in \Theta$. Denote the sequent $\Omega \Rightarrow [\Lambda \Rightarrow \Theta], \Xi$ by $S_0$. Since $\Phi \Rightarrow \Psi$ is saturated with (trans) and (inter), by Proposition 35, we have $\Phi \Rightarrow \Psi \subseteq^S S_0$. According to the model construction, we see that $x \le x_{S_0}$ and $Rx_{S_0}x_{\Lambda \to \Theta}$. Since $B \in \Theta$, by IH we have $x_{\Lambda \to \Theta} \nVdash B$ and we can conclude $x \nVdash \Box B$.
Assume that $\Phi \Rightarrow \Psi$ is blocked and does not satisfy condition (1) for $\Box B$, otherwise the proof proceeds as in case (1) above. Then there is an unblocked sequent $\Sigma \Rightarrow \Pi \in^+ S$ such that $\Phi \Rightarrow \Psi$ is blocked by it. Then $\Sigma \Rightarrow \Pi \simeq \Phi \Rightarrow \Psi$, which implies $\Pi^\sharp = \Psi^\sharp$, so $\Box B \in \Pi$ as well. Moreover, by definition, we have $\Phi \Rightarrow \Psi \subseteq^S \Sigma \Rightarrow \Pi$, whence by model construction (**) $x \le x_{\Sigma \Rightarrow \Pi}$. Given that $\Sigma \Rightarrow \Pi$ is R3-saturated, it satisfies the saturation condition associated with ($\Box_R$) for $\Box B$, but since $\Sigma \Rightarrow \Pi \simeq \Phi \Rightarrow \Psi$, we have that $\Sigma \Rightarrow \Pi$ does not satisfy condition (1), thus it must satisfy condition (2). Therefore there is there is a block $\langle \Omega \Rightarrow [\Lambda \Rightarrow \Theta], \Xi \rangle \in \Pi$, such that $B \in \Theta$. Letting $S_0 = \Omega \Rightarrow [\Lambda \Rightarrow \Theta], \Xi$, we have $x_{\Sigma \Rightarrow \Pi} \le x_{S_0}$ and $Rx_{S_0}x_{\Lambda \Rightarrow \Theta}$. By (**) we have also $x \le x_{S_0}$ and we conclude as in case (2) above.

A is of form $\diamond B$. It is not necessary to distinguish cases when $\Phi \Rightarrow \Psi$ is blocked or not. For (a), let $\diamond B \in \Phi$. Then by the saturation condition associated with ($\diamond_L$), there is a block $[\Lambda \Rightarrow \Theta] \in \Psi$ s.t. $B \in \Lambda$. By model construction, we have $Rxx_{\Lambda \Rightarrow \Theta}$ and by IH, we get $x_{\Lambda \Rightarrow \Theta} \models B$, thus $x \models \diamond B$.

For (b), let $\diamond B \in \Psi$. Let $y \in W$, with $Rxy$ we show that $y \not\models B$. If $Rxy$ it must be $y = x_{\Lambda \Rightarrow \Theta}$ and $[\Lambda \Rightarrow \Theta] \in \Psi$. By saturation condition for ($\diamond_R$), it follows that $B \in \Theta$, thus by IH $x_{\Lambda \Rightarrow \Theta} \not\models B$ and we are done.

This completes our proof.

<figure><img src="image_5.png" /></figure>

**Theorem 53** For any formula $A \in \mathcal{L}$, if $\models A$, then $\Rightarrow A$ is provable in $CC_{\mathbf{FIK}}$.

**Proof.** By contraposition. Given a formula $A$, if $A$ is unprovable in $CC_{\mathbf{FIK}}$, then we see that $PROCEDURE(A)$ produces a derivation containing a non-axiomatic global saturated leaf $S = \Gamma \Rightarrow \Delta$ such that $A \in \Delta$. By the truth lemma, $A$ is not valid in the model $\mathcal{M}_S$. ►

## References

### References

1. Arisaka R., Das A., Straßburger L.: *On nested sequents for constructive modal logics*. Logical Methods in Computer Science **11** (2015) 1–33.

2. Balbiani, P., Diéguez, M., Fernández-Duque, D.: *Some constructive variants of S4 with the finite model property*. In *Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science — LICS 2021, Rome, Italy*. IEEE (2021) 1–13.

3. Bellin G., De Paiva, V., Ritter, E.: *Extended Curry-Howard correspondence for a basic constructive modal logic*. In *Proceedings of the 2nd Workshop on Methods for Modalitie — M4M 2001, Amsterdam, The Netherlands*.

4. Bierman, G., de Paiva, V.: *On an intuitionistic modal logic*. Studia Logica **65** (2000) 383–416.

5. Božić, M., Došen, K.: *Models for normal intuitionistic modal logics*. Studia Logica **43** (1984) 217–245.

6. Brünnler, K.: *Deep sequent systems for modal logic*. Archive for Mathematical Logic **48** (2009): 551–577.

7. Dalmonte T.: *Wijesekera-style constructive modal logics*. In *Advances in Modal Logic. Volume 14*. College Publications (2022) 281–304

8. Das, A. and Marin, S.: *On intuitionistic diamonds (and lack thereof) Accepted for Automated Reasoning with Analytic Tableaux and Related Methods*. (2023)

9. Ewald, W.: *Intuitionistic tense and modal logic*. The Journal of Symbolic Logic **51** (1986) 166–179.
10 Fairtlough, M., Mendler, M.: *Propositional Lax Logic*. Information and Computation **137** (1997) 1–33.

11 Fischer Servi, G.: *On modal logic with an intuitionistic base*. Studia Logica **36** (1977) 141–149.

12 Fischer Servi, G.: *Semantics for a class of intuitionistic modal calculi*. Bulletin of the Section of Logic **7** (1978) 26–29.

13 Fischer Servi, G.: *Axiomatizations for some intuitionistic modal logics*. Rendiconti del Seminario Matematico Università e Politecnico di Torino **42** (1984) 179–194.

14 Fitch, F.: *Intuitionistic modal logic with quantifiers*. Portugaliae mathematica **7** (1948) 113–118.

15 Fitting, M.: *Nested Sequents for Intuitionistic Logics*. Notre Dame J. Formal Log. **55**(1) (2014) 41–61.

16 Font, J.: *Modality and possibility in some intuitionistic modal logics*. Notre Dame Journal of Formal Logic **27** (1986) 533–546.

17 Galmiche D., Salhi Y.: *Label-free natural deduction systems for intuitionistic and classical modal logics*. Journal of Applied Non-Classical Logics **20** (2010) 373–421.

18 Kojima, K., Igarashi, A.: *Constructive linear-time temporal logic: proof systems and Kripke semantics*. Information and Computation **209** (2011) 1491–1503.

19 Marin S., Morales M., Straßburger L.: *A fully labelled proof system for intuitionistic modal logics*. Journal of Logic and Computation **31** 998–1022 (2021).

20 Mendler M., Scheele, S.: *Cut-free Gentzen calculus for multimodal CK*. Information and Computation **209** (2011) 1465–1490.

21 Plotkin, G., Sterling, C.: *A framework for intuitionistic modal logics*. In *Theoretical Aspects of Reasoning About Knowledge*. Morgan Kaufmann Publishers (1986) 399–406.

22 Prawitz, D.: *Natural deduction: A proof-theoretical study*. Almqvist & Wiksell (1965).

23 Simpson, A.: *The Proof Theory and Semantics of Intuitionistic Modal Logic*. PhD Thesis at the University of Edinburgh (1994).

24 Wijesekera, D.: *Constructive modal logics I*. Annals of Pure and Applied Logic **50** (1990) 271–301.