## Semantical Analysis of Intuitionistic Modal Logics between CK and IK

## Jim de Groot, Ian Shillito &amp; Ranald Clouston

{jim.degroot,ian.shillito,ranald.clouston}@anu.edu.au

The Australian National University, Canberra, Ngunnawal &amp; Ngambri Country, Australia

## Abstract

The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant.

## 1 Introduction

Which logic provides the foundation for intuitionistic modal logics, by analogy with the logic K for classical modal logics? If we consider necessity, 2 , but disregard possibility, 3 , then the answer has, until recently, appeared uncontroversial: we extend intuitionistic propositional logic with the inference rule of necessitation (if p is a theorem, then so is 2 p ) and axiom

$$( K _ { \square } ) \ \square ( \varphi \rightarrow \psi ) \rightarrow ( \square \varphi \rightarrow \square \psi )$$

Since this logic, which we here call CK 2 , was introduced by Boˇi´ and Doˇ sen [4], it and its extensions (for z c example, with the S4 axioms) have been studied and applied in a literature too large to summarise here; we briefly mention its use in modern type theory to capture notions ranging from the distinction between contextual and categorical validity [20], to the productivity of recursive definitions [3], to global elements in synthetic topology [24].

How CK 2 should be extended with 3 has received various answers. Consider the following axioms, where we follow the naming conventions of Dalmonte, Grellois, and Olivetti [6]:

- ( K 3 ) 2 ( φ → ψ ) → ( 3 φ → 3 ψ )
- ( C 3 ) 3 ( φ ∨ ψ ) → 3 φ ∨ 3 ψ

Constructive K ( CK ) [2] extends CK 2 with K 3 only; Wijisekera's K ( WK ) [28] extends CK further with N 3 . These logics are proof theoretically natural, attained by restricting the sequent calculus for classical K to single conclusions ( CK ) or zero or one conclusions ( WK ). Both were originally also motivated by applications in AI: the notion of context in knowledge representation and reasoning (CK) [9], and representing states with partial knowledge, as well as constructive concurrent dynamic logic ( WK ) [29]. Intuitionistic K ( IK ) [11] 1 has all the above axioms. It is the logic specified by Fischer Servi's translation to classical ( K S4 , )-bimodal logic, and by the standard translation to intuitionistic first order logic [25]. Besides, IK also respects the G¨ odel-Gentzen double negation translation from classical modal logic, although this also holds for the logic without C 3 [8]. These are by no means the only options for logics between CK and IK ; we mention also Kojima's logic for intuitionistic neighborhood models [17], which lies between CK and WK , and Forward confluenced IK ( FIK ) [1], which modifies IK by replacing I 32 with a weaker axiom.

- ( N 3 ) 3 ⊥ → ⊥

$$( I _ { \odot \square } ) \ ( \odot \varphi & \to \square \psi ) \to \square ( \varphi \to \psi ) \\ \text{nly; Wijisekera's K (WK) [28] extends CK f }$$

While different notions of 3 have arisen from different motivations, it has generally been assumed that only 3 is controversial, and that these logics agree with CK 2 on their 3 -free fragments. This was shown

1 The name IK has been used inconsistently in the literature, sometimes for the logics that we here call CK 2 and CK .

to be incorrect in Grefe's 1999 thesis [14]. Grefe showed that the 3 -free formula ( ¬ 2 ⊥ → 2 ⊥ → ) 2 ⊥ holds in IK but not in CK 2 . This observation was not published, and was only recently rediscovered by Das and Marin [8], who showed, among other results, that while IK is not conservative over CK 2 , the logic CK ⊕ N ⊕ C , and hence its sublogics such as CK and WK , are.

3 3 The (re)discovery that the logics between CK and IK are not as well understood as previously thought raises many questions. With each new axiom that is considered in this space, these questions multiply. Working via Hilbert axiomatisations only is notoriously intractable, and while proof theoretic methods were used successfully by Das and Marin to clarify the status of CK ⊕ N 3 ⊕ C 3 , the effort involved was considerable. In this paper we instead explore the (bi)relational semantics of Kripke frames. Such semantics are known for CK [19], WK [28], FIK [1], and IK [10], although imprecisions in the treatment of WK led to the semantics for that logic being called 'inconclusive' [19]. Moreover, the different choices made for both conditions on the relations and the intepretations of the modal operators impede comparisons between these logics.

In this paper we instead take the relational semantics for CK as a unifying semantics, and give frame conditions for each of the axioms N 3 , C 3 , and I 32 . This allows us to provide completeness proofs for each of these axioms independently. In particular, this answers the challenge of Das and Marin [8, Section 7] to provide relational semantics for logics between WK and IK . We use these semantics to analyse the 3 -free fragments, making the new observations that CK ⊕ C 3 ⊕ I 32 , and hence CK ⊕ I 32 , are conservative over CK 2 . This is a surprising result, as no logics including I 32 were previously shown to retain conservativity; it is now clear that the combination of I and N is to blame here.

32 3 We formalise all our results in the Coq Proof Assistant [26], which not only adds confidence to our results (in particular, relational semantics for WK may now be considered settled), but is a crucial working tool for managing the profusion of logics which arise as one considers new axioms. As a proof of concept of this methodology of working from a base relational semantics for CK with support from Coq, we go on to provide relational semantics and conservativity results for Kojima's logic, and for the weakening of I 32 used in FIK .

This paper begins by introducing basic syntax in Section 2. We give sound and strongly complete relational semantics for our base logic CK in Section 3, then give frame conditions for N 3 , C 3 , and I 32 in Section 4, and compare the resulting logics' 3 -free fragments in Section 5. We extend our techniques to other axioms from the literature in Section 6. We finish by discussing our Coq formalisation in Section 7 and surveying possible further work in Section 8. Each mechanised result in the paper is accompanied by a clickable rooster symbol ' ' leading to its mechanisation. The full mechanisation can be found at https://ianshil.github.io/CK .

## 2 Constructive K and its extensions

In this section we fix the syntax and axiomatic calculus for CK and its extensions. Taking a countably infinite set of propositional variables Prop = { p, q, r, . . . } , we define the language L via the following grammar ( ):

$$\varphi \, \colon = \, p \in \text{Prop} \, | \, \perp \, | \, \varphi \wedge \varphi \, | \, \varphi \vee \varphi \, | \, \varphi \to \varphi \, | \, \bigotimes \varphi \\ \varpi \, \colon = \, \omega \to 1 \text{ and } \, \mathbb { T } \, \colon = \, \neg 1 \text{. We use Greek lowercase letters. e.g. } e. \, \omega. \, \psi$$

We abbreviate ¬ φ := φ →⊥ and ⊤ := ¬⊥ . We use Greek lowercase letters, e.g. φ, ψ, χ and δ , to denote formulas, and Greek uppercase letters, e.g. Γ ∆ Φ Ψ, for multisets of formulas. , , , For such a multiset Γ we define the multisets 2 (Γ) := { 2 φ | φ ∈ Γ } and 2 -1 (Γ) := { φ | 2 φ ∈ Γ } and similarly for 3 (Γ) and 3 -1 (Γ). If Γ is finite, ∨ Γ denotes the disjunction of all formulas in Γ. We distinguish the logical connectives in L from those used in our metalogic with a dot on top of the metalogical connectives, e.g. ˙ . ¬ Since Prop is countably infinite and we have finitely many connectives we can enumerate all formulas of L ( ).

All logics we consider in this paper are syntactically defined as extensions of the base logic CK with axioms. We describe this formally by defining a logic parametrised in some set Ax ⊆ L of axioms, so that Ax = ∅ corresponds to CK . 2 For a set Ax of axioms, we denote the set of all instances of axioms in Ax by I ( Ax ).

Definition 2.1 ( ) . Let CKAx ( ) be an axiomatisation of intuitionistic logic ( ) together with K 2 and K 3 . For a set Ax ⊆ L , define the generalised Hilbert calculus CK ⊕ Ax by:

2 In the formalisation we use as parameter a set of formulas closed under substitution. Given a set Ax of axioms, the set of all instances of axioms in Ax is such a set.

$$( \mathbf A x ) & \quad \frac { \varphi \in \mathcal { I } ( \mathbf C K \mathbf A x ) \cup \mathcal { I } ( \mathbf A x ) } { \Gamma \vdash \varphi } & ( \mathbf E l ) & \quad \frac { \varphi \in \Gamma } { \Gamma \vdash \varphi } \\ ( \text{Nec} ) & \quad \frac { \emptyset \vdash \varphi } { \Gamma \vdash \square \varphi } & ( \text{MP} ) & \quad \frac { \Gamma \vdash \varphi } { \Gamma \vdash \psi }$$

$$( \text{Nec} ) & \frac { v + \varphi } { \Gamma \vdash \Box \varphi } & ( \text{MP} ) & \frac { v + \varphi + \varphi + \varphi \to \varphi } { \Gamma \vdash \psi }$$

̸

2 We write Γ ⊢ Ax φ if Γ ⊢ φ is provable in CK ⊕ Ax , and Γ ⊢ Ax φ if ˙ (Γ ¬ ⊢ Ax φ ). We write Γ ⊢ Ax ∆ for ∆ ⊆ L if there is a finite ∆ ′ ⊆ ∆ such that Γ ⊢ Ax ∨ ∆ . If ′ Ax = { A 0 , . . . , A n } is finite, we write CK ⊕ A 0 ⊕···⊕ A n for CK ⊕ Ax .

Sometimes CK ⊕ Ax has an existing name in the literature. For example, CK ⊕ N 3 is known as WK . In such cases, we use both names interchangeably. The rules displayed below, where σ is a uniform substitution, are admissible in CK ⊕ Ax for any set of axioms Ax .

$$\frac { \Gamma \vdash \varphi } { \Gamma, \Gamma ^ { \prime } \vdash \varphi } \quad \frac { \{ \Gamma \vdash \delta \ | \ \delta \in \Delta \} \ \Delta \vdash \varphi } { \Gamma \vdash \varphi } \quad \frac { \Gamma \vdash \varphi } { \Gamma ^ { \sigma } \vdash \varphi ^ { \sigma } } \quad \frac { \Gamma, \varphi \vdash \psi } { \Gamma \vdash \varphi \to \psi } \quad \frac { \Gamma \vdash \varphi } { \Box ( \Gamma ) \vdash \Box \varphi } \\ \text{The three leftmost rules show that $CK\oplus\,Axis$ is a monotone $\Phi$}. \text{compositional $\Phi$} ) \text{ and structural $\Phi$} )$$

The three leftmost rules show that CK ⊕ Ax is a monotone ( ), compositional ( ) and structural ( ) relation, respectively. Furthermore, we can show that Γ ⊢ Ax φ if and only if there is a finite Γ ′ ⊆ Γ such that Γ ′ ⊢ Ax φ ( ). Therefore CK ⊕ Ax is a finitary logic [18]. The fourth rule can be applied in both directions and corresponds to the deduction-detachment theorem ( , ). 3 The fifth rule captures the modal sequent calculus rule ( ).

Definition 2.2. A set of formulas Γ ⊆ L is a theory ( ) if it is deductively closed, i.e. Γ ⊢ Ax φ implies φ ∈ Γ. It is prime ( ) if φ ∨ ψ ∈ Γ implies φ ∈ Γ or ψ ∈ Γ, for all φ, ψ ∈ L .

We note that the prime theories we consider need not be consistent, and can thus contain ⊥ . This reflects the existence of an inconsistent world in the semantics, defined in Section 3.

̸

̸

Lemma 2.3 (Lindenbaum ) . Let Γ ∪ ∆ ⊆ L . If Γ ⊢ Ax ∆ then there is a prime theory Γ ′ ⊇ Γ such that Γ ′ ⊢ Ax ∆.

We often use the Lindenbaum lemma with ∆ of the form { φ } ( ).

## 3 Relational semantics for CK

We present a relational semantics for CK which is a light modification of Mendler and de Paiva [19]. Their semantics is characterised by the interpretation of both modalities over all intuitionistic successors of worlds, and by the existence of worlds that satisfy all formulas, including ⊥ . Such worlds were introduced by Veldman [27] as 'sick' worlds, whereas Mendler and de Paiva call them 'fallible'; we follow Ilik, Lee and Herbelin's exploding terminology [16]. Because all exploding worlds are essentially the same with respect to formula satisfaction we slightly simplify the Mendler-de Paiva semantics by using a single exploding world, instead of a set.

Definition 3.1. A CK -frame ( ) is a tuple ( X, /bomb , ≤ , R ) where ( X, ≤ ) is a preorder, /bomb ∈ X is a maximal element of ( X, ≤ ), and R is a binary relation on X such that /bomb Rx if and only if x = /bomb . We denote by CK the class of all CK -frames.

A valuation is a map V that assigns to each proposition letter an upset of ( X, ≤ ) such that /bomb ∈ V ( p ). A CK -model ( ) is a CK -frame with a valuation. The interpretation of a formula φ at a world x in a CK -model M = ( X, /bomb , ≤ , R, V ) ( ) is defined recursively by

```
\text{node} \mathcal { M } = ( X, \Phi, \leq, \mathcal { H }, V ) \, ( \Phi ) \, \text{is defined recursively by} \\ \mathcal { M }, x \, \| \, \Phi \, \text{ if} \, \text{ } x \in V ( p ) \\ \mathcal { M }, x \, \| \, \Phi \, \| \, \Phi \, \text{ if} \, \text{ } x = \Phi ^ { \prime } \\ \mathcal { M }, x \, \| \, \varphi \, \wedge \, \psi \, \text{ if} \, \text{ } \mathcal { M }, x \, \| \, \varphi \, \text{ and } \mathcal { M }, x \, \| \, \psi \\ \mathcal { M }, x \, \| \, \varphi \, \vee \, \psi \, \text{ if} \, \text{ } \mathcal { M }, x \, \| \, \varphi \, \text{ or } \mathcal { M }, x \, \| \, \psi \\ \mathcal { M }, x \, \| \, \varphi \, \rightarrow \, \psi \, \text{ if} \, \text{ } \mathcal { Y } y \, ( x \leq y \, \text{ and } \mathcal { M }, y \, \| \, \varphi \, \text{ imply } \mathcal { M }, y \, \| \, \psi ) \\ \mathcal { M }, x \, \| \, \square \, \varphi \, \text{ if} \, \text{ } \mathcal { Y } y, z \, ( x \leq y \, \text{ and } y R z \, \text{ imply } \mathcal { M }, z \, \| \, \varphi ) \\ \mathcal { M }, x \, \| \, \diamondsuit \, \varphi \, \text{ if} \, \text{ } \mathcal { Y } y \, ( x \leq y \, \text{ implies } \, \exists z \in X \, s. t. \, y R z \, \text{ and } \mathcal { M }, z \, \| \, \varphi ) \, \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{ } \text{                                                                                                                                                                                                        
\text{this notably implies that CK and WK satisfy the deduction theorem. Mendler and de Paiva make the opposite clair}
\text{ote} 2 \, \text{ in their analysis of Wijiisekera's work, but despite some imprecision in his definitions, we believe that Wijes}
\, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot.
```

3 This notably implies that CK and WK satisfy the deduction theorem. Mendler and de Paiva make the opposite claim [19, Footnote 2] in their analysis of Wijisekera's work, but despite some imprecision in his definitions, we believe that Wijesekera had in mind a calculus like ours where the rule ( Nec ) has ∅ , and not a general Γ, in its premise.

Let Γ ∪ { φ } ⊆ L and let M be a CK -model. We write M , x ⊩ Γ if x satisfies all ψ ∈ Γ, and M validates Γ ⊢ φ if M , x ⊩ Γ implies M , x ⊩ φ for all worlds x in M . A CK -frame X validates Γ ⊢ φ if every model of the form ( X , V ) validates the consecution, and it validates a formula φ it validates the consecution ∅ ⊢ φ . If F is a class of CK -frames, then we say that Γ semantically entails φ on F ( ), and write Γ ⊩ F φ , if every CK -frame in F validates Γ ⊢ φ .

We will show that CK -frames form a sound and complete semantics for CK .

Lemma 3.2 (Persistence ) . If M , x ⊩ φ and x ≤ y then M , y ⊩ φ .

Proof. By induction on the structure of φ . The ⊥ case holds because /bomb is maximal. All other cases are as usual.

Proposition 3.3 (Soundness ) . If Γ ⊢ CK φ , then Γ ⊩ CK φ .

Proof. By routine induction on the structure of a proof of Γ ⊢ φ . In particular, validity of (any instance of) the axiom ⊥ → p follows from maximality of /bomb .

Next, we define a canonical model for the logic CK ⊕ Ax , where Ax is any set of axioms. This gives rise to a CK -model that validates precisely the consecutions derivable in CK ⊕ Ax . We can use this to obtain completeness for a specific logic CK ⊕ Ax ′ with respect to some class F of CK -frames by showing that all frames in F validate the axioms in Ax ′ , and that the CK -frame underlying the canonical model is in F . In order to achieve the latter we sometimes have to modify the canonical model construction, as we will see in Theorem 3.7.

While canonical models are often based on theories (Definition 2.2), we adapt Wijesekera's use of segments [28]. These are theories paired with a set of theories that intuitively denote their modal successors. This technique prevents distributivity of diamonds over disjunctions, corresponding to the C 3 axiom. Because we have an exploding world, the theories we use to define our segments are allowed to contain ⊥ .

Definition 3.4. A segment ( ) is a pair (Γ , U ) where Γ is a prime theory and U is a set of prime theories such that:

- 1. if 2 φ ∈ Γ then φ ∈ ∆ for all ∆ ∈ U ;

Write SEG for the set of all segments and define relations ⊂ ∼ ( ) and R ( ) on SEG by:

- 2. if 3 φ ∈ Γ then φ ∈ ∆ for some ∆ ∈ U .

$$( \Gamma, U ) \lesssim ( \Gamma ^ { \prime }, U ^ { \prime } ) \ \text{ iff} \ \Gamma \subseteq \Gamma ^ { \prime }$$

(Γ , U ) R (Γ ′ , U ′ ) iff Γ ′ ∈ U

Note that ⊂ ∼ defines a preorder on SEG . Furthermore, observe that ( L , { L } ) is a segment, and conversely any segment of the form ( L , U ) must have U = { L } : 3 ⊥ ∈ L implies that U is non-empty, and 2 ⊥ ∈ L implies that each of its elements is L . Thus, setting /bomb = ( L , { L } ) ( ) gives rise to a CK -frame X CK ⊕ Ax := ( SEG, /bomb , ⊂ ∼ , R ) ( ). We can equip this frame with the valuation V given by V ( p ) = { (Γ , U ) ∈ SEG | p ∈ Γ } for all p ∈ Prop ( ). Then we obtain the model M CK ⊕ Ax = ( X CK ⊕ Ax , V ) ( ).

Lemma 3.5 ( ) . Let Γ be a prime theory such that 3 φ / ∈ Γ. Then there exists a segment (Γ , U ) such that for all ∆ ∈ U we have φ / ∈ ∆.

̸

In particular, the previous lemma implies that for each prime theory Γ we can construct a segment of the form (Γ , U ): if 3 ⊥ ∈ / Γ we use Lemma 3.5 and if 3 ⊥ ∈ Γ then we can take U to be the set of prime theories containing 2 -1 (Γ).

Proof. For any 3 θ ∈ Γ, we have 2 -1 (Γ) , θ ⊢ Ax φ , for otherwise we would get Γ , 3 θ ⊢ Ax 3 φ hence 3 φ ∈ Γ. Now use the Lindenbaum lemma 2.3 to find a prime theory ∆ θ containing 2 -1 (Γ) and θ but not φ . Then (Γ , { ∆ θ | 3 θ ∈ Γ ) is a segment with the desired property. }

Lemma 3.6 (Truth lemma ) . For any segment (Γ , U ) and formula φ ∈ L we have (Γ , U ) ⊩ φ iff φ ∈ Γ.

Proof. By induction on the structure of φ . The cases for proposition letters and ⊥ hold by construction. The inductive steps for meets, joins and implications are routine.

̸

If φ = 3 ψ then 3 ψ ∈ Γ implies Γ ⊩ 3 ψ by construction. Conversely, if 3 ψ / ∈ Γ then using Lemma 3.5 we can find a segment (Γ , U ′ ) such that ψ / ∈ ∆ for all ∆ ∈ U ′ . Since (Γ , U ) ⊂ (Γ , U ′ ) we have (Γ , U ) ⊩ ψ .

∼ 3

̸

̸

Lastly, if φ = 2 ψ and 2 ψ ∈ Γ then by construction we have (Γ , U ) ⊩ 2 ψ . For the converse, suppose 2 ψ / ∈ Γ. Then 2 -1 (Γ) ⊢ Ax ψ (for otherwise we would have 2 ψ ∈ Γ), so we can use the Lindenbaum lemma to find a prime theory Γ ψ containing 2 -1 (Γ) but not ψ . Now we have that (Γ , U ∪ { Γ ψ } ) is a segment and (Γ , U ) ⊂ ∼ (Γ , U ∪ { Γ ψ } ), so that Γ ψ witnesses the fact that (Γ , U ) ⊩ 2 ψ .

Theorem 3.7 (Strong completeness ) . Let F be a class of frame such that X CK ⊕ Ax ∈ F , and every X ∈ F validates Ax . Then, Γ ⊩ F φ entails Γ ⊢ Ax φ .

̸

̸

Proof. We reason by contrapositive. Suppose Γ ⊢ Ax φ . Then we can find a prime theory Γ ′ containing Γ but not φ , and extend Γ to a segment of the form (Γ ′ , U ) ( ). It follows from the truth lemma that (Γ ′ , U ) ⊩ χ for all χ ∈ Γ while (Γ ′ , U ) ⊩ φ . We have X CK ⊕ Ax ∈ F by assumption, this proves Γ ⊩ F φ .

̸

Remark 3.8. The canonical model construction above can also be performed relative to a finite set Σ of formulas. This then gives rise to a finite canonical model, a truth lemma relative to Σ, and ultimately a finite model property. Since finite model properties are beyond the scope of this paper we omit the details.

As the class of frames CK vacuously validates all additional axioms of CK , i.e none, and the frame X CK ∈ CK , we exploit the result above to obtain strong completeness for CK .

Theorem 3.9 (Strong completeness for CK ) . If Γ ⊩ CK φ then Γ ⊢ CK φ .

Remark 3.10. Wijesekera [28] uses a similar construction as above to obtain completeness for WK . Besides incorporating an inconsistent world, the main difference is that our canonical model is based on the set of all segments, while Wijesekera uses recursion to generate a model from a given segment. We also note that Wijesekera claims completeness with respect to partially ordered frames, but their canonical model construction only gives a preorder. The claim for partially ordered frames can be recovered via an unravelling construction [5, Section 3.3].

## 4 Three axioms between CK and IK

The logic IK can be obtained by extending CK with N 3 , C 3 and I 32 . This section examines these three axioms individually. We give frame conditions that guarantee validity for each of them, and then refine these to frame correspondence conditions. While the latter conditions provide sound and strongly complete semantics for the extension of CK with any combination of N 3 , C 3 and I 32 , we use the former when possible because of their greater simplicity. In particular, we provide the birelational semantics for CK ⊕ N 3 ⊕ C 3 called for by Das and Marin [8, Section 7].

Definition 4.1. Let X = ( X, /bomb , ≤ , R ) be a CK -frame. We identify three frame conditions ( , , ):

$$( N _ { \diamondsuit } \text{-suff} ) & \ \forall x \ ( x R _ { \theta } ^ { \prime } \text{ implies } x = \theta ^ { \prime } ) \\ ( C _ { \diamond } \text{-suff} ) & \ \forall x \, \exists x ^ { \prime } \, ( x \leq x ^ { \prime } \text{ and } \forall y, z \, ( \text{if } x \leq y \text{ and } x ^ { \prime } R z \\ & \quad \text{ then } \exists w \in X \ s. t. \ y R w \text{ and } z \leq w ) ) \\ ( \text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text$$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\tt$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text	$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text#$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text
$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text}$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text{$\text                                                                                                                                                                                                         }                                                                                                                                                                                                       
                                                                                                                                                                                                        "                                                                                                                                                                                                        -                                                                                                                                                                                                       .                                                                                                                                                                                                        +                                                                                                                                                                                                        *                                                                                                                                                                                                        +#                                                                                                                                                                                                        */$$

Proposition 4.2. Let X = ( X, /bomb , ≤ , R ) be a frame and A ∈ { N 3 , C 3 , I 32 } . If X satisfies ( A -suff), then X validates the axiom A .

Proof. This result ( , , ) follows from the fact that each of the conditions above implies the correspondence condition of the axiom under consideration ( , , ), given below.

Remark 4.3. If we take x = x ′ in ( C 3 -suff), we obtain a stronger condition ( ),

$$( C _ { \diamond } \text{-strong} ) \ \forall x, y, z \ ( \text{if $x\leq y$ and $xRz$ then $\existsw\ (yRw\ and $z\leq w)$} ).$$

This is a standard frame condition for the semantics of IK [10, 21]. It implies that we can ignore the universal quantifier in the interpretation of 3 φ , looking only at modal successors of the current world. In presence of ( C 3 -strong), condition ( I 32 -suff) is equivalent to ( )

$$( \mathfrak { I } _ { \partial \square } \text{-weak} ) \ \forall x, y, z \ ( \text{if } x R y \leq z \text{ then } \exists u \ ( x \leq u R z ) ),$$

which is also used in the standard semantics of IK .

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-99aa4fd4-870a-4df7-860c-a1dae505909c.jpg)

3

3

32

3

32

Figure 1: Sufficient conditions for validity of N 3 , C 3 and I 32 . Unlabelled arrows denote the intuitionistic relation. Solid arrows indicate universally quantified relations, while the dashed ones indicate existential ones.

The five frame conditions introduced in Definition 4.1 and Remark 4.3 are depicted in Figure 1. While these are sufficient to ensure validity of certain axioms, none of them are necessary. The next examples illustrate this for ( N 3 -suff) and ( I 32 -suff).

Example 4.4. Consider the frame depicted in Figure 2a. This validates 3 ⊥ → ⊥ , because /bomb is the only world that satisfies 3 ⊥ . But it does not satisfy ( N 3 -suff), because xR /bomb .

̸

Example 4.5. Consider the frame given in Figure 2b. This satisfies neither ( I 32 -suff) nor ( I 32 -weak). However, the frame does validate I 32 . To see this, we show that every world that satisfies 3 p → 2 q also satisfies 2 ( p → q ). For z, u, v, w this follows immediately from their lack of modal successors, which implies that they trivially satisfy 2 ( p → q ). For y it follows from the fact that y ⊩ 3 p → 2 q implies that either w ⊩ p or w ⊩ q , so that w ⊩ p → q whence y ⊩ 2 ( p → q ). Lastly, suppose x ⊩ 3 p → 2 q . If none of u, v, w satisfy p then they all satisfy p → q , and hence x ⊩ 2 ( p → q ). If any of u, v, w satisfy p then so does w , which implies x ⊩ 3 p . Then we have x ⊩ 2 q , so that u ⊩ q and hence u, v, w ⊩ q . Therefore u, v, w ⊩ p → q , which again implies x ⊩ 2 ( p → q ).

(a) Frame from Example 4.4.

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-48d3d3ce-b9fc-4313-8afc-b5d1fadc9d56.jpg)

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-529fbb2b-f896-4c9b-a71a-07c0e8ee2dc0.jpg)

(b) Frame from Example 4.5.

Figure 2: Frames witnessing non-necessity of some of the sufficient conditions from Definition 4.1.

We now give exact correspondence conditions for each of the axioms N 3 , C 3 and I 32 . Two of the three correspondence conditions are depicted in Figure 3 below.

Proposition 4.6 ( ) . A frame X = ( X, /bomb , ≤ , R ) validates N 3 if and only if it satisfies:

$$( N _ { \diamond } \text{-corr} ) \ \forall x \, ( \text{if $yR\nmid$ for all $y\geq x$, then $x=\nmid$} )$$

Proof. The correspondence condition implies validity of N 3 by definition. Conversely, if the correspondence condition does not hold then this must be witnessed by a world that satisfies 3 ⊥ but not ⊥ .

To simplify the statement of the correspondence condition for C 3 we use the following notations: if ( X, ≤ ) is a preorder, R a binary relation on X x , ∈ X and a ⊆ X , then ↓ a := { x ∈ X | x ≤ y for some y ∈ a } and R x [ ] := { y ∈ X | xRy } .

Proposition 4.7 ( ) . A frame X = ( X, /bomb , ≤ , R ) validates C 3 if and only if it satisfies:

$$( C _ { \diamond } \text{-cor} ) & \ \forall x, y, z \ ( \text{if } y, z \notin R ^ { - 1 } ( \Theta ^ { \prime } ) \text{ and } x \leq y \text{ and } x \leq z \\ & \quad \text{then } \exists w ( x \leq w \text{ and } R [ w ] \subseteq \downarrow R [ y ] \text{ and } R [ w ] \subseteq \downarrow R [ z ] ) )$$

̸

̸

̸

Proof. Suppose X satisfies ( C 3 -corr). Let x be a world, V any valuation and suppose x ⊩ 3 p ∨ 3 q . Then x ⊩ 3 p and x ⊩ 3 q , so there exist y ≥ x and z ≥ x such that R y [ ] ∩ V ( p ) = ∅ and R z [ ] ∩ V ( q ) = ∅ . We must have y, z / R ∈ -1 ( /bomb ), so by ( C 3 -corr) we can find some w ≥ x such that every R -successor of w lies below an R -successor of y and below an R -successor of z . This implies that R w [ ] ∩ ( V ( p ) ∪ V ( q )) = ∅ , so that w witnesses x ⊩ 3 ( p ∨ q ). Since this holds for every x ∈ X and every valuation, it follows that X ⊩ ( p ∨ q ) → p ∨ q .

̸

Proposition 4.8 ( ) . A frame X = ( X, /bomb , ≤ , R ) validates I 32 if and only if it satisfies:

3 3 3 For the converse, suppose that ( C 3 -corr) does not hold. Then we can find x, y, z satisfying y, z / R ∈ -1 ( /bomb ) and x ≤ y and x ≤ z , and such that there is no w ≥ x such that every R -successor of w lies below R -successors of y and z . Taking V ( p ) = ( X \ ↓ R y [ ]) ∪ { /bomb } and V ( q ) = ( X \ ↓ R z [ ]) ∪ { /bomb } then results in a model where x satisfies 3 ( p ∨ q ) but not 3 p or 3 q , whence x ⊩ 3 ( p ∨ q ) → 3 p ∨ 3 q .

̸

$$( \mathfrak { l } _ { \odot \square } \text{-corr} ) \ \forall x, y, z ( \text{if } x R y \leq z \neq \mathbb { m } ^ { \prime } & \text{ then } \exists u, w \ ( x \leq u R w \leq z \\ & \text{ and } \forall s \ ( \text{if } u \leq s \ \text{then } s R \mathbb { m } ^ { \prime } & \text{or } \exists t ( s R t \ \text{and } z \leq t ) ) ) )$$

̸

̸

Proof. Suppose X satisfies ( I 32 -corr). Let V be any valuation and suppose x ′ ⊩ 2 ( p → q ). Then there exist worlds x , y and z such that x ′ ≤ xRy ≤ z and z ⊩ p and z ⊩ q . Indeed, then y ⊩ p → q so x ′ ⊩ 2 ( p → q ). Since z ⊩ q we must have z = /bomb , so we can find u, w with the properties mentioned in ( I 32 -corr). Then u ⊩ 3 p because each intuitionistic successor s of u can modally see /bomb or some successor of z , both of which satisfy p . But we have u ⊩ 2 q , because u ≤ Rw and w ≤ z , hence w ⊩ q . Since x ′ ≤ x ≤ u , we conclude x ′ ⊩ p → q .

̸

̸

̸

̸

̸

̸

̸

̸

̸

̸

̸

̸

3 2 For the converse, suppose that the frame validates ( 3 p → 2 q ) → 2 ( p → q ) and let x, y, z ∈ X be such that xRy ≤ z and z = /bomb . Define V ( p ) = ( ↑ z ) ∪ { /bomb } and V ( q ) = ( X \ ↓ z ) ∪ { /bomb } . Then z ⊩ p and z ⊩ q (because z = /bomb ), and therefore y ⊩ p → q , so that x ⊩ 2 ( p → q ). But this means that we must have x ⊩ 3 p → 2 q . So there exists some successor v of x such that v ⊩ 3 p while v ⊩ 2 q . The latter implies that there exists some u, w such that v ≤ uRw and w ⊩ q . By definition of V ( q ) this means w ≤ z . Furthermore, v ⊩ 3 p implies u ⊩ 3 p , so each intuitionistic successor s of u has a modal successor that satisfies p . By definition this means that either sR /bomb or there is some t such that sRt and z ≤ t . Thus we have found u, w ∈ X with the desired properties, hence the frame satisfies ( I 32 -corr).

̸

3

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-9ad8e654-573c-4cbf-96cb-8a43bd3671a1.jpg)

32

Figure 3: Correspondence conditions for validity of C 3 and I 32 . The solid arrows indicate universally quantified arrows, while the dashed ones indicate existential ones. The modal relations are labelled R and the intuitionistic relation is unlabelled.

The correspondence results for the axioms N 3 , C 3 and I 32 , give rise to sound semantics for extensions of CK with any combination of them. Next, we prove completeness using sufficient conditions.

Theorem 4.9. Let Ax ⊆ { N 3 , C 3 , I 32 } . Then the logic CK ⊕ Ax is sound and strongly complete with respect to the class of frames satisfying ( A -suff) for each A ∈ Ax , except for CK ⊕ N 3 and CK ⊕ N 3 ⊕ C 3 , for which ( N 3 -corr) replaces ( N 3 -suff).

Proof sketch. Soundness results are straightforwardly obtained as instances of a general result ( ) via the use of correspondence conditions ( , , , , , , , ).

For completeness, the proof splits into four cases, depending on whether or not C 3 and I 32 are in Ax . Each uses a slightly different canonical model construction, In each case, adding N 3 to the logic yields a notion of (prime) theory which implies that the corresponding canonical model satisfies ( N 3 -corr) or ( N 3 -suff). We sketch the constructions here.

̸

̸

̸

̸

Case 1: C 3 / ∈ Ax and I 32 / ∈ Ax . This is considered in Section 3 ( , ).

Case 3: C 3 / ∈ Ax and I 32 ∈ Ax . In this case we use what we call P-segments (for Purposeful segments) ( ). The idea is that each segment (Γ , U ) has a purpose, in the sense that it is used to falsify the truth condition for some 3 π that is not in Γ. Additionally, we consider edge cases based on whether ⊥ and 3 ⊥ are in Γ.

Case 2: C 3 ∈ Ax and I 32 / ∈ Ax . In this case we construct a canonical model as in Section 3 but we restrict our segments ( ) to those of the form (Γ , U ) where either U = { ∆ | 2 -1 (Γ) ⊆ ∆ and 3 (∆) ⊆ Γ , or } U = { ∆ | 2 -1 (Γ) ⊆ ∆ . These types of segments allow us to prove the truth lemma. The resulting model } satisfies ( C 3 -suff) ( ), and hence yields the desired strong completeness results ( , ).

- · If ⊥ ∈ Γ, then the only P-segment based on Γ is (Γ , { Γ ) (i.e. ( } /bomb , { /bomb } ));
- · If ⊥ ∈ / Γ but 3 ⊥ ∈ Γ, then the only P-segment based on Γ is (Γ , { ∆ | 2 -1 (Γ) ⊆ ∆ ); }

$$U = \{ \Delta \, | \, \Box ^ { - 1 } ( \Gamma ) \subseteq \Delta \text{ and } \pi \notin \Delta \}.$$

- · If 3 ⊥ ∈ / Γ, then a segment (Γ , U ) is a P-segment if there exists a 3 π / ∈ Γ such that

Again, our choice of segments allows us to prove the truth lemma, while being restrictive enough to let us prove satisfaction of ( I 32 -suff) ( ), giving strong completeness ( , ).

Case 4: C 3 ∈ Ax and I 32 ∈ Ax . In this final case we can use prime theories as the worlds of our canonical models ( ), rather than segments. These are partially ordered by inclusion, and we define the modal accessibility relation R by letting Γ R ∆ iff 2 -1 (Γ) ⊆ ∆ and 3 (∆) ⊆ Γ. We can view this as the restriction to segments of the form (Γ , U ) where a prime theory ∆ is in U if and only if Γ R ∆. It turns out that C 3 is crucial to prove the truth lemma, while I 32 allows us to prove that the resulting frame satisfies ( C 3 -strong) and ( I 32 -weak) ( ). Once again, we obtain strong completeness ( , ).

Completeness with respect to correspondence conditions straightforwardly follows.

Corollary 4.10. Let Ax ⊆ { N 3 , C 3 , I 32 } . Then the logic CK ⊕ Ax is sound and strongly complete with respect to the class of frames satisfying ( A -corr) for each A ∈ Ax .

Proof. Note that the cases where Ax ⊆ { N 3 } are already treated above. For the remaining ones, as sufficient conditions entail correspondence conditions ( , , ), we directly use Theorem 4.9 to obtain our result ( , , , , , ).

## 5 Comparison of diamond-free fragments

We leverage the sound and complete semantics for extensions of CK to study their diamond-free fragments. We call a logic a conservative extension of CK 2 if its 3 -free fragment coincides with CK 2 . It is known that the 3 -free fragment of CK ⊕ N 3 ⊕ C 3 is a conservative extension of CK 2 [8, Corollary 30], and that this is not the case for CK ⊕ N 3 ⊕ I 32 . In a blog comment [7] Das speculated that 'the real distinction of IK is due to [ I 32 ]', but we falsify this by proving that CK ⊕ C 3 ⊕ I 32 (hence CK ⊕ I 32 ) is conservative over CK 2 . As a consequence, we characterise precisely which extensions of CK with axioms in { N 3 , C 3 , I 32 } are conservative over CK 2 . 4

Proposition 5.1 ( ) . The logic CK ⊕ C 3 ⊕ I 32 is a conservative extension of CK 2 .

Proof. By definition every formula that is derivable in CK 2 is also derivable in CK ⊕ C 3 ⊕ I 32 , so we focus on the converse. We show that for every world in every CK -frame we can find a world in a frame for CK ⊕ C 3 ⊕ I 32 that satisfies exactly the same diamond-free formulas. This implies that the class of CK -frames validates all diamond-free consecutions in CK ⊕ C 3 ⊕ I 32 , so that the result follows from completeness of CK with respect to the class of CK -frames.

2 Let X = ( X, /bomb , ≤ , R ) be a CK -frame, and define binary relations ⪯ and R on X by:

$$x \preceq y \quad \text{iff} \ \ x \leq y \ \text{or} \ y = \tilde { \oplus } \quad \ x \mathcal { R } y \quad \text{iff} \ \ x R y \ \text{or} \ y = \tilde { \oplus }$$

Then X ′ = ( X, /bomb , ⪯ R , ) is a CK -frame ( ). The fact that every world can intuitionistically and modally access /bomb implies that X ′ satisfies ( C 3 -strong) ( ). Moreover, we have that x R ⪯ y z implies x ⪯ x R ⪯ y z and all intuitionistic successors of x can modally access /bomb , wherefore ( I 32 -corr) holds ( ).

4 Formally, we show that CK ⊕ Ax and CK coincide on their 3 -free fragments for certain Ax , relying on Das and Marin [8, Corollary 6] that this coincides with CK 2 .

Therefore X ′ is a frame for CK ⊕ C ⊕ I .

3 32 Valuations for X and X ′ coincide because we only added relations of the form x ⪯ /bomb to the intuitionistic accessibility relation. Let V be such a valuation for X . Then we can show by induction on the structure of φ that

$$( \mathfrak { X }, V ), x \ll \varphi \text{ iff } ( \mathfrak { X } ^ { \prime }, V ), x \ll \varphi$$

for all diamond-free formulas φ ( ). This entails that every diamond-free consecution Γ ⊢ φ in CK ⊕ C 3 ⊕ I 32 is true at x . Since X , V and x are arbitrary, the result follows.

We can also give a semantical proof for CK ⊕ N 3 ⊕ C 3 [8, Corollary 30]. This uses a different frame transformation: whereas the proof of Proposition 5.1 makes /bomb modally accessible to all worlds to force validity of 3 ⊥ , the frame transformation in the next proposition falsifies 3 ⊤ in all worlds. Both approaches ensure validity of C 3 by trivialising diamonds.

Proposition 5.2 ( ) . The logic CK ⊕ C 3 ⊕ N 3 is a conservative extension of CK 2 .

̸

Proof. We use the same strategy as in the proof of Proposition 5.1. Let X = ( X, /bomb , ≤ , R ) be any CK -frame. We construct a new frame X ′ by adding for each world x = /bomb an additional world x + that satisfies x ≤ x + ≤ x and that cannot modally see anything. Intuitively, this makes 3 ⊤ false at every world (except /bomb ), forcing distributivity of diamonds over joins.

̸

Let X + be a copy of X \ { /bomb } , and for each /bomb = x ∈ X denote its copy in X + by x + 5 . Define a preorder ⪯ on X ∪ X + by

$$\preceq \coloneqq \bigcup \left \{ \{ ( x, y ), ( x, y ^ { + } ), ( x ^ { + }, y ), ( x ^ { + }, y ^ { + } ) \} \ | \ x, y \in X \text{ and } x \leq y \right \}.$$

Leave R unchanged, but view it as a relation on X ∪ X + . Then X ′ = ( X ∪ X , + /bomb , ⪯ , R ) is a CK -frame ( ). The worlds x + ensure satisfaction of ( N 3 -corr) ( ). Furthermore, ( C 3 -corr) is satisfied ( ), because if x ⪯ y and x ⪯ z then x + ⪰ x is a world such that R x [ + ] ⊆ ↓ R y [ ] and R x [ + ] ⊆ ↓ R z [ ] (since R x [ + ] = ). ∅ So X ′ is a frame for CK ⊕ C ⊕ N .

3 3 Let V be any valuation for X and define a valuation V ′ for X ′ by V ′ ( p ) = V ( p ) ∪{ x + | x ∈ V ( p ) } . Then a routine induction on the structure of φ yields ( X , V ) , x ⊩ φ iff ( X ′ , V ′ ) , x ⊩ φ for every diamond-free formula φ ( ). The remainder of the proof is as in Proposition 5.1.

Summarising our results, we get:

Theorem 5.3. Let Ax ⊆ { N 3 , C 3 , I 32 } . Then CK ⊕ Ax is a conservative extension of CK 2 if and only if N 3 / ∈ Ax or I 32 / ∈ Ax .

Proof. Non-conservativity of { N 3 , I 32 } ( ) and { N 3 , C 3 , I 32 } ( ) is witnessed by the fact that they prove ¬¬ 2 ⊥ → 2 ⊥ [8], while CK does not. Conservativity of the remaining extensions ( , , ) follows from Propositions 5.1 and 5.2.

Theorem 5.3 leaves us with two logics that are not conservative over CK 2 . While clearly CK ⊕ N 3 ⊕ I 32 is included in IK , whether or not the converse inclusion holds is unknown.

Open question 5.4. Does the 3 -free fragment of CK ⊕ N 3 ⊕ I 32 coincide with that of CK ⊕ N 3 ⊕ I 32 ⊕ C 3 ? Are either or both fragments finitely axiomatisable?

## 6 Other axioms

In Sections 4 and 5 we focussed on logics between CK and IK generated by three axioms. There are of course myriad axioms to be considered, which can all be investigated semantically. As an example of this, we study two more axioms that have appeared in the literature.

5 In the formalisation, X + is taken to include a copy of /bomb . This copy is forced to be isolated in the sense that it is only intuitionistically or modally accessible from itself. Therefore it does not affect validity in the corresponding model.

## 6.1 The weak normality axiom

We first consider the weak normality axiom :

$$( N _ { \diamondsuit \square } ) \ \diamond \perp \to \square \perp$$

This axiom was used by Kojima [17] in the context of neighbourhood semantics, weakening WK by replacing N 3 with N 32 . We investigate how this axiom fits in our semantic framework, and use it to compare extensions of CK that include N 32 . This gives rise to logics whose diamond-free fragments do not coincide with the ones from Section 5.

Proposition 6.1. A frame validates N 32 whenever it satisfies ( ):

$$( N _ { \odot \square } \text{-suff} ) \ \forall x \ ( \text{if $xR\nabla^{\prime}$ and $xRy$ then $y=\nabla^{\prime}$} )$$

Moreover, a frame validates N 32 if and only if it satisfies ( ):

$$\left ( N _ { \circ \square ^ { \prime } \text{-corr} } \right ) \ \forall x \left ( \text{if } \forall y \left ( x \leq y \text{ implies } y R _ { \alpha } \right ) \text{ then } \forall y, z \left ( x \leq y R z \text{ implies } z = \alpha \right ) \right )$$

Proof. The first claim follows from the second, because ( N 32 -suff) implies ( N 32 -corr) ( ). The second claim follows from a routine verification.

What happens if we add N 32 to any of the eight logical systems discussed in Section 4? Since N 3 implies N 32 , adding it to a system containing N 3 does not change anything. Furthermore, Theorem 5.3 implies that Kojima's logic CK ⊕ N 32 , as well as its extension with C 3 , are conservative over CK 2 ( , ). This leaves us with two new logics (in terms of diamond-free fragment) between CK 2 and IK . We claim that they relate as in Figure 4.

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-8e3d7705-fcf1-4df2-a5ef-2baa646d708e.jpg)

Figure 4: Logics including N 32 . Inclusion of logics from left to right is immediate. Dashed arrows indicate non-inclusion of diamond-free fragments, and follow from Propositions 6.3 and 6.4. We note that non-inclusion of the middle question mark would imply non-inclusion of the other two.

Theorem 6.2. Let Ax ⊆ { C 3 , I 32 } . Then the logic CK ⊕ N 32 ⊕ Ax is sound and strongly complete with respect to the class of frames satisfying ( N 32 -corr), and ( A -suff) for each A ∈ Ax ( , ). Moreover, if I 32 ∈ Ax then we can replace ( N 32 -corr) by ( N 32 -suff) ( , ).

Proof. Here again soundness is straightforward ( , , , ). Completeness follows from verifying that the canonical model constructed for each of the resulting logics satisfies ( N 32 -corr) or ( N 32 -suff).

The next propositions witness the non-inclusions indicated in Figure 4.

Proposition 6.3 ( ) . The formula ¬¬ 2 p → 2 ¬¬ p is derivable in CK ⊕ N 3 ⊕ I 32 but not in CK ⊕ N 32 ⊕ C 3 ⊕ I 32 (hence not in CK ⊕ N 32 ⊕ I 32 ).

Proof. Derivability in CK ⊕ N 3 ⊕ I 32 is a known result [8, Lemma 10]. Figure 5a gives a frame that satisfies ( N 32 -suff), ( C 3 -strong) and ( I 32 -suff) where the formula is not valid (it is false at x ), hence it is not derivable in CK ⊕ N 32 ⊕ I 32 .

Proposition 6.4 ( ) . The formula

$$\neg \Box \bot \to ( \neg \neg \Box p \to \Box \neg p ). \quad \quad \quad ( 1 ) \\. \ \cdot \. \ \cdot \. \ \cdot \. \.$$

is derivable in CK ⊕ N 32 ⊕ I 32 , but not in CK .

̸

̸

Proof. To see that the formula is not derivable in CK , consider the frame from Figure 5b with valuation V ( p ) = { w, /bomb } . Then clearly x and y do not satisfy 2 ⊥ , hence x ⊩ ¬ 2 ⊥ . Furthermore, the fact that y ⊩ 2 p implies that both x and y do not satisfy ¬ 2 p , and hence x ⊩ ¬¬ 2 p . Finally, z ⊩ ¬¬ p because z ⊩ ¬ p , which implies x ⊩ ¬¬ p . Combining this entails that x falsifies the formula.

2 Next, we derive the formula in CK ⊕ N 32 ⊕ I 32 . Applying Nec and K 2 to p →¬¬ p , which is a theorem of IPL, yields 2 p → 2 ¬¬ p . This is equal to 2 p → 2 ( ¬ p →⊥ ), so K 3 yields 2 p → ( 3 ¬ p → 3 ⊥ ). Using N 32 gives 2 p → ( 3 ¬ p → 2 ⊥ ). Using propositional intuitionistic reasoning we can rewrite this to

$$\neg \neg \Box p & \to ( \neg \Box \bot \to \neg \Diamond \neg p ). \\. e \leq n _ { \dots } \dots \dots \leq 1 \dots \dots \quad \neg \vdash \dots.$$

Now currying and commutativity of ∧ allows us to derive ¬ 2 ⊥ → ¬¬ ( 2 p →¬ ¬ 3 p ). Rewriting ¬ 3 ¬ p to 3 ¬ p →⊥ and using the fact that ⊥ → 2 ⊥ yields

$$\neg \Box \bot \to ( \neg \neg \Box p \to ( \Diamond \neg p \to \Box \bot ) ). \\ \neg \bot \cdot \cdot \cdot / \quad \neg \dots \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot$$

Finally, applying I 32 we find ¬ 2 ⊥ → ¬¬ ( 2 p → 2 ¬¬ p ).

(a) Frame for Proposition 6.3.

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-1c3dcde6-ee66-41fa-b347-2c5e797d08b6.jpg)

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-bef7a0f6-aee1-45bb-92ae-399ea3db6d60.jpg)

(b) Frame for Proposition 6.8.

Figure 5: Two more frames used to falsify formulas.

We have the following analogue of Open question 5.4.

Open question 6.5. Does the 3 -free fragment of CK ⊕ N 32 ⊕ I 32 coincide with that of CK ⊕ N 32 ⊕ I 32 ⊕ C 3 ? Are the 3 -free fragments of either of these logics finitely axiomatisable?

## 6.2 The weak constant domain axiom

The logic FIK arises from IK by replacing I 32 with the weak constant domain axiom:

$$( \text{wCD} ) \ \Box ( p \vee q ) \to ( ( \Diamond p \to \Box q ) \to \Box q )$$

It was introduced by Balbiani, Gao, Gencer, and Olivetti [1] to axiomatise the intuitionistic modal logic with birelational semantics satisfying ( C 3 -strong), but not necessarily ( I 32 -weak). We briefly investigate wCD and how it relates to the axioms from Section 4 to obtain results similar to those of Figure 4. We postpone completeness results and finite axiomatisability of some of the diamond-free fragments to future work.

Proposition 6.6 ( ) . Over CK , the axiom I 32 implies wCD .

Proof. Suppose we have ( 3 p → 2 q ) → 2 ( p → q ). Then it follows that

$$\Box ( p \vee q ) \to ( ( \Diamond p \to \Box q ) \to ( \Box ( p \vee q ) \land \Box ( p \to q ) ) ). \\ \cdots \dots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots.$$

The right hand conjunction is equal to 2 (( p ∨ q ) ∧ ( p → q )), and since (( p ∨ q ) ∧ ( p → q )) → q is a theorem of intuitionistic logic it implies 2 q . Thus we find 2 ( p ∨ q ) → (( 3 p → 2 q ) → 2 q .

The previous proposition implies that adding wCD to a logic that already proves I 32 does not add any extra deductive power. So adding wCD to the logics from Section 4 yields four logics of interest: CK ⊕ wCD CK , ⊕ C 3 ⊕ wCD CK , ⊕ N 3 ⊕ wCD , and FIK . The diamond-free fragments of the first two coincide with CK 2 as a consequence of Theorem 5.3. Thus we are left with a picture similar to Figure 4.

Proposition 6.7. ¬¬ 2 p → 2 ¬¬ p is derivable in CK ⊕ N 3 ⊕ I 32 ( ) but not in FIK .

Proof. The first part of the statement is a known result [8, Lemma 10]. The second part follows from constructing a countermodel in the semantics for FIK [1].

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-d370a4b7-cec5-4f2e-8afc-8914991c0f4a.jpg)

3

3

?

Figure 6: Logics including wCD . Inclusion of logics from left to right is immediate. Dashed arrows indicate non-inclusion of diamond-free fragments, and follow from Propositions 6.7 and 6.8.

Proposition 6.8 ( ) . The formula

$$( \text{wCD} _ { \Box } ) \ \Box ( p \vee q ) \to ( ( \neg \Box \neg p \to \Box q ) \to \Box q ) \\ \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot$$

is derivable in CK ⊕ N 3 ⊕ wCD but not in CK .

Proof. The formula 3 p → ¬ 2 ¬ p is a theorem of CK ⊕ N 3 . Now using instance of the intuitionistic theorems

$$( \varphi \to \psi ) \to ( ( \chi \to \varphi ) \to ( \chi \to \psi ) ) \ \text{ and } \ ( \varphi \to \psi ) \to ( ( \psi \to \chi ) \to ( \varphi \to \chi ) )$$

we can derive wCD 2 from wCD . The fact that wCD 2 is not derivable in CK can be shown by taking the CK -frame from Figure 5b and setting V ( p ) = { z, /bomb } and V ( q ) = { w, /bomb } . The resulting model falsifies wCD 2 at x .

Open question 6.9. Does the 3 -free fragment of CK ⊕ N 3 ⊕ wCD coincide with that of CK ⊕ N 3 ⊕ wCD ⊕ C 3 ? Are the 3 -free fragments of either of these logics finitely axiomatisable?

## 7 A note on the formalisation

Beyond the extra confidence it provides in our results, for example clarifying the semantics of WK which have been disputed, our use of formalisation in the Coq Proof Assistant has been crucial for our work.

Because of the multitude of axiomatic extensions of CK we consider, we had to formalise most of our results parametrised by an arbitrary set of axioms. This generality led to formalised results which are both insightful and close to their pen-and-paper counterparts. For example, while it is often questioned in modal logic [15], we proved the deduction theorem for all axiomatic extensions of CK . Additionally, each of our strong completeness results via canonical model construction, roughly 500 lines of code, was leveraged for several logics, around 50 lines only per logic. Their size and structure make these arguments very close to their pen-and-paper counterparts.

Pragmatically, the code for a certain set of logics could be copied, pasted, and modified for another such set in a heuristic and efficient way. This enabled us to study a total of 12 logics, with an additional two-to-three days of work for each further axiom analysed. We invite our readers to experience it for themselves by downloading our code and adding their favourite axioms.

## 8 Further work

We have shown that using a relational semantics for CK , and employing Coq to verify our proofs and tame the profusion of logics arising from combinations of axioms, allows us to analyse the modal logics between CK and IK . The success of this methodology leaves us with much further work to pursue.

Open questions. While our work has closed some open questions about the logics between CK and IK , others remain. Most pressingly, do the 3 -free fragments of CK ⊕ N 3 ⊕ I 32 and IK coincide, and do they have a finite axiomatisation? We are aware of discussion, reported by Das and Marin [8], that the fragment of IK might not have a finite axiomatisation, but we are not aware of any proof of this; Grefe's thesis [14] proves only the much weaker result that there exists an infinite chain of finitely axiomatisable 3 -free logics between CK and IK .

Finite model properties. As noted in Remark 3.8, the canonical model construction for CK can be carried out relative to a set Σ of formulas. This yields a finite model, hence gives rise to the finite model property for CK , as proved already [19, Section 4]. Since the completeness results in Theorem 3.7 use various model constructions, the finite model property does not readily carry over. This raises the question how we can use these constructions to obtain finite model properties for the logics between CK and IK .

- Axiomatic extensions. Focus on the K family of logics is reasonable to answer basic questions in modal logic, but much interest concerns extensions of a basic modal logic with further axioms, from S4 to provability logic and more. How does the choice of base logic, from CK to IK , effect the properties of these logics? Adding even more axioms into the mix will, of course, make our Coq framework more crucial than ever.
- Weaker or incomparable basic logics. While most work in intuitionistic modal logic builds on at least CK , this is not universal: Gor´ e, Postniece and Tiu [13] take as basis necessitation, K 2 , N 3 , and C 3 , which is incomparable with CK because K 3 is merely an optional extension. This setup, with no assumed links between 2 and 3 , is too weak for a sensible birelational semantics, so instead takes a tri relational semantics with separate relations for the two modalities. However if we wished to remain within birelational semantics we could still consider logics where 2 and 3 interact, but not via K 3 , or logics with weaker properties of 2 , forgoing necessitation or K 2 .
- Sahlqvist theorems. Finding link between axioms and relational properties can take ingenuity. Sahlqvist theorems for classical modal logic [22, 23, 12] make this automatic for certain syntactically defined class of formulas. If these techniques could be modified to take the relational semantics for CK as their basis, they would provide another tool for taming the jungle of logics in this space.

Proof theory and types. There is a body of research too large to summarise on proof theory for intuitionistic modal logics, but our work may help to identify new logics to target and techniques to use, such as labelled sequents that take CK -semantics as their basis. In particular, we note that much recent work on proofs for intuitionistic modal logic involve calculi with type assignment, but no 3 . These type theories now support impressive applications in formalised mathematics, so it may also be worthwhile to investigate type theory with 3 from a CK base, following Bellin, de Paiva and Ritter [2], while simultaneously taking cues from more recent work on modal type theory.

## Acknowledgements

We gratefully acknowledge discussions with Dominik Kirst, Dirk Pattinson, and Alwen Tiu.

## References

- [1] Philippe Balbiani, Han Gao, Ci˘dem Gencer, and Nicola Olivetti. ¸ g A natural intuitionistic modal logic: Axiomatization and bi-nested calculus. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) , 2024. doi:10.4230/LIPIcs.CSL.2024.13 .
- [2] Gianluigi Bellin, Valeria De Paiva, and Eike Ritter. Extended Curry-Howard correspondence for a basic constructive modal logic. In Methods for Modalities 2 (M4M-2) , 2001.
- [3] Aleˇ s Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E Møgelberg, and Lars Birkedal. Guarded dependent type theory with coinductive types. In Foundations of Software Science and Computation Structures (FoSSaCS 2016) , pages 20-35, 2016. doi:10.1007/978-3-662-49630-5\_2 .
- [4] Milan Boˇ zi´ and Kosta Doˇen. Models for normal intuitionistic modal logics. c s Studia Logica , 43:217-245, 1984. doi:10.1007/BF02429840 .
- [5] Alexander Chagrov and Michael Zakharyaschev. Modal Logic . Oxford University Press, Oxford, 1997.
- [6] Tiziano Dalmonte, Charles Grellois, and Nicola Olivetti. Intuitionistic non-normal modal logics: A general framework. Journal of Philosophical Logic , 49:833-882, 2020. doi:10.1007/ s10992-019-09539-3 .
- [7] Anupam Das. Comment on blog post 'Brouwer meets Kripke: constructivising modal logic', 2022. on The Proof Theory Blog, accessed 27 June 2024. URL: https://prooftheory.blog/2022/08/19/ brouwer-meets-kripke-constructivising-modal-logic/#comment-1327 .
- [8] Anupam Das and Sonia Marin. On intuitionistic diamonds (and lack thereof). In R. Ramanayake and J. Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023) , pages 283-301, 2023. doi:10.1007/978-3-031-43513-3\_16 .

| [9]   | Valeria de Paiva. Natural deduction and context as (constructive) modality. In Modeling and Using Context (CONTEXT 2003) , pages 116-129, 2003. doi:10.1007/3-540-44958-2_10 .                                                                               |
|-------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| [10]  | Gis`le e Fischer Servi. Semantics for a class of intuitionistic modal calculi. In D. Chiara and M. Luisa, editors, Italian Studies in the Philosophy of Science , pages 59-72, Dordrecht, Netherlands, 1980. Springer. doi:10.1007/978-94-009-8937-5_5 .     |
| [11]  | Gis`le e Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rend. Sem. Mat. Univers. Politecn. Torino , 42:179-194, 1984.                                                                                                                  |
| [12]  | Damiano Fornasiere and Tommaso Moraschini. Intuitionistic Sahlqvist theory for deductive systems. The Journal of Symbolic Logic , pages 1-59, 2023. doi:10.1017/jsl.2023.7 .                                                                                 |
| [13]  | Rajeev Gor´, e Linda Postniece, and Alwen Tiu. Cut-elimination and proof search for bi-intuitionistic tense logic. In Advances in Modal logic (AiML) , volume 6, 2010.                                                                                       |
| [14]  | Carsten Grefe. Fischer Servi's intuitionistic modal logic and its extensions . PhD thesis, Freie Universit¨t a Berlin, 1999.                                                                                                                                 |
| [15]  | Raul Hakli and Sara Negri. Does the Deduction Theorem Fail for Modal Logic? Synthese , 187(3):849- 867, 2012. doi:10.1007/s11229-011-9905-9 .                                                                                                                |
| [16]  | Danko Ilik, Gyesik Lee, and Hugo Herbelin. Kripke models for classical logic. Ann. Pure Appl. Log. 161(11):1367-1378, 2010. doi:10.1016/J.APAL.2010.04.007 .                                                                                                 |
| [17]  | Kensuke Kojima. Relational and neighborhood semantics for intuitionistic modal logic. Reports on Mathematical Logic , 47:87-113, 2012.                                                                                                                       |
| [18]  | Marcus Kracht. Tools and Techniques in Modal Logic . Elsevier, 1999.                                                                                                                                                                                         |
| [19]  | Michael Mendler and Valeria De Paiva. Constructive CK for contexts. In Context Representation and Reasoning (CRR'05) , 2005.                                                                                                                                 |
| [20]  | Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic (TOCL) , 9(3):1-49, 2008.                                                                                                   |
| [21]  | Gordon Plotkin and Colin Stirling. A framework for intuitionistic modal logics: Extended abstract. In TARK '86: Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge pages 399-406, 1986.                                  |
| [22]  | Henrik Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In S. Kanger, editor, Proceedings of the Third Scandinavian Logic Symposium , volume 82, pages 110-143, 1975. doi:10.1016/S0049-237X(08)70728-6 . |
| [23]  | Giovanni Sambin and Virginia Vaccaro. A new proof of Sahlqvist's theorem on modal definability and completeness. The Journal of Symbolic Logic , 54(3):992-999, 1989. doi:10.2307/2274758 .                                                                  |
| [24]  | Michael Shulman. Brouwer's fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science , 28(6):856-941, 2018.                                                                                                     |
| [25]  | Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic . PhD thesis, University of Edinburgh, UK, 1994. URL: https://hdl.handle.net/1842/407 .                                                                                        |
| [26]  | The Coq Development Team. The Coq Proof Assistant. doi:10.5281/zenodo.1003420 .                                                                                                                                                                              |
| [27]  | Wim Veldman. An intuitionistic completeness theorem for intuitionistic predicate logic. J. Symb. Log. , 41(1):159-166, 1976. doi:10.1017/S0022481200051859 .                                                                                                 |
| [28]  | Duminda Wijesekera. Constructive modal logics I. Annals of Pure and Applied Logic , 50:271-301, 1990. doi:10.1016/0168-0072(90)90059-B .                                                                                                                     |
| [29]  | Duminda Wijesekera and Anil Nerode. Tableaux for constructive concurrent dynamic logic. Annals of Pure and Applied Logic , 135(1-3):1-72, 2005. doi:10.1016/j.apal.2004.12.001 .                                                                             |

## A Completeness results for logics between CK and IK

We provide details for the canonical model constructions used in Case 2 and Case 3 of the proof of Theorem 3.7.

## A.1 Completeness for some extensions of CK with C 3

We consider the logic CK ⊕ C 3 .

Definition A.1 ( ) . Let Γ and ∆ be prime theories.

- 1. The A-segment of Γ is the segment (Γ , A ) where ∆ ∈ A if and only if for all φ ∈ L :
- · 2 φ ∈ Γ implies φ ∈ ∆;
- 2. The B-segment of Γ is the segment (Γ , B ) where ∆ ∈ B if and only if { φ | 2 φ ∈ Γ } ⊆ ∆.
- · φ ∈ ∆ implies 3 φ ∈ Γ.

We construct a canonical model ( ) as above, except that we restrict our worlds to A-segments and B-segments. We define the intuitionistic and modal accessibility relations by ⊂ ∼ and R as above.

We note that every B-segment of a prime theory Γ contains /bomb in the tail. The A-segment of Γ only contains /bomb if 3 ⊥ ∈ Γ. The next lemma verifies that the A-segment and B-segment of a prime theory Γ are indeed segments in the sense of Definition 3.4.

Lemma A.2. Let Γ be a prime theory with A- and B-segment (Γ , A ) and (Γ , B ). Then we have:

- 1. If 2 φ ∈ Γ then φ ∈ ∆ for all ∆ ∈ A ∪ B ( ).
- 2. If 3 φ ∈ Γ then φ ∈ ∆ for some ∆ ∈ A , and φ ∈ Θ for some Θ ∈ B ( ).

Proof. The first statement holds by definition of the A- and B-segment of Γ. The second for B-segments is witnessed by Θ = /bomb ∈ B . For the second statement for A-segments, suppose 3 φ ∈ Γ. If 3 ⊥ ∈ Γ, then we here also use ∆ = /bomb ∈ A as witness. Else, we claim that

$$\Box ^ { - 1 } ( \Gamma ) \cup \{ \varphi \} \not \, \diamond ^ { - 1 } ( \Gamma ^ { c } ). & & ( 2 ) \\ \dots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots$$

2 3 3 3 2 3 3 Thus we can use the Lindenbaum lemma to find a prime theory ∆ containing 2 -1 (Γ) ∪ { φ } but avoiding 3 -1 (Γ ). c Therefore φ ∈ ∆ and ∆ ∈ A , as desired.

(We use Γ c for the complement of Γ, so 3 -1 (Γ ) = c { θ | 3 θ / ∈ Γ .) } Note that 3 -1 (Γ ) is not empty as c 3 ⊥ ̸∈ Γ by assumption. Suppose the above is not the case, then there are ψ , . . . , ψ 1 n ∈ 2 -1 (Γ) and θ , . . . , θ 1 m ∈ 3 -1 (Γ ) such that c ψ 1 ∧ · · · ∧ ψ n ∧ φ ⊢ θ 1 ∨ · · · ∨ θ m . Since boxes distribute over meets, 2 -1 (Γ) is closed under binary meets, and since 3 distribute over joins ( ) the set 3 -1 (Γ ) is closed under c binary joins. Therefore ψ := ψ 1 ∧··· ψ n ∈ 2 -1 (Γ) and θ := θ 1 ∨··· ∨ θ m ∈ 3 -1 (Γ ), and c ψ ∧ φ ⊢ θ . This implies ψ ∧ φ ⊢ θ (using K ). By assumption ψ, φ ∈ Γ, so that θ ∈ Γ, a contradiction.

Let us proceed to the truth lemma.

Lemma A.3 (Truth lemma ) . Let (Γ , U ) be an A- or B-segment. Then for all φ ∈ L we have

$$( \Gamma, U ) \models \varphi \text{ iff } \varphi \in \Gamma.$$

̸

̸

Proof. By induction on the structure of φ . The only interesting cases are for φ = 2 ψ and φ = 3 ψ . If 2 ψ ∈ Γ then Γ ⊩ 2 ψ by construction. If 2 ψ / ∈ Γ then 2 -1 (Γ) ⊢ ψ , so we can use the Lindenbaum lemma to find a prime theory ∆ containing 2 -1 (Γ) but not ψ . By definition this ∆ is in the tail of the B-segment of Γ. Extending ∆ to a segment (∆ , V ) (using either the A- or B-segment), we then find (Γ , U ) ⊂ ∼ (Γ , B ) R (∆ , V ), and by the induction hypothesis (∆ , V ) ⊩ ψ . Therefore (Γ , U ) ⊩ ψ .

̸

̸

As a final ingredient for strong completeness for CK ⊕ C 3 , we need to show that the canonical model falls within the correspondence class of the extra axiom C 3 . In fact, we show that it falls in the sufficient class of C 3 .

2 If 3 ψ ∈ Γ then (Γ , U ) ⊩ 3 ψ by the definition of segments. If 3 ψ / ∈ Γ then no ∆ in the tail of the A-segment of Γ satisfies ψ (by definition of the A-segment). Since (Γ , U ) ⊆ (Γ , A ) this implies (Γ , U ) ⊩ 3 ψ .

Lemma A.4 ( ) . The construction satisfies ( C 3 -suff).

Proof. Given (Γ , U ), we claim that the A-segment (Γ , A ) of Γ is the witness of ( C 3 -suff). Suppose (Γ , U ) ⊂ ∼ (Γ ′ , U ′ ) and ∆ ∈ A . If (Γ ′ , U ′ ) has /bomb in the tail, the we use the latter as ∆ ⊆ /bomb as desired.

So we may assume that (Γ ′ , U ′ ) does not have /bomb in the tail, and hence is an A-segment. We construct a ∆ ′ ∈ U ′ such that ∆ ⊆ ∆ . ′ First, note that { ψ | 3 ψ / ∈ Γ ′ } is not empty, else 3 ⊥ ∈ Γ ′ which would entail the presence of /bomb in the tail. Second, observe that

̸

$$\Box ^ { - 1 } ( \Gamma ^ { \prime } ) \cup \Delta \not \, \{ \psi \, | \, \diamond \psi \not \in \Gamma ^ { \prime } \}. \quad \quad \quad$$

For suppose it did, then we can find φ and δ ∈ ∆ and ψ such that φ ∧ δ ⊢ ψ . This implies

2

φ

∧

3

δ

⊢

3

ψ.

̸

By definition of A-segments, δ ∈ ∆ implies 3 δ ∈ Γ, and hence 3 δ ∈ Γ . ′ But 2 φ ∈ Γ by construction, ′ hence 3 ψ ∈ Γ , a contradiction. ′ So (3) holds, and we can use the Lindenbaum lemma to find some prime theory ∆ ′ containing ∆ and φ for each 2 φ ∈ Γ , while avoiding ′ ψ for each 3 ψ / ∈ Γ . ′ We also have 3 φ ∈ Γ ′ for each φ ∈ ∆ . To show this, assume for a contradiction that there is a ′ φ ∈ ∆ such that ′ 3 φ ∈ Γ . ′ But this is in contradiction with the fact that ∆ ′ avoids all ψ such that 3 ψ / ∈ Γ . ′ This implies ∆ ⊆ ∆ and ′ ∆ ′ ∈ U ′ .

Theorem A.5 ( ) . The logic CK ⊕ C 3 is sound and strongly complete with respect the class of frames satisfying ( C 3 -suff).

Strong completeness for the correspondence class follows straightforwardly.

Lemma A.6 ( ) . This construction satisfies ( C 3 -corr).

Proof. As ( C -suff) implies ( C -corr) (

$$& P r o o f. \, As \, ( C _ { \odot } \text{-suff} ) \, \text{implies} \, ( C _ { \odot } \text{-corr} ) \, ( \underline { p } ),$$

Theorem A.7 ( ) . The logic CK ⊕ C 3 is sound and strongly complete with respect the class of frames satisfying ( C 3 -corr).

## A.2 Completeness for extensions of CK including I 32

We now consider the axiom

$$( \diamond p \to \square q ) & \to \square ( p \to q ). \\ \text{ind before. Note that the set } \mathbf L$$

We work with (prime) theories defined before. Note that the set L of all formulas corresponds to the exploding theory, i.e. with /bomb .

Definition A.8 ( ) . A P-segment (or purposeful segment ) of Γ is defined as follows:

- · If ⊥ ∈ Γ, then the only P-segment based on Γ is (Γ , { Γ ) (i.e. ( } /bomb , { /bomb } ));
- · If ⊥ ∈ / Γ but 3 ⊥ ∈ Γ, then the only P-segment based on Γ is (Γ , U ), where

$$U = \{ \Delta \, | \, \Box ^ { - 1 } ( \Gamma ) \subseteq \Delta \} ;$$

- · If ⊥ , 3 ⊥ ∈ / Γ, then a segment (Γ , U ) is a P-segment if there exists a 3 π / ∈ Γ such that

$$U = \{ \Delta \, | \, \Box ^ { - 1 } ( \Gamma ) \subseteq \Delta \text{ and } \pi \notin \Delta \}.$$

We let X be the set of P-segments, with binary relations ⊂ ∼ and R defined as above. This is the canonical model for CK ⊕ I ( ).

32 It is clear that the two cases with 3 ⊥ ∈ Γ give rise to segments. For the case 3 ⊥ ∈ / Γ, the next lemma tells us what P-segments there are.

Lemma A.9 ( ) . Let Γ be a prime theory and 3 π / ∈ Γ. Let U π = { ∆ | 2 -1 (Γ) ⊆ ∆ and π / ∈ ∆ . Then } (Γ , U π ) is a segment.

Proof. By definition 2 φ ∈ Γ implies φ ∈ ∆. Let 3 φ ∈ Γ. Then we have 2 -1 (Γ) ∪ { φ } ̸⊢ π , for if this were not the case then Γ , 3 φ ⊢ 3 π , contradicting the fact that 3 π / ∈ Γ. So we can use the Lindenbaum lemma to construct a prime theory ∆ containing 2 -1 (Γ) and φ but not π , so that ∆ ∈ U and φ ∈ ∆ as desired.

In particular, the previous lemma shows that for each prime theory Γ there exists a P-segment headed by Γ. Indeed, if 3 ⊥ ∈ Γ then there is precisely one P-segment based on Γ, and if 3 ⊥ ∈ / Γ then the lemma above yields a P-segment headed by Γ.

Lemma A.10 (Truth lemma ) . Let (Γ , U ) be a P-segment in our canonical model. Then for all φ ∈ L we have

$$( \Gamma, U ) \models \varphi \text{ iff } \varphi \in \Gamma.$$

̸

̸

̸

Proof. By induction on the structure of φ . The only interesting cases are for φ = 2 ψ and φ = 3 ψ . If 2 ψ ∈ Γ then Γ ⊩ 2 ψ by construction. If 2 ψ / ∈ Γ then 2 -1 (Γ) ⊢ ψ . Use the Lindenbaum lemma to construct a prime theory ∆ containing 2 -1 (Γ) but not ψ . Now we consider two cases: if 3 ⊥ ∈ Γ then ∆ is in the tail of the (unique) P-segment headed by Γ by definition. So that (Γ , U ) R ∆ and ∆ ⊩ ψ and hence (Γ , U ) ⊩ ψ . If ⊥ ∈ / Γ then ∆ ∈ U ⊥ , so (Γ , U ⊥ ) is a segment above (Γ , U ) witnessing (Γ , U ) ⊩ ψ

̸

̸

̸

We show that the canonical model satisfies ( I 32 -corr).

2 3 2 If 3 ψ ∈ Γ then (Γ , U ) ⊩ 3 ψ by the definition of segments. If 3 ψ / ∈ Γ then Lemma A.9 yields a segment (Γ , V ) such that no ∆ ∈ V satisfies ψ . By induction we then find (Γ , V ) ⊩ ψ , and since (Γ , U ) ⊆ (Γ , A ) this implies (Γ , U ) ⊩ 3 ψ .

Lemma A.11 ( ) . The construction satisfies ( I 32 -corr).

̸

Proof. Suppose (Γ , U ) R (Γ ′ , U ′ ) ⊂ ∼ (Γ ′′ , U ′′ ) = ( /bomb , { /bomb } ). The inequality implies that ⊥ ∈ / Γ . ′′ We claim that

̸

For suppose it did, then using the fact that Γ and Γ ′′ are prime theories we can find φ ∈ Γ, δ ∈ Γ ′′ and ψ / ∈ Γ ′′ such that

$$\Gamma \cup \diamond \Gamma ^ { \prime \prime } \not \, \Box ( [ \Gamma ^ { \prime \prime } ] ^ { c } ). & & ( 4 ) \\ \text{the fact that } \Gamma \text{ and } \Gamma ^ { \prime \prime } \text{ are prime theories we can find } \omega \in \Gamma. \, \delta \in \Gamma ^ { \prime \prime } \text{ and }$$

$$\varphi \wedge \diamond \delta \vdash \Box \psi. \\ \vdots ( I _ { \cap \cap } ) \text{ we find } \varphi \vdash$$

This implies φ ⊢ 3 δ → 2 ψ , so by validity of ( I 32 ) we find φ ⊢ 2 ( δ → ψ ). This implies that 2 ( δ → ψ ) ∈ Γ, wherefore δ → ψ ∈ Γ , hence ′ δ → ψ ∈ Γ . By assumption ′′ δ ∈ Γ , but then deductive closure of Γ ′′ ′′ implies ψ ∈ Γ , a contradiction. ′′ Thus (4) holds.

Use the Lindenbaum lemma to generated a prime theory Θ that contains Γ and 3 (Γ ) but avoids ′′ 2 ([Γ ′′ ] c ). If 3 ⊥ ∈ Θ, then Θ is the head of a unique P-segment, which can modally see Γ ′′ by construction. Furthermore, all its successor contain 3 ⊥ and hence can modally see /bomb , which witnesses validity of ( I -corr).

32 Finally, if 3 ⊥ ∈ / Θ, then consider the P-segment (Θ , U ⊥ ). By construction we have Γ ′′ ∈ U ⊥ . Moreover, for any (Θ ′ , V ′ ) that is (intuitionistically) above (Θ , U ⊥ ), we can find some Ω ∈ V ′ such that Γ ′′ ⊆ Ω. Suppose given such a (Θ ′ , V ′ ). If ⊥ ∈ Θ or ′ 3 ⊥ ∈ Θ then we have ′ /bomb ∈ V ′ and we are done. If not, then V ′ must be of the form U π for some 3 π / ∈ Θ . By construction ′ π / ∈ Γ . Observe that ′′

̸

Suppose for a contradiction that 2 -1 (Θ ) ′ ∪ Γ ′′ ⊢ π , then we can find φ ∈ 2 -1 (Θ ) and ′ δ ∈ Γ ′′ such that φ ∧ δ ⊢ π . This implies 2 φ ∧ 3 δ ⊢ 3 π . But both 2 φ and 3 δ are in Θ , so we find ′ 3 π ∈ Θ , a ′ contradiction. Now use the Lindenbaum lemma to generate a prime theory ∆ from (5), and extend it to some segment (∆ , W ). Then by construction we have ∆ ∈ V ′ , so (Θ ′ , V ′ ) R (∆ , W ), as well as Γ ′′ ⊆ ∆. We conclude that ( I 32 -corr) is satisfied in the canonical model.

$$\Box ^ { - 1 } ( \Theta ^ { \prime } ) \cup \Gamma ^ { \prime \prime } \, \mathbb { f } \, \pi. \quad \quad \quad & ( 5 ) \\ \cdot \, - 1 / \in \alpha ^ { \prime } \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \, \cdot \, - 1 / \in \alpha ^ { \prime } \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cd.$$

Theorem A.12 ( ) . The logic CK ⊕ I 32 is sound and strongly complete with respect to the class of frames validating ( I 32 -corr).

In fact, the theory shows a slightly stronger completeness result, namely with respect to frames satisfying ( ):

![Image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00262v2-figure-9cd895c6-b292-4f04-8382-8bcb4a39f448.jpg)

The split between /bomb and t is no longer necessary because in the canonical model /bomb lies intuitionistically above any other world.

If we add 3 ⊥ → ⊥ to this logic, then every prime theory Γ with 3 ⊥ ∈ Γ satisfies ⊥ ∈ Γ, hence is the exploding world. This means that we don't have any P-segments of the shape described in the second item of Definition A.8. In the resulting canonical model, the only world that can modally see /bomb is /bomb itself, because P-segments of the form (Γ , U π ) do not have /bomb in their tail. This means that the resulting model satisfies ( N 3 -suff), so that we obtain:

Theorem A.13 ( ) . The logic CK ⊕ N 3 ⊕ I 32 is sound and strongly complete with respect to the frames satisfying ( N 3 -suff) and ( I 32 -suff).
Jim de Groot Ian Shillito Ranald Clouston
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
The intuitionistic modal logics considered between Constructive K (CK) and
Intuitionistic K (IK) differ in their treatment of the possibility (diamond)
connective. It was recently rediscovered that some logics between CK and IK
also disagree on their diamond-free fragments, with only some remaining
conservative over the standard axiomatisation of intuitionistic modal logic
with necessity (box) alone. We show that relational Kripke semantics for CK can
be extended with frame conditions for all axioms in the standard axiomatisation
of IK, as well as other axioms previously studied. This allows us to answer
open questions about the (non-)conservativity of such logics over
intuitionistic modal logic without diamond. Our results are formalised using
the Coq Proof Assistant.