Nested Sequents for Quantified Modal Logics

Abstract

This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal—i.e., each sequent has a formula interpretation—whenever the existence predicate is expressible in the language.

Tim S. Lyon was supported by the European Research Council (ERC) Consolidator Grant 771779 (DeciGUT).

1 Introduction

Generalisations of Gentzen-style sequent calculi have proven useful for developing cut-free and analytic proof systems for many propositional non-classical logics, including modal and intermediate ones. Among these generalisations are display calculi [2], hypersequents [1], labelled calculi [23, 25], and nested sequents [5, 12]. They often allow one to give constructive proofs of important meta-theoretical properties such as decidability [3], interpolation [9], and automatic countermodel extraction [16]. These systems generalise the structural level of Gentzen-style calculi in different ways in order to express wider classes of logics. In the case of propositional modal logics they can express the structure of various relational models. In particular, nested sequents encode tree-like relational models and labelled calculi encode graph-like models. In contrast to other formalisms (e.g. labelled sequents) nested sequents have the advantage of being internal calculi: each nested sequent has a formula interpretation, and thus, such expressions are not a major departure from the modal language.

Things become more difficult when we add the quantifiers. As is well known [7, 10], in quantified modal logics (QMLs) we have interaction formulas such as

$$ {\textbf {CBF}}:=\; \Box \forall xA\supset \forall x\Box A \qquad \text {and}\qquad {\textbf {BF}}:=\;\forall x\Box A\supset \Box \forall xA $$

whose validity depends on the interrelations between the domains of quantification ($\mathcal {D}_w$) of the different worlds (w) of the model: CBF is valid only if domains are increasing—$w\mathcal {R}v$ implies $\mathcal {D}_w\subseteq \mathcal {D}_v$—and BF is valid only if domains are decreasing—$w\mathcal {R}v$ implies $\mathcal {D}_w\supseteq \mathcal {D}_v$. Axiomatically, CBF is derivable from the interaction of the axioms/rules for modalities and those for the classical quantifiers, and BF is independent from them. However, the situation is radically different for sequent calculi than for axiomatic calculi. The problem is that BF becomes derivable when we add standard sequent rules for the quantifiers to a calculus having separated left and right rules for the modalities—i.e., it is derivable in all generalisations of Gentzen-style calculi mentioned above.

To overcome this issue for nested sequents, we employ a formulation technique motivated by labelled sequent calculi. One way of making CBF and BF independent of the rules for quantifiers within labelled sequent calculi is to extend the language with domain atoms of shape $y\in D(w)$ whose intended meaning is that ‘y belong to the quantificational domain of the label w’ [20, 25]. In this way, one can restrict the rules for the quantifiers to the terms belonging to the domain of the label under consideration:

As a consequence, CBF and BF are derivable only if we extend the basic calculus with rules relating the domains of the distinct labels.

In this paper, we study nested sequent calculi for QMLs with varying, increasing, decreasing, and constant domains. Similar to the use of domain atoms in labelled sequents, we will formulate our nested calculi by extending the syntax of sequents with signatures—i.e., multisets of terms that restrict the applicability of the rules for the quantifiers at that node of the nested sequent—as was done in [24] to define hypersequents for Gödel-Dummett logic with non-constant domains. In particular, we will use the following rules for the universal quantifier:

and will add signature structural rules for increasing, decreasing, and constant domains (Table 3).

As a consequence, we will be able to define nested calculi that are equivalent to the labelled calculi considered in [25, Ch. 6] and [20, Ch. 12.1]. We will show that our nested calculi have good structural properties—all rules are height-preserving invertible, weakening and contraction are height-preserving admissible, and cut is syntactically admissible—and that they characterise the quantified extensions of the propositional modal logics in the cube of normal modalities. One advantage of the present approach is that nested sequents with signatures have a formula interpretation given that the language can express the existence predicate $\mathcal {E}$. In this paper, we will consider a language with identity so that $\mathcal {E}x$ can be expressed as $\exists y(y=x)$ and it need not be taken as an additional primitive symbol; cf. [7]. Thus, our calculi utilise (nested) sequents as expressive as the modal language, showing that our calculi are syntactically economical.

The rest of the paper is organised as follows: Sect. 2 sketches the QMLs considered in the paper, and Sect. 3 introduces the nested calculi for these logics. Then, Sect. 4 shows that these calculi have good structural properties distinctive of $\textsf{G3}$-style calculi, including syntactic cut-elimination, and Sect. 5 shows that each calculus is sound and compete with respect to its intended semantics. Finally, Sect. 6 presents some future lines of research.

2 Quantified Modal Logics

-Syntax. Let Rel be a set containing, for each $n\in \mathbb {N}$, an at most countable set of n-ary predicates $R_1^n,\,R_2^n,\dots$, and let Var be a denumerable set of individual variables. The language $\mathcal {L}$ is defined by the following grammar:

where $x,x_1,\dots ,x_n\in$Var and $R_i^n\in$Rel. An atomic formula is a formula of the shape $R_i^n(x_1,\dots ,x_n)$ or $x_1=x_2$. We use the following metavariables: x, y, z for variables; P, Q, R for atomic formulas; and A, B, C for formulas. An occurrence of a variable x in a formula is free if it is not in the scope of $\forall x$; otherwise, it is bound. A sentence is a formula without free occurrences of variables. The formulas $\lnot A$, $A\wedge B$, $A\vee B$, $\exists xA$, and $\Diamond A$ are defined as expected. We follow the usual conventions for parentheses. The weight of a formula |A| is defined accordingly: $|R_i^n(x_1,\dots ,x_n)| = |x=y| = |\bot | = 0$, $|A \supset B| = |A| + |B| + 1$, and $|\forall xA| = |\Box A| = |A| + 1$. We use A(y/x) to denote the formula obtained from A by replacing each free occurrence of x with an occurrence of y, possibly renaming bound variables to avoid capture: if $y\not \equiv x$, then $(\forall y A)(y/x)\equiv \forall z((A(z/y))(y/x))$, where z is fresh.

-Semantics. A frame is a triple $\mathcal {F}=\langle \mathcal {W},\,\mathcal {R},\mathcal {D}\rangle$, where:

• $\mathcal {W}$ is a non-empty set of worlds;

• $\mathcal {R}$ is a binary accessibility relation defined over $\mathcal {W}$;

• $\mathcal {D}$ is a function mapping each $w\in \mathcal {W}$ to a possibly empty set of objects $\mathcal {D}_w$ (the domain of w); we impose that $\mathcal {D}$ is such that $\mathcal {D}_v\ne \varnothing$ for some $v\in \mathcal {W}$.

We say that $\mathcal {F}$ has:

• 1. increasing domains if for all $w,v\in \mathcal {W}$, $w\mathcal {R}v$ implies $D_w\subseteq D_v$;

• 2. decreasing domains if for all $w,v\in \mathcal {W}$, $w\mathcal {R}v$ implies $D_w\supseteq D_v$;

• 3. constant domains if for all $w,v\in \mathcal {W}$, $D_w=D_v$;

• 4. varying domains if none of the above conditions hold.

A model $\mathcal {M}$ is a frame together with a valuation function $\mathcal {V}$ such that for each $w\in W$ and each $R^n$ in Rel, $\mathcal {V}(w,R_n)\subseteq (D_\mathcal {W})^n$, where $D_\mathcal {W}=\bigcup _{v\in \mathcal {W}} D_v$. An assignment $\sigma$ is a function mapping each variable to an object in $\mathcal {D}_\mathcal {W}$. We let $\sigma ^{ x\triangleright o}$ be the assignment mapping x to $o\in \mathcal {D}_\mathcal {W}$, which behaves like $\sigma$ for all other variables. Observe that variables are rigid designators in that their value does not change from one world to another.

Table 1. Axioms and corresponding properties

The notion of satisfaction of a formula A at a world w of a model $\mathcal {M}$ under an assignment $\sigma$—to be denoted by $\sigma \Vdash _w^\mathcal {M}A$, possibly omitting $\mathcal {M}$—is defined as follows:

$\sigma \Vdash _w^\mathcal {M}R^n(x_1,\dots ,x_n)$	iff	$\langle \sigma (x_1),\dots ,\sigma (x_n)\rangle \in \mathcal {V}(w,R^n)$
$\sigma \Vdash _w^\mathcal {M}x=y$	iff	$\sigma (x)=\sigma (y)$
$\sigma \not \Vdash _w^\mathcal {M}\bot$
$\sigma \Vdash _w^\mathcal {M}A\supset B$	iff	$\sigma \not \Vdash _w^\mathcal {M}A$ or $\sigma \Vdash _w^\mathcal {M}B$
$\sigma \Vdash _w^\mathcal {M}\forall xA$	iff	for each $o\in \mathcal {D}_w$, $\sigma ^{x\triangleright o}\Vdash _w^\mathcal {M}A$
$\sigma \Vdash _w^\mathcal {M}\Box A$	iff	for each $v\in \mathcal {W}$, $w\mathcal {R}v$ implies $\sigma \Vdash _v^\mathcal {M}A$

The notions of truth at a world w ($\Vdash _w^\mathcal {M}A$), truth in a model $\mathcal {M}$ ($\Vdash ^\mathcal {M}A$), validity in a frame $\mathcal {F}$ ($\mathcal {F}\Vdash A$), and validity in class $\mathcal {C}$ of frames ($\mathcal {C}\Vdash A$) are defined as usual. It is well-known that the formula:

• CBF:= $\Box \forall xA\supset \forall x\Box A$ is valid over frames with increasing domains;

• BF:= $\forall x\Box A\supset \Box \forall xA$ is valid over frames with decreasing domains;

• UI:= $\forall xA\supset A(y/x)$ is valid over frames with constant domains.

Over frames with non-constant domains the valid theory of quantification is that of positive free logic instead of that of classical logic. This means that the axiom UI is replaced by the weaker axiom UI$^\circ := \forall y(\forall xA\supset A(y/x))$. If we extend the language with an existence predicate $\mathcal {E}$—whose satisfaction clause is $\sigma \models _w^\mathcal {M}\mathcal {E}x$ iff $\sigma (x)\in \mathcal {D}_w$—then we have the following weaker form of UI that is valid UI$^\mathcal {E}:= \forall xA\wedge \mathcal {E}y \supset A(y/x)$. Over the language $\mathcal {L}$ the formula $\mathcal {E}x$ can be defined as $\exists y(y=x)$, but over an identity-free language the existence predicate has to be taken as an additional primitive symbol. This distinction has an impact on the calculi introduced in the next section: nested sequents have a formula interpretation when $\mathcal {E}$ is expressible in the language.

-Logics. A QML is defined to be the set of all formulas that are valid in some given class of frames. In this paper, we consider logics that are defined by imposing combinations of the properties in Table 1. We use $\mathsf {Q.L}$ for a generic logic and we say that a formula is $\mathsf {Q.L}$-valid if it belong to the logic $\mathsf {Q.L}$. The formulas that are valid over the class of all frames is called $\mathsf {Q.K}$ and it is axiomatised by the axioms and rules given in Table 2. We notice that UI$^\mathcal {E}$ is a theorem of $\mathsf {Q.K}$, see [7, Lem. 2.1(iii)]. The additional axioms for the logics extending $\mathsf {Q.K}$ are given in Table 1. We follow the usual conventions for naming logics—e.g., $\mathsf {Q.S4\oplus CBF}$ is the set of formulas that are valid over all reflexive and transitive frames with increasing domains and it is axiomatised by adding axioms T, 4, and CBF to $\mathsf {Q.K}$. We will not distinguish between a logic and its axiomatisation. This is justified by the following theorem.

Theorem 1

([7]). A formula is a theorem of $\mathsf {Q.L}$ if and only if it is $\mathsf {Q.L}$-valid.

Table 2. Axiomatisation of $\mathsf {Q.K}$.

3 Nested Calculi for QML

A sequent is an expression $X;\varGamma \Rightarrow \varDelta$ where X is a multiset of variables, called a signature, and $\varGamma ,\,\varDelta$ are multisets of formulas of the language $\mathcal {L}$. The signature of a sequent is a syntactic counterpart of the existence atoms used in calculi where UI is replaced by UI$^\circ$ or UI$^\mathcal {E}$, see [19]. Nested sequents are defined as follows:

$$ \mathcal {S}\;{::}\!\!=\; X;\varGamma \Rightarrow \varDelta \;|\; \mathcal {S},\,[\mathcal {S}],\dots ,[\mathcal {S}] $$

A nested sequent $\mathcal {S}$ codifies the tree of sequents $\texttt{tr}(\mathcal {S})$, as shown in Fig. 1.

Fig. 1.

The tree of the sequent $X;\varGamma \Rightarrow \varDelta ,[\mathcal {S}_1],\dots ,[\mathcal {S}_n]$.

Substitution of free variables are extended to (nested) sequents and to multisets of formulas by applying them component-wise. The formula interpretation of a sequent is defined as follows:

$$ \texttt {fm}(X;\varGamma \Rightarrow \varDelta ) \equiv \bigwedge _{x\in X} \mathcal {E}x \wedge \bigwedge \varGamma \supset \bigvee \varDelta $$

where $\mathcal {E}x$ is short for the formula $\exists y(y=x)$ and an empty conjunction (disjunction) is $\top$ ($\bot$, resp.). To provide a formula reading of nested sequents over the identity-free language we could add $\mathcal {E}$ to the language or interpret formulas via their universal closure. In the latter case, for example, the formula interpretation of a sequent would be $\texttt {fm}(X;\varGamma \Rightarrow \varDelta )\equiv \forall x\in X(\bigwedge \varGamma \supset \bigvee \varDelta )$, and it seems our nested calculi would capture the QMLs in [13].¹ Nonetheless, we believe there are independent reasons for studying QMLs over a language containing identity; cf. [7, 10]. The formula interpretation of a nested sequent is defined recursively as:

$$ \texttt {fm}(X;\varGamma \Rightarrow \varDelta ,[\mathcal {S}_1],\dots ,[\mathcal {S}_n])\equiv (\bigwedge _{x\in X}\mathcal {E}x\wedge \bigwedge \varGamma \supset \bigvee \varDelta ) \vee \bigvee _{k=1}^{n}\Box \,\texttt {fm}(\mathcal {S}_k) $$

Rules are based on the notion of a hole $\{\cdot \}$, which is a placeholder for a subtree of (the tree of) a nested sequent and, thus, allows one to apply a rule at an arbitrary node in the tree of a nested sequent. A context is defined as follows:

$$ \mathcal {C} {::}= X;\varGamma \Rightarrow \varDelta ,\{\cdot \},\dots ,\{\cdot \}\ \;|\; \mathcal {C} ,\,[\mathcal {C} ],\dots ,[\mathcal {C}] $$

In other words, a context $\mathcal {C}$ is a nested sequent with $n \ge 0$ hole occurrences, which do not occur inside formulas and must occur within consequent position. We hitherto write contexts as $\mathcal {S}\{\cdot \}\cdots \{\cdot \}$ indicating each of the holes occurring within the context. The depth of a hole in a context is defined as the height of the branch from that hole to the root (cf. [3]), and we write $Depth(\mathcal {S}\{\cdot \}) \ge n$ for $n \in \mathbb {N}$ to mean that the depth of the hole in $\texttt{tr}(\mathcal {S}\{\cdot \})$ is n or greater.

We define substitutions of nested sequents into contexts recursively on the number and depth of holes in a given context: suppose first that our context is of the form $\mathcal {S}\{\cdot \} \equiv X;\varGamma \Rightarrow \varDelta ,\{\cdot \},[\mathcal {S}_{1}], \ldots , [\mathcal {S}_{n}]$ with a single hole at a depth of 0 and let $\mathcal {S}' \equiv Y, \varPi \Rightarrow \varSigma , [\mathcal {S}_{1}'], \ldots , [\mathcal {S}_{k}']$ be a nested sequent. Then,

$$ \mathcal {S}\{\mathcal {S}'\} \equiv X,Y; \varPi , \varGamma \Rightarrow \varDelta , \varSigma , [\mathcal {S}_{1}], \ldots , [\mathcal {S}_{n}], [\mathcal {S}_{1}'], \ldots , [\mathcal {S}_{k}'] $$

If our context is of the form $\mathcal {S}\{\cdot \} \equiv X;\varGamma \Rightarrow \varDelta ,[\mathcal {S}_{1}\{\cdot \}], \ldots , [\mathcal {S}_{n}]$ with a single hole at a depth greater then 0, then we recursively define $\mathcal {S}\{\mathcal {S}'\}$ to be the nested sequent $X;\varGamma \Rightarrow \varDelta ,[\mathcal {S}_{1}\{\mathcal {S}'\}], \ldots , [\mathcal {S}_{n}]$. This definition extends to a context $\mathcal {S}\{\cdot \}\cdots \{\cdot \}$ with n holes in the expected way, and for nested sequents $\mathcal {S}_1, \dots , \mathcal {S}_n$, we let $\mathcal {S}\{\mathcal {S}_1\}\cdots \{\mathcal {S}_n\}$ denote the nested sequent obtained by replacing, for each $i\in \{1,\dots ,n\}$, the i-th hole $\{\cdot \}$ in $\mathcal {S}\{\cdot \}\cdots \{\cdot \}$ with $\mathcal {S}_i$. We may also write $\mathcal {S}\{\mathcal {S}_{1}\}\{\mathcal {S}_{i}\}^{n}_{i=2}$ to indicate $\mathcal {S}\{\mathcal {S}_{1}\}\cdots \{\mathcal {S}_{n}\}$ more succinctly. Plugging $\emptyset$ into a hole suggests the removal of the hole; for instance, if $\mathcal {S}\{\cdot \}\{\cdot \} \equiv x; A \Rightarrow B, \{\cdot \}, [x,y, B,C \Rightarrow D, \{\cdot \}]$, then $\mathcal {S}\{\cdot \}\{\emptyset \} \equiv x; A \Rightarrow B, \{\cdot \}, [x,y; B,C \Rightarrow D]$.

The rules of the nested calculi for QMLs are given in Table 3. The minimal calculus $\mathsf {NQ.K}$ contains initial sequents, the logical rules, and the rules for identity (rule Rig is needed—and is sound—because variables are rigid designators). If $\mathsf {Q.L}$ is an extension of $\mathsf {Q.K}$ as discussed in Sect. 2, then $\mathsf {NQ.L}$ denotes the nested calculus extending $\mathsf {NQ.K}$ with the rules for the axioms of those logics. Observe that to capture axioms D, CBF, BF, and UI we have added structural rules instead of logical ones since the former have a better behaviour.

In [3], Brünnler only considers nested calculi (for propositional modal logics) defined relative to 45-complete sets of axioms. This restriction is required to ensure that the nested calculi contain all rules required for their completeness. Similarly, in the first-order setting, we only consider nested calculi defined relative to properly closed sets of axioms, which is a generalisation of 45-completeness and takes care of the interaction of B with CBF and BF (for example), ensuring the completeness of our nested calculi.

Definition 1

(Properly Closed). Let $\textsf{L} \subseteq \{\textbf{D}, \textbf{T}, \textbf{B}, \textbf{4}, \textbf{5}, \textbf{CBF}, \textbf{BF}, \textbf{UI}\}$. We define $\textsf{L}$ to be properly closed iff if all $\mathsf {Q.L}$-frames satisfy $X\in \{\textbf{4}, \textbf{5}, \textbf{CBF}, \textbf{BF}\}$, then $X \in \textsf{L}$. We define a nested calculus $\mathsf {NQ.L}$ to be properly closed iff (1) $\textsf{L}$ is properly closed, and (2) $R_{5dom} \in \mathsf {NQ.L}$ iff $\textbf{5} \in \textsf{L}$ and $\{\textbf{CBF},\textbf{BF}\} \cap \textsf{L} \ne \emptyset$.

Remark 1

All nested calculi hitherto considered will be assumed properly closed.

Table 3. Nested rules for QML

Given a calculus $\mathsf {NQ.L}$, an $\mathsf {NQ.L}$-derivation of a nested sequent ${}\mathcal {S}$ is a tree of nested sequents, whose leaves are initial sequents, whose root is ${}\mathcal {S}$, and which grows according to the rules of $\mathsf {NQ.L}$. We consider only derivations of pure sequents, meaning no variable has both free and bound occurrences and each eigenvariable (i.e., a fresh variable participating in an $R\forall$ inference) is distinct. The height of an $\mathsf {NQ.L}$-derivation is the number of nodes of one of its longest branches. We say that $\mathcal {S}$ is $\mathsf {NQ.L}$-derivable if there is an $\mathsf {NQ.L}$-derivation of $\mathcal {S}$ or of an alphabetical variant of $\mathcal {S}$. We let $\mathsf {NQ.L}\vdash \mathcal {S}$ denote that $\mathcal {S}$ is $\mathsf {NQ.L}$-derivable. A rule is said to be (height-preserving) admissible in $\mathsf {NQ.L}$, if, whenever its premisses are $\mathsf {NQ.L}$-derivable (with height at most n), also its conclusion is $\mathsf {NQ.L}$-derivable (with height at most n). A rule is said to be (height-preserving) invertible in $\mathsf {NQ.L}$, if, whenever its conclusion is $\mathsf {NQ.L}$-derivable (with height at most n), each premiss is $\mathsf {NQ.L}$-derivable (with height at most n). For each rule displayed in Table 3, the formulas explicitly displayed in the conclusion are called principal, those explicitly displayed in the premisses are called auxiliary, and everything else constitutes the context.

4 Properties and Cut-Elimination

We now show that our nested calculi satisfy fundamental admissibility and invertibility properties. Ultimately, we will apply these properties in our proof of syntactic cut-elimination.

Lemma 1

(Generalised Initial Sequents). $\mathsf {NQ.L}\vdash \mathcal {S}\{X;A,\varGamma \Rightarrow \varDelta ,A\}$, for any arbitrary $\mathcal {L}$-formula A.

Proof

By a standard induction on the weight of A.    $\square$

Lemma 2

The sequents $\mathcal {S}\{\;\Rightarrow x=x\}$ and $\mathcal {S}\{x=y,A(x/z)\Rightarrow A(y/z)\}$ are $\mathsf {NQ.L}$-derivable.    $\square$

Proof

$\mathcal {S}\{\;\Rightarrow x=x\}$ is derivable by applying an instance of rule Ref to the initial sequent $\mathcal {S}\{\;x=x\Rightarrow x=x\}$. The case of $\mathcal {S}\{x=y,A(x/z)\Rightarrow A(y/z)\}$ is handled by induction on |A(x/z)|. We consider only the case where $A(x/z)= \Box B(x/z)$.

   $\square$

Lemma 3

The following $R\bot$ rule is height-preserving admissible in $\mathsf {NQ.L}$:

Proof

By a straightforward induction on the height of the derivation $\mathcal {D}$ of the premiss. The proof is almost trivial as any application of $R\bot$ to an initial sequent of an instance of $L\bot$ gives another initial sequent or instance of $L\bot$, respectively, and $R\bot$ permutes above every other rule of $\mathsf {NQ.L}$.    $\square$

Lemma 4

(Substitution). The following rule of substitution of free variables is height-preserving admissible in $\mathsf {NQ.L}$:

Proof

By induction on the height of the derivation $\mathcal {D}$ of the premiss. The only interesting case is when the last step of $\mathcal {D}$ is an instance of $R\forall$:

We transform the derivation of the premiss by applying the inductive hypothesis twice to ensure the freshness condition is preserved: the first time to replace $z_2$ with a fresh variable $z_3$ and then to replace x with y. We conclude by applying $R\forall$ with $z_3$ as the eigenvariable.    $\square$

Typically, admissible structural rules operate on either formulas (e.g., see the internal weakening rule IW below) or nesting structure (e.g., see the Merge rule below) in nested calculi. An interesting observation in the first-order setting is that admissible structural rules also act on the signatures occurring in nested sequents. This gives rise to forms of weakening and contraction for terms, which are reminiscent of analogous rules formulated in the context of hypersequents with signatures [24].

Lemma 5

(Signature Structural Rules). The following rules of signature weakening and signature contraction are height-preserving admissible in $\mathsf {NQ.L}$:

Proof

By a standard induction on the height of the derivation $\mathcal {D}$ of the premiss. Proving height-preserving admissibility of SC is trivial as the rule permutes above all rules of $\mathsf {NQ.L}$. Proving the height-preserving admissibility of SW is also straightforward with the only interesting case arising when $\mathcal {D}$ ends with an instance of $R\forall$ with x as the eigenvariable. However, this case is easily managed by applying the height-preserving admissible substitution (y/x) to ensure the freshness condition for $R\forall$ is satisfied, followed by the inductive hypothesis, and an application of $R\forall$.    $\square$

As in the setting of first-order intuitionistic logics with increasing and constant domains (see [14]), we find that our structural rules for domains give rise to admissible logical rules generalising the $L\forall$ rule. Such rules (presented in the proposition below) combine the functionality of the associated domain structural rules with the $L\forall$ rule. The $L\forall _{bf}$ and $L\forall _{cbf}$ rules are instances of reachability rules [16, 17], which bottom-up operate by searching for terms along edges in a nested sequent used to instantiate universal formulas.

Proposition 1

The following logical rules for ‘domain-axioms’ and for axiom D are admissible in the nested calculi including the appropriate structural rules for domains or $R_D$:

Proof

The admissibility of $L\forall _{cbf}$ from $R_{cbf}$ and SW is proven as follows:

The cases of $L\forall _{bf}$ and $L\forall _{ui}$ are similar, and the case of $L_D$ follows immediately from $R_D$.    $\square$

Lemma 6

(Weakenings). The following rules of internal and external weakening are height-preserving admissible in $\mathsf {NQ.L}$:

Proof

By induction on the height of the derivation $\mathcal {D}$ of the premiss. If $\mathcal {D}$ ends with an instance of rule $R\forall$ with y the eigenvariable, we apply the (height-preserving admissible) substitution rule to replace y with a fresh variable z occurring neither in ${\mathcal {S}}\{{X; \varGamma \Rightarrow \varDelta } \}$, nor in $\varPi ,\varSigma$ (in the IW case) or in $Y,\varPi ,\varSigma$ (in the EW case). Then, we apply the inductive hypothesis and an instance of $R\forall$ to conclude ${\mathcal {S}}\{{X; \varPi ,\varGamma \Rightarrow \varDelta ,\varSigma } \}$ in the IW case and ${\mathcal {S}}\{{X; \varGamma \Rightarrow \varDelta ,[Y; \varPi \Rightarrow \varSigma ]} \}$ in the EW case.    $\square$

Lemma 7

(Necessitation and Merge). The following rules are height-preserving admissible in $\mathsf {N.QL}$:

Proof

By a simple induction on the height of the derivation of the premiss.    $\square$

Lemma 8

(Invertibility). Each rule of $\mathsf {NQ.L}$ is height-preserving invertible.

Proof

The proof is by induction on the height of the derivation. The height-preserving invertibility of all rules but $L{\supset }$, $R{\supset }$, $R\forall$ and $R\Box$ follows from Lemmas 5 and 6, and the proof of the remaining cases is standard.    $\square$

Lemma 9

(Contraction). The following rules of left and right contraction are height-preserving admissible in $\mathsf {NQ.L}$:

Proof

By simultaneous induction on the height of the derivation of the premisses of CL and CR. We consider only the non-trivial $R \forall$ case for CR as the remaining cases are similar or simpler. Assume that the last step of $\mathcal {D}$ is:

To resolve the case, we apply the height-preserving invertibility of $R\forall$, the height-preserving admissibility of (y/z) and SC, followed by the inductive hypothesis. Finally, an application of $R\forall$ gives the desired conclusion.

   $\square$

Due to the presence of $R_4$ and $R_5$ in specific nested calculi, our cut elimination theorem (Theorem 2 below) requires us to simultaneously eliminate a second form of cut that acts on modal formulas. We refer to this rule as $\textsf{L}$-Cut and note that it is essentially Brünnler’s $\textsf{Y}$-$\textsf{cut}$ rule [3]. Since the principal and auxiliary formulas of $R_4$ and $R_5$ are of the same weight (i.e. both are $\Box A$), $\textsf{L}$-Cut is needed to permute the cut upward in these special cases as cuts cannot be reduced to formulas of a smaller weight.

Definition 2

($\textsf{L}$-Cut and $\textsf{L}$-Str). Let $\mathsf {NQ.L}$ be properly closed. We define $\textsf{L}$-Cut to be the following rule:

which is subject to the following side conditions:

• if $\textbf{4}, \textbf{5} \not \in \textsf{L}$, then $n = 0$;

• if $\textbf{4} \in \textsf{L}$ and $\textbf{5} \not \in \textsf{L}$, then $\mathcal {S}\{\cdot \}\{\cdot \}$ is of the form $\mathcal {S}\{X; \varGamma \Rightarrow \varDelta , \{\cdot \},\{\mathcal {S}_{1}\{\cdot \}^{n}\}\}$;

• if $\textbf{5} \in \textsf{L}$ and $\textbf{4} \not \in \textsf{L}$, then $Depth(\mathcal {S}\{\cdot \}\{\emptyset \}^{n}) \ge 1$;

• otherwise, if $\textbf{4}, \textbf{5} \in \textsf{L}$, then no restriction on the shape of the rule is enforced.

We define $\textsf{L}$-Str to be the following rule:

which is subject to the following side conditions:

• if $\textbf{4}, \textbf{5} \not \in \textsf{L}$, then $\mathcal {S}\{\cdot \}\{\cdot \}$ is of the form $\mathcal {S}\{X; \varGamma \Rightarrow \varDelta , \{\cdot \},\{\cdot \}\}$;

• if $\textbf{4} \in \textsf{L}$ and $\textbf{5} \not \in \textsf{L}$, then $\mathcal {S}\{\cdot \}\{\cdot \}$ is of the form $\mathcal {S}\{X; \varGamma \Rightarrow \varDelta , \{\cdot \},\{\mathcal {S}_{1}\{\cdot \}\}\}$;

• if $\textbf{5} \in \textsf{L}$ and $\textbf{4} \not \in \textsf{L}$, then $Depth(\mathcal {S}\{\cdot \}\{\emptyset \}) \ge 1$;

• otherwise, if $\textbf{4}, \textbf{5} \in \textsf{L}$, then no restriction on the shape of the rule is enforced.

Lemma 10

(Special Structural Rules). If $\mathsf {NQ.L}$ contains the rule $R_X$ for the propositional axiom X, then the corresponding structural rule from Table 4 is admissible in $\mathsf {NQ.L}$. Moreover, $\textsf{L}$-Str is admissible in $\mathsf {NQ.L}$.

Table 4. Structural rules for propositional axioms

Proof

We argue the $S_B$ case by induction on the height of the given derivation; the remaining cases are considered in the appended version of this paper [18]. We only consider the $R_{bf}$ and $R_{5dom}$ cases of the inductive step as the remaining cases are simple or similar.

As our nested calculi are assumed to be properly closed, we know that if $\mathsf {NQ.L}$ contains $R_B$ and $R_{bf}$, then it must contain $R_{cbf}$, showing that we can apply IH first and then $R_{cbf}$ as shown below.

Last, we consider an interesting $R_{5dom}$ case:

To resolve the case, we apply the inductive hypothesis, followed by the height-preserving admissible rule SW. We apply the SW rule $n-1$ times adding the variable x along the path from the root to $Y,x;\varPi _{2}\Rightarrow \varSigma _{2}$, and then the $R_{cbf}$ rule n times to delete the $n-1$ copies of x up to the root. We may apply $R_{cbf}$ as our nested calculi are properly closed, that is, $\textbf{B}, \textbf{BF} \in \textsf{L}$ only if $\textbf{CBF} \in \textsf{L}$.

   $\square$

In our cut-elimination theorem below, we provide a procedure to eliminate an additive (i.e. context-sharing) version of cut as in the work on nested sequents for propositional modal logics by Brünnler [3]. We note that we could have considered an equivalent, multiplicative (i.e. context-independent) version—like the cut rule shown eliminable in the tree-hypersequent systems of Poggiolesi [22]—however, we find the additive version of the rule to be simpler as we can forgo considerations of how to fuse nested sequents of a different form.²

Theorem 2

(Cut). $\textsf{L}$-Cut and the following rule of Cut are admissible in $\mathsf {NQ.L}$:

Proof

We consider an uppermost instance of $\textsf{L}$-Cut or Cut with $A \equiv \Box B$ and A the cut formula of each rule, respectively. We argue by simultaneous induction on the lexicographic ordering of pairs $(|A|,h_{1}+h_{2})$, where |A| is the weight of A and $h_{1}$ ($h_2$) is the height of the derivation $\mathcal {D}_1$ ($\mathcal {D}_2$) of the left (right) premiss of the instance of $\textsf{L}$-Cut or Cut under consideration.

Let us first consider the case where the weight of A is zero, i.e. A is a formula of the form $R_i^n(x_1,\dots ,x_n)$, $\bot$, or $x = y$. The first two cases are standard, so we consider the case when A is of the form $x = y$. We suppose first that $x=y$ is not principal in the left premiss of Cut. If the left premiss is an initial sequent or an instance of $L\bot$, then the conclusion will be as well, so we may assume that the left premiss was derived by means of another rule. We suppose w.l.o.g. that the left premiss was derived by means of a unary rule as the binary case for $L\supset$ is similar, meaning our Cut is of the following form:

As shown below, we can resolve the case by applying the height-preserving invertibility of R1 to the right premiss of Cut, applying Cut with the premiss of R1, and then applying R1 after (note that R1 is applicable after the Cut since $x=y$ is neither auxiliary nor principal in R1 by the shape of the rules in $\mathsf {NQ.L}$).

If we suppose now that $x = y$ is principal in the left premiss of Cut, then the left premiss must be an initial sequent of the form $\mathcal {S}\{X, x=y,\varGamma \Rightarrow \varDelta ,x=y\}$. We have cases according to whether $x=y$ is principal or not in the right premiss. If it is principal then the right premiss is either (i) an initial sequent or (ii) the conclusion of an instance of a rule in $\{Repl,\,Repl_X,\,Rig\}$. In case (i) the conclusion of Cut is an initial sequent and in case (ii) the conclusion of Cut is identical to the conclusion of its right premiss, which is cut-free derivable. Else, the Cut is of the form shown below, where two copies of $x=y$ must occur in the right premiss since the contexts must match in Cut.

Applying the height-preserving admissible rule CL to the right premiss of Cut gives the desired conclusion.

Let us suppose now that the weight of the cut formula is greater than zero. We also assume that the cut formula is principal in both premisses of Cut and consider the interesting cases when $A \equiv \forall xB$ and $A \equiv \Box B$ as all other cases are standard, see [3, Thm. 5]. If the cut formula $A \equiv \forall xB$ is principal in both premisses of Cut, then our Cut is of the following form:

We first shift the Cut upward by applying the height-preserving admissibility of IW to the left premiss of Cut, and then apply Cut with the premiss of $L\forall$ as shown below, thus reducing $h_{1}+h_{2}$.

Let us refer to the above proof as $\mathcal {D}$. We now reduce the weight of the cut formula by applying Cut as shown below, giving the desired conclusion.

We now assume that the cut formula $A \equiv \Box B$ is principal in both premisses and we may assume w.l.o.g. that the cut is an instance of $\textsf{L}$-Cut. We consider the case where the right premiss of $\textsf{L}$-Cut is an instance of $R_T$ and the left premiss of $\textsf{L}$-Cut is an instance of $R\Box$. The remaining cases are proven in a similar fashion. The trick is to use the height-preserving admissibility of the special structural rules (see Lemma 10), namely, the $S_{T}$ rule. Our $\textsf{L}$-Cut is of the following form:

Let $\mathcal {D}_{1}$ and $\mathcal {D}_{2}$ denote the derivation of the left and right premiss of $\textsf{L}$-Cut, respectively. To resolve the case, we first apply the height-preserving admissible rule IW to the conclusion of $\mathcal {D}_1$, yielding the derivation $\mathcal {D}_{3}$ shown below top. We then apply $\textsf{L}$-Cut to the conclusion of $\mathcal {D}_3$ and the premiss of $\mathcal {D}_2$ (where $h_{1}+h_{2}$ is strictly smaller), giving the second derivation shown below, which we refer to as $\mathcal {D}_{4}$. Finally, as shown in the third derivation below, we can apply Cut to B (which has a strictly smaller weight than $\Box B$), and derive the desired conclusion after applying a single application of the admissible rule $S_{T}$ to the left premiss.

   $\square$

5 Soundness and Completeness

Theorem 3

(Soundness). If $\mathsf {NQ.L}\vdash \mathcal {S}$ then $\texttt {fm}(\mathcal {S})$ is $\mathsf {Q.L}$-valid.

Proof

We first note that nested application of rules is sound: for each context $\mathcal {S}\{\cdot \}$, if $A\supset B$ is $\mathsf {Q.L}$-valid then $\texttt {fm}(\mathcal {S}\{A\}) \supset \texttt {fm}(\mathcal {S}\{B\})$ is $\mathsf {Q.L}$-valid. This can be shown by induction on the depth of the context $\mathcal {S}\{\cdot \}$; see [3, Lem. 3] for details.

The $\mathsf {Q.L}$-soundness of the rules of $\mathsf {NQ.L}$ is proved by induction on the height of the derivation. The cases of initial sequents and of propositional rules of $\mathsf {NQ.L}$ are given in [3, Thm. 1]. We present the cases of $L\forall$, $R_{cbf}$, Rig, and $R_{5dom}$, all other cases being similar. If $\texttt {fm}(X,z; A(z/x),\forall xA,\varGamma \Rightarrow \varDelta )$ is $\mathsf {Q.L}$-valid, then the $\mathsf {Q.L}$-validity of $\texttt {fm}(X,z; \forall xA,\varGamma \Rightarrow \varDelta )$ follows by the soundness of the axiom UI$^\mathcal {E}$. If $\texttt {fm}(X,x;\varGamma \Rightarrow \varDelta ,[Y,x;\varPi \Rightarrow \varSigma ])$ is $\mathsf {Q.L.CBF}$-valid, then the formula $\texttt {fm}(X,x;\varGamma \Rightarrow \varDelta ,[Y;\varPi \Rightarrow \varSigma ])$ is as well because frames for $\mathsf {Q.L.CBF}$ have increasing domains. The $\mathsf {Q.L}$-validity of $\texttt {fm}(\mathcal {S}\{X;x=y,\varGamma \Rightarrow \varDelta \}\{Y;\varPi \Rightarrow \varSigma \})$ follows from that of $\texttt {fm}(\mathcal {S}\{X;x=y,\varGamma \Rightarrow \varDelta \}\{Y;x=y,\varPi \Rightarrow \varSigma \})$ since variables are rigid designators—i.e., the validity of $\textbf{NI}:= x=y\supset \Box (x=y)$ and that of $\textbf{ND}$ allow identities to be duplicated up and down the accessibility relation, respectively. Finally, we argue that $R_{5dom}$ preserves $\mathsf {Q.L}$-validity when either $\textbf{5},\textbf{CBF}\in \textsf{L}$ or $\textbf{5},\textbf{BF}\in \textsf{L}$. We show this holds for the following one-context rules from which $R_{5dom}$ is $\mathsf {NQ.L}$-derivable (if x is in the signature of a non-root node, these rules bottom-up copy x into the signature of another non-root node):

If the premiss of one of these rules is $\mathsf {Q.L}$-valid, then so is the respective conclusion since for 5-frames with increasing or decreasing domains the points satisfying $X,x;\varGamma \Rightarrow \varDelta$ and $Y;\varPi \Rightarrow \varSigma$ are mutually accessible and have the same domain.    $\square$

Theorem 4

(Completeness). If $\texttt {fm}(\mathcal {S})$ is $\mathsf {Q.L}$-valid, then $\mathsf {NQ.L}\vdash \mathcal {S}$.

Proof

We show that $\mathsf {Q.L}\vdash \texttt {fm}(\mathcal {S})$ implies $\mathsf {NQ.L}\vdash \mathcal {S}$; the theorem follows by the completeness of $\mathsf {Q.L}$ (Theorem 1). We proceed by induction on the height of the derivation of $\texttt {fm}(\mathcal {S})$ in $\mathsf {Q.L}$. The $\mathsf {NQ.L}$-admissibility of rule MP/UG/N is a corollary of Theorem 2/Lemma 6/Lemma 7. We consider only axioms UI$^\circ$ (assuming $y\not \in A$ for simplicity), ND, and CBF. The cases of axioms REF and REPL follows from Lemma 2 and the other cases are similar.

   $\square$

6 Conclusion and Future Work

We provided a uniform nested sequent presentation of quantified modal logics characterised by combinations of fundamental properties. Due to the inclusion of equality in the language of the QMLs considered, our nested calculi permit a formula translation by means of the (definable) existence predicate. As a consequence, our systems possess both a good degree of modularity and utilise a language as expressive as that of each logic, yielding more economical systems in contrast to the labelled calculi given for the same QMLs, which employ a more expressive language [20, 25]. Beyond formula interpretability, our nested calculi satisfy fundamental properties such as the admissibility of important structural rules, invertibility of all rules, and syntactic cut-elimination.

In future work, we aim to investigate constructive proofs of interpolation properties with our nested calculi (cf. [9, 15]), to use (variations of) our nested calculi to identify decidable QML fragments, as well as extend the present approach to QMLs with non-rigid designators and, possibly, definite descriptions based on $\lambda$-abstraction (see [10]) as was done in [21] for labelled sequent calculi. Another open problem is to give nested sequents with a formula interpretation for QMLs where the existence predicate is not expressible; we conjecture that this might be achieved by using the ‘universally closed nesting’ defined by Brünner for free logics [4].

We also aim to generalise our approach by employing a wider selection of propagation rules [6, 8] and reachability rules [16, 17] in our systems. As shown in various works [11, 16], diverse classes of logics characterised by Horn properties can be supplied cut-free nested calculi by utilising logical rules that propagate or consume data along paths within nested sequents specified by formal grammars. Applying this technique, we plan to see if we can capture a much wider class of QMLs in a uniform and modular fashion, and plan to investigate admissibility and invertibility properties as well as cut-elimination in this more general setting. It would also be worthwhile to examine the relationship between our nested calculi and other calculi for QMLs; e.g., we could study the computational relationship between our nested calculi and the labelled calculi for QMLs, showing how proofs can be translated and determining complexity bounds for the relative sizes of proofs.