1 Introduction↩︎

Intuitionistic modal logics form a rich class of logics that formalise modal reasoning over an intuitionistic propositional base. They pop up in different forms and applications and are sensitive to many design choices. When considering intuitionistic modal logics with both \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\), a common feature is that \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\) are not interdefinable (this in contrast to classical modal logics). One traditionally identifies two main streams to define such logics: Intuitionistic modal logic and Constructive modal logic. Intuitionistic modal logics were early investigated by, e.g., Fischer Servi [1], [2], Plotkin and Stirling [3], and Ewald [4] and are motivated by their algebraic connection to classical bi-modal logics [1], [5]–[7] and their interpretation via the standard translation into first-order intuitionistic logic [8]. The base system in this setting is Intuitionistic \(\mathsf{K}\), here denoted \(\mathsf{IK}\), as a counterpart to classical modal logic \(\mathsf{K}\). Constructive modal logics are mostly motivated by computational applications. Constructive \(\mathsf{K}\), here denoted \(\mathsf{CK}\), and its modal extensions are motivated by their Curry-Howard interpretation in type theory and their categorical semantics [9]–[12]. A closely related constructive modal logic is Wijesekera’s system introduced to model reasoning in dynamic systems [13]. We denote its propositional part by \(\mathsf{WK}\).¹ Recently, new approaches have been proposed to define intuitionistic versions of classical \(\mathsf{K}\) [16], [17]. In this paper we concentrate on the well-studied constructive modal logics \(\mathsf{CK}\) and \(\mathsf{WK}\).

The research on these two logics is extensive and revealed some surprises in recent years. Axiomatically, the two logics form extensions of intuitionistic propositional logic \(\mathsf{IL}\) with the following modal rule and (subset) of modal axioms below. These axioms follow classically from the usual normality axiom \(\hyperlink{ax:Kb}{\text{K}_{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex}}\), but are independent in an intuitionistic setting. We define \(\mathsf{CK}= \mathsf{IL}+ \{\hyperlink{ax:Kb}{\text{K}_{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex}},\hyperlink{ax:Kd}{\text{K}_{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex}}\}\) and \(\mathsf{WK}= \mathsf{CK}+ \{\hyperlink{ax:N}{\text{N}}\}\), and note that \(\mathsf{CK}\subset \mathsf{WK}\).

For semantic characterisations of the logics one can consult [18]. Recent studies [18]–[21] surprisingly resolved a common misbelief that the \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\)-free fragments of Constructive and Intuitionistic modal logics coincide: those for \(\mathsf{CK}\) and \(\mathsf{WK}\) coincide with the \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\)-only logic \(\mathsf{iK}\), but the one for \(\mathsf{IK}\) is strictly stronger.

We are interested in the interpolation properties for \(\mathsf{CK}\) and \(\mathsf{WK}\). Interpolation properties form a central theme in logic due to their good mathematical properties and widespread applications in computer science (see [22] for a recent overview on foundations, methods and applications of interpolation). Craig interpolation states that if \(\varphi\) entails \(\psi\), there is a formula \(\theta\) in the common vocabulary of \(\varphi\) and \(\psi\) such that \(\varphi\) entails \(\theta\) and \(\theta\) entails \(\psi\). The formula \(\theta\) is called the interpolant and explains the reason why \(\varphi\) entails \(\psi\). Uniform interpolation is stronger, as the interpolant only depends on \(\varphi\) and uniformly works for any \(\psi\) in a specified vocabulary. This property makes it possible to provide an interpretation of propositional quantifiers within the propositional base [23].

Proof-theoretic methods are ideal for establishing metalogical results such as interpolation. Indeed, the Craig interpolation property has been established for \(\mathsf{WK}\) in Wijesekera’s original paper using a sequent calculus [13]. In [15], terminating sequent calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\) were designed, but the uniform interpolation question was left open. Even though other systems are designed for \(\mathsf{CK}\) and \(\mathsf{WK}\) including a sequent system, a natural deduction system [11], a nested sequent calculus [24] and a focused 2-sequent calculus [25] for \(\mathsf{CK}\), and a tableaux calculus for the richer version \(\sf{CCDL}\) of \(\mathsf{WK}\) [14], neither Craig interpolation for \(\mathsf{CK}\) nor uniform interpolation for \(\mathsf{CK}\) or \(\mathsf{WK}\) has been investigated. Most surprising, to the best of our knowledge, no other interpolation result is known for any Constructive or Intuitionistic modal logic with independent \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\) [26], also not via semantic means, except for one. We came to know via personal communication with N. Bezhanishvili that the intuitionistic modal logic \(\sf{MIPC}\) [27]–[29], which can be viewed as an \(\sf{S5}\)-extension of \(\mathsf{IK}\), does not have the Craig interpolation property.

In this paper we focus on constructive methods towards uniform interpolation. The seminal work of Pitts provides a proof-theoretic proof of uniform interpolation for \(\mathsf{IL}\) using a strongly terminating sequent calculus. It is now a fruitful technique for proving uniform interpolation among many types of modal logic: classical modal logics [30]–[32], intuitionistic modal logics [32], [33], modal substructural logics and linear logics [34], [35], and non-normal modal and conditional logics [36]. However, these studies only treat mono-modal logics (with \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\)), but do not cover intuitionistic modal logics with independent \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\).

1.0.0.1 Our contributions

We positively answer the uniform interpolation question for \(\mathsf{CK}\) and \(\mathsf{WK}\). This question is specifically posed by Dalmonte, Grellois and Olivetti in [15] in which they designed strongly terminating sequent calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\). Our work can be seen as a follow-up in which we (1) provide single-succedent variants of these calculi and provide termination and cut-elimination proofs, (2) provide a constructive proof of uniform interpolation à la Pitts for \(\mathsf{CK}\) and \(\mathsf{WK}\), and (3) contribute to The Rocq Prover rocq? library for logics between \(\mathsf{CK}\) and \(\mathsf{IK}\) [18] by formalising all our results. All results described in this paper are accompanied by a clickable symbol “" leading to their formalisation.

Our work establishes the first positive uniform interpolation result among intuitionistic modal logics with independent \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\). Since uniform interpolation is stronger than Craig interpolation, we immediately obtain the Craig interpolation property for \(\mathsf{CK}\) and \(\mathsf{WK}\) as well. The constructive approach in Rocq provides us with a uniform interpolation calculator for \(\mathsf{WK}\) and \(\mathsf{CK}\) already available for some classical and intuitionistic modal logics [32], [37].

2 Preliminaries↩︎

In this section we fix the syntax and axiomatic calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\) as presented in de Groot, Shillito and Clouston’s work [18]. For the mechanisation of most of the elements of this section, we refer to their paper.

Using a countably infinite set of propositional variables \({\sf{Prop}}=\{p,q,r, \dots\}\), we define the language \(\mathcal{L}\) via the following grammar in BNF notation (): \[\varphi ::= p\in{\sf{Prop}}\mid \bot \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \varphi \rightarrow \varphi \mid \text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\varphi \mid \text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\varphi\] We abbreviate \(\neg\varphi:=\varphi\rightarrow\bot\) and \(\top:=\neg\bot\). We use Greek lowercase letters, e.g. \(\varphi, \psi, \chi\) and \(\delta\), to denote formulas, and Greek uppercase letters, e.g. \(\Gamma, \Delta, \Phi, \Psi\), for multisets of formulas. For such a multiset \(\Gamma\) we define the two multisets \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\Gamma := \{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\varphi \mid \varphi\in\Gamma\}\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}\Gamma := \{ \varphi\mid \text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\varphi\in \Gamma \}\) and similarly for \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\Gamma\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}\Gamma\). We also write \(\Gamma\uplus\Delta\) for the disjoint union of multisets \(\Gamma\) and \(\Delta\). If \(\Gamma\) is finite, \(\bigvee\Gamma\) denotes the disjunction of all formulas in \(\Gamma\) and \(\bigwedge \Gamma\) denotes the conjunction of all formulas in \(\Gamma\), with the convention that \(\bigvee \emptyset = \bot\) and \(\bigwedge \emptyset = \top\).

To finish with the syntax, we define a notion which we use to show termination of backward proof-search in our sequent calculi.

We provide generalised Hilbert calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\), i.e. axiomatic calculi manipulating consecutions of the shape \(\Gamma\vdash\varphi\) where \(\Gamma\) is a set of formulas. The calculus \(\mathsf{CKH}\) for \(\mathsf{CK}\) extends the one for intuitionistic logic \(\mathsf{IL}\), with its axioms and rules, with the necessitation rule () and axioms \(\hyperlink{ax:Kb}{\text{K}_{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex}}\) and \(\hyperlink{ax:Kd}{\text{K}_{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex}}\). The calculus \(\mathsf{WKH}\) for \(\mathsf{WK}\) is nothing but the calculus \(\mathsf{CKH}\) augmented with the axiom \(\hyperlink{ax:N}{\text{N}}\). All the axioms and rules just mentioned are presented in Figure 1. We write \(\Gamma\vdash_{\mathsf{H}}\varphi\) if \(\Gamma\vdash\varphi\) is provable in \(\mathsf{H}\), for \(\mathsf{H}\in\{\mathsf{CKH},\mathsf{WKH}\}\).

3 Sequent calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\)↩︎

In this section we introduce the sequent calculi \(\mathsf{G4CK}\) () and \(\mathsf{G4WK}\) () for \(\mathsf{CK}\) and \(\mathsf{WK}\), respectively. Sequents in these calculi, which are presented in Figure 2, are expressions of the shape \(\Gamma\Rightarrow\Delta\) where the antecedent \(\Gamma\) and the succedent \(\Delta\) are both finite multisets of formulas. Note that \(\Gamma,\varphi\) and \(\Gamma,\Pi\) stand for \(\Gamma\uplus\{\varphi\}\) and \(\Gamma\uplus\Pi\), respectively. While antecedents are unconstrained multisets in both calculi, succedents need to have a cardinality of exactly one (i.e. \(|\Delta|=1\)) in \(\mathsf{G4CK}\), and of at most one (i.e. \(|\Delta|\leq 1\)) in \(\mathsf{G4WK}\). This technically makes \(\mathsf{G4CK}\) a single-succedent calculus, and \(\mathsf{G4WK}\) a calculus with either empty or singleton succedents.² For simplicity, we call both calculi single-succedent. Beyond their succedents, these calculi differ on their rule for diamond on the left: the rule \(\hyperlink{rule:DiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL})}\) of \(\mathsf{G4CK}\) is replaced by the rule \(\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}\) in \(\mathsf{G4WK}\). Note that \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}\Delta\) is non-empty only if \(\Delta=\{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\delta\}\). As shown below, \(\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}\) is crucial to prove \(\hyperlink{ax:N}{\text{N}}\). \[\infer[\scriptstyle\hyperlink{rule:impR}{(\text{\rightarrowR})}]{\Rightarrow\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\bot\to\bot}{ \infer[\scriptstyle\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}]{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\bot\Rightarrow\bot}{ \infer[\scriptstyle\hyperlink{rule:botL}{(\text{\botL})}]{\bot\Rightarrow}{} } }\] We write \(\vdash_{\mathsf{S}}\Gamma\Rightarrow\Delta\) when \(\Gamma\Rightarrow\Delta\) is provable in \(\mathsf{S}\), with \(\mathsf{S}\in\{\mathsf{G4CK},\mathsf{G4WK}\}\).

\(\mathsf{G4CK}\) and \(\mathsf{G4WK}\) are connected to multiple calculi in the literature. First, they extend with rules for modalities the strongly terminating calculus \(\mathsf{G4ip}\) for \(\mathsf{IL}\), which has been invented many times [38]–[40]. Second, they are extensions of Iemhoff’s single-succedent calculus for \(\mathsf{iK}\) [41] with rules for \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\). Third, our calculi are single-succedent versions of Dalmonte, Grellois and Olivetti’s multi-succedent calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\) (which they call \(\mathsf{CCDL}\)) [15]. As suggested by these last authors, the adaptation of their calculi to a single-succedent setting is straightforward. The only noteworthy element in this transformation is the use of the single rule \(\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}\) in \(\mathsf{G4WK}\) for the treatment of \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\) on the left, in contrast with their counterpart multi-succedent calculus which has two.

3.1 Termination, cut admissibility and equivalence↩︎

In this section we prove of both our calculi that they strongly terminate, eliminate cut, and are equivalent to their corresponding axiomatic system.

First, we prove that \(\mathsf{G4CK}\) and \(\mathsf{G4WK}\) strongly terminate. We say that a calculus strongly terminates if the process of naive backward proof-search, i.e. freely and iteratively applying rules backward on a sequent, necessarily comes to a halt. To show strong termination, it is sufficient to provide a well-founded ordering on sequents which decreases upwards in any application of any rule of our calculi. To define such an order we exploit the Dershowitz-Manna order on finite multisets [42]: a finite multiset \(A\) of elements of type \(T\) is smaller than another finite multiset \(B\) of \(T\)-elements if \(A\) is obtained from \(B\) by replacing \(T\)-elements from \(B\) by finitely many \(T\)-elements which are strictly smaller according to a well-founded order over \(T\).

Note that a \(\mathsf{G4WK}\) sequent \(\Gamma\Rightarrow\) with an empty succedent is compared in the order over sequents via the multiset \(\Gamma\uplus\emptyset = \Gamma\). A quick inspection of the rules of our calculi shows that any premise of a rule is smaller in \(\prec\) than its conclusion.

This directly establishes the decidability of provability in \(\mathsf{G4CK}\) and \(\mathsf{G4WK}\).

In Theorem 2, at the end of this section, we prove that our calculi capture \(\mathsf{CK}\) and \(\mathsf{WK}\), respectively. In this light, the proposition above constitutes a constructive and mechanised proof of decidability for these logics. Such proofs for the two logics were already given by Dalmonte et al. [15], constructively but not mechanised, and for \(\mathsf{CK}\) in particular by Mendler and de Paiva [43], though neither constructive nor mechanised.

Second, we aim at proving cut elimination for both calculi, building on proofs of cut admissibility via local proof transformations. To get there, we need to follow a path, first established by Dyckhoff and Negri [44], paved by a succession of technical lemmas, and leading to the admissibility of contraction. We omit the majority of these intermediate lemmas, referring to our mechanisation and Dyckhoff and Negri’s work [44], except for the admissibility of some useful rules.

Next, we state the admissibility of contraction.

We leverage contraction to prove the admissibility of the cut rule. Our proof goes by primary induction on the weight of the cut formula and secondary (well-founded) induction on \(\prec\), a standard method for terminating calculi [45]–[48].

As this theorem is proved syntactically via local proof transformations, it entails that both calculi eliminate cut: any proof in the calculus augmented with the cut rule can be transformed into a proof without instances of cut.

Third, and finally, we show that \(\mathsf{G4CK}\) and \(\mathsf{G4WK}\) capture exactly the logics \(\mathsf{CK}\) and \(\mathsf{WK}\). For this, we exploit both the decidability of the sequent calculi and the admissibility of cut.

4 Uniform interpolation↩︎

We start this section by introducing general definitions and facts about uniform interpolation.

The notation of \(\exists p \varphi\) and \(\forall p \varphi\) is suggestive: the formulas do not really contain quantifiers, but they are defined over the modal language \(\mathcal{L}\). This notation is justified by Pitts’ result stating that uniform interpolants provide an interpretation for propositional quantifiers of second order intuitionistic logic into the propositional language [23].

We provide a proof-theoretic construction to prove the uniform interpolation property. In light of Remark [remark:dual] we use a sequent-style definition of uniform interpolation in which pre- and post-uniform interpolants are constructed simultaneously.

Note that in the above definition, we have \(|\Delta| = 1\) for \(\mathsf{G4CK}\) and \(|\Delta| \leq 1\) for \(\mathsf{G4WK}\). In the latter case, Definition 4 is equivalent to the uniform interpolant properties from [33]. We have the following well-known fact.

4.1 Uniform interpolation for \(\mathsf{CK}\)↩︎

To prove the uniform interpolation property for \(\mathsf{CK}\), we use the sequent calculus \(\mathsf{G4CK}\) to construct \(\mathsf{E}_{p}(\Gamma)\) and \(\mathsf{A}_{p}(s)\) for any multiset \(\Gamma\) and any sequent \(s\). Our construction adapts the one for \(\mathsf{iK}\) [33] by adding extra cases for the \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\).

Let us explain the construction of Figure 3. Rows \((\mathsf{E}_p^{\mathsf{CK}}0),(\mathsf{E}_p^{\mathsf{CK}}1'),(\mathsf{E}_p^{\mathsf{CK}}4')\) and \((\mathsf{A}_p^{\mathsf{CK}}1'),(\mathsf{A}_p^{\mathsf{CK}}4'),(\mathsf{A}_p^{\mathsf{CK}}9)\) take care of boolean constants and variables other than \(p\), which can be smartly taken out of the recursive call since these are atomic \(p\)-free formulas. Rows \((\mathsf{E}_p^{\mathsf{CK}}1''),(\mathsf{E}_p^{\mathsf{CK}}4'')\) and rows \((\mathsf{A}_p^{\mathsf{CK}}1''),(\mathsf{A}_p^{\mathsf{CK}}4'')\) are not necessary for the construction, as \(\bot\) is a neutral element for \(\mathsf{E}_{p}(\cdot)\) and \(\top\) is a neutral element for \(\mathsf{A}_{p}(\cdot)\), but are required in Rocq to ensure the functionality of \(\mathsf{E}_{p}(\cdot)\) and \(\mathsf{A}_{p}(\cdot)\) by making them defined on all inputs.

Rows \((\mathsf{E}_p^{\mathsf{CK}}2),(\mathsf{E}_p^{\mathsf{CK}}3),(\mathsf{E}_p^{\mathsf{CK}}5')\text{-}(\mathsf{E}_p^{\mathsf{CK}}8'),(\mathsf{E}_p^{\mathsf{CK}}10),(\mathsf{E}_p^{\mathsf{CK}}12)\) and \((\mathsf{A}_p^{\mathsf{CK}}2)\), \((\mathsf{A}_p^{\mathsf{CK}}3)\), \((\mathsf{A}_p^{\mathsf{CK}}5')\text{-}(\mathsf{A}_p^{\mathsf{CK}}8')\), \((\mathsf{A}_p^{\mathsf{CK}}11)\text{-}(\mathsf{A}_p^{\mathsf{CK}}17)\) correspond to what we call a full application of a calculus rule where the middle column presents the conclusion of the rule and the right column uses the premise of that rule in the recursive call.

Rows \((\mathsf{E}_p^{\mathsf{CK}}9),(\mathsf{E}_p^{\mathsf{CK}}11),(\mathsf{E}_p^{\mathsf{CK}}13),(\mathsf{A}_p^{\mathsf{CK}}18)\) and \((\mathsf{A}_p^{\mathsf{CK}}19)\) correspond to what we call partial applications of a rule from the calculus. When considering the uniformity property of uniform interpolation in Definition 4, a rule application might be possible due to extra formulas in the \(p\)-free context \(\Pi\) outside the reach of the interpolant construction meaning that these rows in the table partially match the form of rule from the calculus. For example, row \((\mathsf{E}_p^{\mathsf{CK}}11)\) is used in case there is a formula \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\delta'_1 \to \delta_2'\) in the hidden \(p\)-free context that would together with \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\delta \in \Gamma\) make an application of the rule \(\hyperlink{rule:impdiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\!\rightarrowL})}\) possible. Row \((\mathsf{E}_p^{\mathsf{CK}}9)\) is used for partial applications of \(\hyperlink{rule:BoxR}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2exR})}\) and \(\hyperlink{rule:DiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL})}\).

We will use the following simple facts.

We now present the main theorem of this section. Due to space restrictions we highlight some of the important steps of the proof below.

:::: center
::: prooftree
\[$\scriptstyle\hyperlink{rule:DiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL})}$\]\_0,'\_1,\_p(\^-1)'\_0
\[Lemma [4](#Lemma95simple2){reference-type="ref"
reference="Lemma95simple2"}\]\_0,'\_1,\_p() \_0'
:::
::::

:::: center
::: prooftree
\[$\scriptstyle\hyperlink{rule:impR}{(\text{\rightarrowR})}$\]\^-1\_0,'\_1
\_p(\^-1)\_p(\^-1)
\[$\scriptstyle\hyperlink{rule:DiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL})}$\]\_0,'\_1
\[\_p(\^-1)\_p(\^-1)\]
\[$\scriptstyle\hyperlink{rule:wk}{(\text{wk})}$\]\_0,'\_1,\_p()
\[\_p(\^-1)\_p(\^-1)\] \[$(\mathsf{A}_p^{\mathsf{CK}}18)$,
Lemma [3](#Lemma95simple1){reference-type="ref"
reference="Lemma95simple1"}\]\_0,'\_1,\_p() \_p()
:::
::::

4.2 Uniform interpolation for \(\mathsf{WK}\)↩︎

The construction of uniform interpolants for \(\mathsf{WK}\) only requires two modifications compared to the construction of uniform interpolants for \(\mathsf{CK}\) in Figure 3, because the two calculi \(\mathsf{G4CK}\) and \(\mathsf{G4WK}\) only differ in two aspects. First, since sequents \(\Gamma \Rightarrow\Delta\) in \(\mathsf{G4WK}\) obey \(|\Delta|\leq 1\) instead of \(|\Delta|=1\), we should read any row in Figure 3 that matches a sequent \(s\) with \(\varphi\) in the succedent, as having \(\Delta\) in the succedent with \(|\Delta|\leq 1\). So we replace all occurrences of \(\varphi\) (without a subscript) in Figure 3 with \(\Delta\). To be precise, this applies to rows \((\mathsf{A}_p^{\mathsf{CK}}1')\text{-}(\mathsf{A}_p^{\mathsf{CK}}8'), (\mathsf{A}_p^{\mathsf{CK}}15), (\mathsf{A}_p^{\mathsf{CK}}17)\), and \((\mathsf{A}_p^{\mathsf{CK}}19)\).

Second, the main difference between the calculi \(\mathsf{G4CK}\) and \(\mathsf{G4WK}\) lies in the left rule for \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\) which in \(\mathsf{G4WK}\) has the form: \[\infer[\scriptstyle\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}]{\Gamma,\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\varphi\Rightarrow\Delta}{ \text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}\Gamma,\varphi\Rightarrow\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}\Delta}\] That is why we modify row \((\mathsf{A}_p^{\mathsf{CK}}16)\) from Figure 3 to the following row ():

Now, \(\mathsf{E}_{p}(\Gamma)\) and \(\mathsf{A}_{p}(s)\) with respect to \(\mathsf{G4WK}\) are defined as in Definition 5 with the modified table as described above. The analogues of Theorem 3 and Lemmas 3 and 4 hold for \(\mathsf{G4WK}\) by the same proofs.

:::: center
::: prooftree
\[$\scriptstyle\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}$\]\_0,',\_p(\^-1)'
\[Lemma [4](#Lemma95simple2){reference-type="ref"
reference="Lemma95simple2"}\]\_0,',\_p() '
:::
::::

:::: center
::: prooftree
\[$\scriptstyle\hyperlink{rule:DiamLW}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL'})}$\]\_0,',\_p(\^-1)\_p()
\[Lemma [4](#Lemma95simple2){reference-type="ref"
reference="Lemma95simple2"}\]\_0,',\_p() \_p()
:::
::::

If
$\Delta = \{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi\}$,
then the same derivation applies as case (b) for
$\hyperlink{rule:DiamL}{(\text{\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2exL})}$
in the proof of Theorem [4](#thm:UIP95CK){reference-type="ref"
reference="thm:UIP95CK"}.

5 Conclusion↩︎

We have established the uniform interpolation property for constructive modal logics \(\mathsf{CK}\) and \(\mathsf{WK}\), the first positive result of this kind among intuitionistic modal logics with independent \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\). Our proof is constructive where we extend Pitts’ proof technique to constructive \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\) by exploiting terminating sequent calculi for \(\mathsf{CK}\) and \(\mathsf{WK}\). Our results have been formalised in Rocq which could contribute to the uniform interpolation calculator available in [32], [37].

Our construction aims at showing that uniform interpolants can be constructed. Our approach is based on Pitts’ naive construction, which can be simplified and optimised, as shown for the case of \(\mathsf{IL}\) in [50]. Such simplifications, optimisations and hence more efficient algorithms, would be welcome in modal logics. A recent overview on complexity bounds on (uniform) interpolants in classical modal logics is provided in [51].

Another interesting direction for future research is to study the definability of so-called bisimulation quantifiers. These are interpreted over relational semantics and closely linked to uniform interpolants [52], [53]. It would be interesting to see whether these are also definable in the birelational models of intuitionistic modal logics. Birelational semantics have been developed for \(\mathsf{CK}\) [43] and \(\mathsf{WK}\) [13] and a general study of such semantics is provided and formalised in Rocq in [18].

Finally, Pitts’ technique received attention in the recent field of universal proof theory in which the uniform interpolation is linked to nicely behaved proof systems by inspecting the form of inference rules. So-called negative results have been established in the realm of intermediate logics stating that many of such logics cannot have a semi-analytic sequent calculus [33]. Modal logics are also treated in this context [35], [54], [55], but the negative results are in our opinion quite restrictive in the modal setting because only a few \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\)-only rules are treated and a general format of ‘modal rule’ is not provided. We hope to provide a first step to widen the scope of universal proof theory by studying both \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.1ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\) and \(\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.1ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\).

References↩︎