Labelled Calculi for Lattice-Based Modal Logics

Abstract

We introduce labelled sequent calculi for the basic normal non-distri-butive modal logic $\textbf{L}$ and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of the algebras in the variety corresponding to the logic $\textbf{L}$. Modular proofs are presented that these calculi are all sound, complete and conservative w.r.t. $\textbf{L}$, and enjoy cut elimination and the subformula property. The introduction of these calculi showcases a general methodology for introducing labelled calculi for the class of LE-logics and their analytic axiomatic extensions in a principled and uniform way.

1 Introduction

The present paper pertains to a line of research in structural proof theory aimed at generating analytic calculi for wide classes of nonclassical logics in a principled and uniform way. Since the 1990s, semantic information about given logical frameworks has proven key to generate calculi with excellent properties [19]. The contribution of semantic information has been particularly perspicuous in the introduction of labelled calculi for e.g. classical normal modal logic [16] and intuitionistic logic [17], and their axiomatic extensions defined by axioms for which first-order correspondents exist of a certain syntactic shape [10]. Moreover, recently, the underlying link between the principled and algorithmic generation of analytic rules for capturing axiomatic extensions of given logics and the systematic access to, and use of, semantic information for this purpose has been established also in the context of other proof-theoretic formats, such as proper display calculi [1, 15], and relative to classes of logics as wide as the normal (D)LE-logics, i.e. those logics canonically associated with varieties of normal (distributive) lattice expansions [7] (cf. Definition 1.1). In particular, in [15], the same algorithm ALBA which computes the first-order correspondents of (analytic) inductive axioms in any (D)LE-signature was used to generate the analytic rules in a suitable proper display calculus corresponding to those axioms.

The algorithm ALBA [6, 7] is among the main tools in unified correspondence theory [5], and allows not only for the mechanization of well known correspondence arguments from modal logic, but also for the uniform generalization of these arguments to (D)LE-logics, thanks to the fact that the ALBA-computations are motivated by and interpreted in an algebraic environment in which the classic model-theoretic correspondence arguments can be rephrased in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. These properties guarantee the soundness of the rewriting rules applied in ALBA-computations, thanks to which, the first-order correspondent of a given input axiom (in any given LE-language $\mathcal {L}$) is generated in a language $\mathcal {L}^+$ expanding $\mathcal {L}$, which is interpreted in the canonical extensions of $\mathcal {L}$-algebras.

In the present paper, we showcase how the methodology adopted in [15] for introducing proper display calculi for (D)LE-logics and their analytic axiomatic extensions can be used also for endowing LE-logics with labelled calculi. Specifically, we focus on a particularly simple LE-logic, namely the basic normal non-distributive (i.e. lattice-based) modal logic $\textbf{L}$ [3, 4], for which we introduce a labelled calculus and show its basic properties, namely soundness, completeness, cut-elimination and subformula property. Moreover, we discuss, by way of examples, how ALBA can be used to generate analytic rules corresponding to (analytic inductive) axiomatic extensions of the basic logic $\textbf{L}$.

Structure of the Paper. Section 2 recalls preliminaries on basic normal non-distributive logic, canonical extensions and the algorithm ALBA, Sect. 3 presents a labelled calculus for normal non-distributive logic and its extensions. Section 4 proves soundness, completeness, cut elimination and subformula property for basic normal non-distributive logic and some of its axiomatic extensions. Section 5 shows that the all calculi introduced in the paper are proper labelled calculi. We conclude in Sect. 6. In Appendix A we provide the formal definition of proper labelled calculi and we show that any calculus in this class enjoys the canonical cut elimination à la Belnap.

2 Preliminaries

2.1 Basic Normal Non-distributive Modal Logic, Its Associated ALBA-language, and Some of Its Axiomatic Extensions

The basic normal non-distributive modal logic is a normal LE-logic (cf. [7, 8]) which was used in [3, 4] as the underlying environment for an epistemic logic of categories and formal concepts, and in [2] as the underlying environment of a logical theory unifying Formal Concept Analysis [13] and Rough Set Theory [18].

Let $\textsf{Prop}$ be a (countable or finite) set of atomic propositions. The language $\mathcal {L}$ is defined as follows:

$$ \varphi {:}{=}\bot \mid \top \mid p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \Box \varphi \mid \Diamond \varphi , $$

where $p\in \textsf{Prop}$. The extended language $\mathcal {L}^+$, used in ALBA-computations taking inequalities of $\mathcal {L}$-terms in input, is defined as follows:

where $\varphi \in \mathcal {L}$, and the variables $\textbf{j}\in \textsf{NOM}$ (resp. $\textbf{m}\in \textsf{CNOM}$), referred to as nominals (resp. co-nominals), range over disjoint sets which are also disjoint from $\textsf{Prop}$. The basic, or minimal normal $\mathcal {L}$-logic is a set $\textbf{L}$ of sequents $\varphi \vdash \psi$, with $\varphi ,\psi \in \mathcal {L}$, containing the following axioms:

$$\begin{aligned} \begin{array}{ccccccccccccc} p \vdash p &{} \quad \quad &{} \bot \vdash p &{} \quad \quad &{} p \vdash p \vee q &{} \quad \quad &{} p \wedge q \vdash p &{} \quad \quad &{} \top \vdash \Box \top &{} \quad \quad &{} \Box p \wedge \Box q \vdash \Box (p \wedge q) \\ &{} \quad &{} p \vdash \top &{} \quad &{} q \vdash p \vee q &{} \quad &{} p \wedge q \vdash q &{}\quad &{} \Diamond \bot \vdash \bot &{} \quad &{} \Diamond (p \vee q) \vdash \Diamond p \vee \Diamond q \end{array} \end{aligned}$$

and closed under the following inference rules:

$$\begin{aligned} \frac{\varphi \vdash \chi \quad \chi \vdash \psi }{\varphi \vdash \psi } \quad \frac{\varphi \vdash \psi }{\varphi \left( \chi /p\right) \vdash \psi \left( \chi /p\right) } \quad \frac{\chi \vdash \varphi \quad \chi \vdash \psi }{\chi \vdash \varphi \wedge \psi } \quad \frac{\varphi \vdash \chi \quad \psi \vdash \chi }{\varphi \vee \psi \vdash \chi } \quad \frac{\varphi \vdash \psi }{\Box \varphi \vdash \Box \psi } \quad \frac{\varphi \vdash \psi }{\Diamond \varphi \vdash \Diamond \psi } \end{aligned}$$

An $\mathcal {L}$-logic is any extension of $\textbf{L}$ with $\mathcal {L}$-axioms $\varphi \vdash \psi$. In what follows, for any set $\varSigma$ of $\mathcal {L}$-axioms, we let $\textbf{L}.\varSigma$ denote the axiomatic extension of $\textbf{L}$ generated by $\varSigma$. Throughout the paper, we will consider all subsets $\varSigma$ of the set of axioms listed in the table below. These axioms are well known from classical modal logic, and have also cropped up in [2] in the context of the definition of relational structures simultaneously generalizing Formal Concept Analysis and Rough Set Theory.

2.2 $\mathcal {L}$-algebras, Their Canonical Extensions, and the Algebraic Interpretation of the Extended Language of ALBA

In the present section, we recall the definitions of the normal lattice expansions canonically associated with the basic logic $\textbf{L}$, their canonical extensions, the existence of which can be shown both constructively and non-constructively, and the interpretation of the extended language $\mathcal {L}^+$ in the canonical extensions of $\mathcal {L}$-algebras.

An $\mathcal {L}$-algebra is a tuple $\mathbb {A} = (L,\Diamond ^\mathbb {A},\Box ^\mathbb {A})$, where L is a bounded lattice, $\Diamond ^\mathbb {A}$ (resp. $\Box ^\mathbb {A}$) is a finitely join-preserving (resp. finitely meet-preserving) unary operation. That is, besides the usual identities defining general lattices, the following identities hold:

$$\begin{aligned} \Diamond (x\vee y) = \Diamond x\vee \Diamond y\quad \quad \Diamond \bot = \bot \quad \quad \Box (x\wedge y) = \Box x\wedge \Box y\quad \quad \Box \top = \top . \end{aligned}$$

In what follows, we let $\textsf{Alg}(\mathcal {L})$ denote the class of $\mathcal {L}$-algebras. Let L be a (bounded) sublattice of a complete lattice $L'$.

• 1. L is dense in $L'$ if every element of $L'$ can be expressed both as a join of meets and as a meet of joins of elements from L. We let $K(L')$ (resp. $O(L')$) denote the meet-closure (resp. join-closure) of L in $L'$. That is, $K(L') = \{k\in L'\mid k = \bigwedge S$ for some $S\subseteq L\}$, and $O(L') = \{o\in L'\mid o = \bigvee T$ for some $T\subseteq L\}$.

• 2. L is compact in $L'$ if, for all $S, T \subseteq L$, if $\bigwedge S\le \bigvee T$ then $\bigwedge S'\le \bigvee T'$ for some finite $S'\subseteq S$ and $T'\subseteq T$.

• 3. The canonical extension of a lattice L is a complete lattice $L^\delta$ containing L as a dense and compact sublattice. Elements in $K(L^\delta )$ (resp. $O(L^\delta )$) are the closed (resp. open) elements of $L^\delta$.

As is well known (cf. [14]), the canonical extension of a lattice L exists and is unique up to an isomorphism fixing L. The non-constructive proof of existence can be achieved via suitable dualities for lattices, while the constructive proof uses the MacNeille completion construction on a certain poset obtained from the families of proper lattice filters and ideals of the original lattice L (cf. [11, 14] for details). In the latter case, the ensuing complete lattice $L^\delta$ can be shown to be perfect, i.e., to be both completely join-generated by the set $J^\infty (L^\delta )\subseteq K(L^\delta )$ of the completely join-irreducible elements of $L^\delta$, and completely meet-generated by the set $M^\infty (L^\delta )\subseteq O(L^\delta )$ of the completely meet-irreducible elements of $L^\delta$.¹

For every unary, order-preserving operation $f : L\rightarrow L$, the $\sigma$-extension of f is defined first on any $k\in K(L^\delta )$ and then on every $u\in L^\delta$ as follows:

$$f^\sigma (k):= \bigwedge \{ f(a)\mid a\in L \text{ and } k\le a\} \quad \quad f^\sigma (u):= \bigvee \{ f^\sigma (k)\mid k\in K(L^\delta ) \text{ and } k\le u\}.$$

The $\pi$-extension of f is defined first on every $o\in O(L^\delta )$, and then on every $u\in L^\delta$ as follows:

$$f^\pi (o):= \bigvee \{ f(a)\mid a\in L \text{ and } a\le o\}\quad \quad f^\pi (u):= \bigwedge \{ f^\pi (o)\mid o\in O(L^\delta ) \text{ and } u\le o\}.$$

Defined as above, the $\sigma$- and $\pi$-extensions maps are monotone, and coincide with f on the elements of $\mathbb {A}$. Moreover, the $\sigma$-extension (resp. (resp. $\pi$-extension) of a finitely join-preserving (resp. finitely meet-preserving) map is completely join-preserving (resp. completely meet-preserving). This justifies defining the canonical extension of an $\mathcal {L}$-algebra $\mathbb {A} = (L, \Box , \Diamond )$ as the $\mathcal {L}$-algebra $\mathbb {A}^\delta : = (L^\delta , \Box ^{\pi }, \Diamond ^{\sigma })$. By construction, $\mathbb {A}$ is a subalgebra of $\mathbb {A}^\delta$ for any $\mathbb {A}\in \textsf{Alg}(\mathcal {L})$. In fact, compared to arbitrary $\mathcal {L}$-algebras, $\mathbb {A}^\delta$ enjoys additional properties that make it a suitable semantic environment for the extended language $\mathcal {L}^+$ of Sect. 2.1. Indeed, the lattice reduct of $\mathbb {A}^\delta$ is a complete lattice. Together with the fact that the operations $\Diamond ^\sigma$ and $\Box ^\pi$ do not preserve only finite joins and meets respectively, but arbitrary joins and meets, this implies, by well known order-theoretic facts (cf. [9, Proposition 7.34]), that the right and left adjoint of $\Diamond ^\sigma$ and of $\Box ^\pi$ are well defined on $\mathbb {A}^\delta$, which we denote $\blacksquare ^{\mathbb {A}^\delta }$ and respectively,² and provide the interpretations of the corresponding logical connectives in $\mathcal {L}^+$. Moreover, by denseness, $\mathbb {A}^\delta$ is both completely join-generated by the elements in $K(L^\delta )$ and completely meet-generated by the elements in $O(L^\delta )$, and when considering the non-constructive proof, these families of generators can be further restricted to $J^{\infty }(L^\delta )$ and $M^{\infty }(L^\delta )$, respectively. These generating subsets provide the interpretation of the variables in $\textsf{NOM}$ and $\textsf{CNOM}$, respectively. As is well known, for any set $\varSigma$ of $\mathcal {L}$-sequents, if $\textsf{K}(\varSigma )= \{\mathbb {A}\in \textsf{Alg}(\mathcal {L}) \mid \mathbb {A}\models \varSigma \}$ is closed under taking canonical extensions,³ then the axiomatic extension $\textbf{L}.\varSigma$ is complete w.r.t. the subclass $\textsf{K}^\delta (\varSigma )= \{\mathbb {A}^\delta \mid \mathbb {A}\in \textsf{K}(\varSigma )\}$, because any non-theorem $\xi \ \,{\vdash }\ \,\chi$ will be falsified in the Lindenbaum-Tarski algebra $\mathbb {A}$ of $\textbf{L}.\varSigma$, which is an element of $\textsf{K}(\varSigma )$ by construction, and hence $\xi \ \,{\vdash }\ \,\chi$ will be falsified under the same assignment in $\mathbb {A}^\delta$, given that $\mathbb {A}$ is a subalgebra of $\mathbb {A}^\delta$.

2.3 The Algorithm ALBA

The algorithm ALBA is guaranteed to succeed on a large class of formulas, called (analytic) inductive axioms, and it can be used to automatically generate labelled calculi with good properties equivalently capturing the LE-logics axiomatized by means of those axioms. We refer the reader to [7, Section 6,8] for the proof of correctness and success in the general setting of LE-logics. In the present section, we informally illustrate how the algorithm ALBA works by means of examples, namely, we run ALBA on the modal axioms in $\varSigma =\{\Box p \ \,{\vdash }\ \,p, p \ \,{\vdash }\ \,\Box \Diamond p, \Box p \ \,{\vdash }\ \,\Diamond p, \Diamond \Box p \ \,{\vdash }\ \,\Box \Diamond p\}$ computing their first-order correspondent, which, in turn, can be automatically transformed into an analytic structural rule of a labelled calculus equivalently capturing the axioms (see the table at the end of Sect. 3). In what follows, $\mathbb {A}$ denotes an $\mathcal {L}$-algebra, and $\mathbb {A}^\delta$ denotes its canonical extension. We abuse notation and use the same symbol for the algebra and its domain. We recall that variables $\textbf{j}, \textbf{h}$ and $\textbf{k}$ (resp. $\textbf{m}$) range in the set of the complete join-generators (resp. complete meet-generators) of $\mathbb {A}^\delta$.

The following chain of equivalences is sound on $\mathbb {A}^\delta$:

$$ \begin{aligned} \begin{array}{rcll} &{}&{} \forall p(\Diamond \Diamond p \le \Diamond p)\\ &{} \text {iff} &{} \forall p\forall \textbf{j}\forall \textbf{m}\, ((\textbf{j}\le p\ \& \ \Diamond p\le \textbf{m})\Rightarrow \Diamond \Diamond \textbf{j}\le \textbf{m}) &{} \ \ \ \text {join- and meet-generation}, \Diamond \,\text {c.~join-preserving} \\ &{} \text {iff} &{} \forall \textbf{j}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow \Diamond \Diamond \textbf{j}\le \textbf{m}) &{} \ \ \ \text {Ackermann's lemma}\\ &{} \text {iff} &{} \forall \textbf{j}\forall \textbf{h}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow (\textbf{h}\le \Diamond \textbf{j}\Rightarrow \Diamond \textbf{h}\le \textbf{m})) &{} \\ \end{array} \end{aligned}$$

Indeed, the first equivalence in the chain above is due to the fact that, since the variable $\textbf{j}$ (resp. $\textbf{m}$) ranges over a completely join-generating (resp. completely meet-generating) subset of $\mathbb {A}^\delta$, and $\Diamond$ is completely join-preserving, we can equivalently rewrite the initial inequality as follows: $\forall p(\bigvee \{\Diamond \Diamond \textbf{j}\mid \textbf{j}\le p\}\le \bigwedge \{\textbf{m}\mid \Diamond p\le \textbf{m}\})$, which yields the required equivalence by the definition of the least upper bound and the greatest lower bound of subsets of a poset. The second equivalence is an instance of the core rule of ALBA, which allows to eliminate the quantification over proposition variables. As to the direction from bottom to top, by the monotonicity of $\Diamond$, the inequalities $\textbf{j}\le p$ and $\Diamond p\le \textbf{m}$ immediately imply $\Diamond \textbf{j}\le \Diamond p\le \textbf{m}$, from which the required inequality $\Diamond \Diamond \textbf{j}\le \textbf{m}$ follows by assumption. For the converse direction, for a given interpretations of $\textbf{j}$ and $\textbf{m}$ such that $\Diamond \textbf{j}\le \textbf{m}$, we let p have the same interpretation as $\textbf{j}$. Then this interpretation satisfies both inequalities $\textbf{j}\le p$ and $\Diamond p = \Diamond \textbf{j}\le \textbf{m}$, from which the required inequality $\Diamond \Diamond \textbf{j}\le \textbf{m}$ follows by assumption. The third equivalence immediately follows from considerations similar to those made for justifying the first equivalence; namely, that the inequality $\Diamond \Diamond \textbf{j}\le \textbf{m}$ can be equivalently rewritten as $\bigvee \{\Diamond \textbf{h}\mid \textbf{h}\le \Diamond \textbf{j}\}\le \textbf{m}$, which yields the required equivalence by the definition of a subset of a poset. Analogous arguments can be made to justify the following chains of equivalences:

$$ \begin{aligned} \begin{array}{rcll} &{}&{} \forall p(\Box p \le p)\\ &{} \text {iff} &{} \forall p\forall \textbf{j}\forall \textbf{m}\, ((\textbf{j}\le \Box p\ \& \ p\le \textbf{m})\Rightarrow \textbf{j}\le \textbf{m}) &{} \ \ \ \text {join- and meet-generation} \\ &{} \text {iff} &{} \forall \textbf{j}\forall \textbf{m}\, (\textbf{j}\le \Box \textbf{m}\Rightarrow \textbf{j}\le \textbf{m}) &{} \ \ \ \text {Ackermann's lemma}\\ \end{array} \end{aligned}$$

$$ \begin{aligned} \begin{array}{rcll} &{}&{} \forall p( p \le \Box \Diamond p)\\ &{} \text {iff} &{} \forall p\forall \textbf{j}\forall \textbf{m}\, ((\textbf{j}\le p\ \& \ \Diamond p\le \textbf{m})\Rightarrow \textbf{j}\le \Box \textbf{m}) &{} \ \ \ \text {join- and meet-generation} \\ &{} \text {iff} &{} \forall \textbf{j}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow \textbf{j}\le \Box \textbf{m}) &{} \ \ \ \text {Ackermann's lemma}\\ \end{array} \end{aligned}$$

The second equivalence in the chain above is based on the existence of the adjoints of the maps interpreting the original connectives on canonical extensions of $\mathcal {L}$-algebras (cf. Sect. 2.2). Finally, we remark that carrying out the correspondence arguments above in the algebraic environment of the canonical extensions of $\mathcal {L}$-algebras allows us to clearly identify their pivotal properties, and, in particular, to verify that no property related with the setting of (perfect) distributive lattices (viz. the complete join-primeness of the elements interpreting nominal variables) is required.

3 The Labelled Calculus A.L and Some of Its Extensions

In what follows, we use $p, q, \ldots$ for proposition variables, $A, B, \ldots$ for formulas metavariables (in the original language of the logic), $\textbf{j}, \textbf{i}, \ldots$ for nominal variables, $\textbf{m}, \textbf{n}, \ldots$ for conominal variables, $\textbf{J}, \textbf{H}, \ldots$ (resp. $\textbf{M}, \textbf{N}, \ldots$) for nominal terms metavariables (resp. conominal terms), $\textbf{T}$ for terms metavariables, and $\varGamma , \varDelta , \ldots$ for meta-structures metavariables. Given $p \in \textsf{Prop}$, $\textbf{j}\in \textsf{NOM}$, $\textbf{m}\in \textsf{CNOM}$, the language of (labelled) formulas, terms and structures is defined as follows:

Let us first recall some terminology (see e.g. [21, Section 4.1]) and notation. A ($\mathbf {A.L}$-)sequent is a pair $\varGamma \vdash \varDelta$ where $\varGamma$ and $\varDelta$ (the antecedent and the consequent of the sequent, respectively) are metavariables for meta-structures separated by commas. An inference r, also called an instance of a rule, is a pair (S, s) of a (possibly empty) set of sequents S (the premises) and a sequent s (the conclusion). We identify a rule R with the set of all instances that are instantiations of R. A rule R, also referred to as a scheme is usually presented schematically using metavariables for meta-structures (denoted by upper-case Greek letters $\varGamma , \varDelta , \varPi , \varSigma , \ldots , \varGamma _1, \varGamma _2, \ldots$), or metavariables for structures (denoted by lower-case Latin letters: $a, b, c, \ldots , a_1, a_2, \ldots$ for labelled formulas and $t_1, t_2, t_3, \ldots$ for pure structures), or metavariables for formulas (denoted by $A, B, C, \ldots A_1, A_2, \ldots$, or metavariables for terms (denoted by $\textbf{j}, \textbf{i}, \textbf{h}, \ldots , \textbf{j}_1, \textbf{j}_2, \ldots$ for nominal terms and $\textbf{m}, \textbf{n}, \textbf{o}, \ldots , \textbf{m}_1, \textbf{m}_2, \ldots$ for conominal terms). A rule R with no premises, i.e. $S = \emptyset$, is called an axiom scheme, and an instantiation of such R is called an axiom. The immediate subformulas of a principal formula (see Definition 1) in the premise(s) of an operational inference are called auxiliary formulas. The formulas that are not preserved in an inference instantiating the cut rule are called cut formulas. If the cut formulas are principal in an inference instantiating the cut rule, then the inference is called principal cut. A cut that is not principal is called parametric. A proof of (the instantiation of) a sequent $\varGamma \vdash \varDelta$ is a tree where (the instantiation of) $\varGamma \vdash \varDelta$ occurs as the end-sequent, all the leaves are (instantiations of) axioms, and each node is introduced via an inference. Before providing the list of the primitive rules of $\mathbf {A.L}$, we need two preliminary definitions.

Definition 1 (Analysis)

The specifications are instantiations of meta-structure meta-variables in the statement of R. The parameters of $r \in R$ are substructures of instantiations of (meta-)structure metavariables in the statement of R. A formula instance is principal in an inference $r \in R$ if it is not a parameter in the conclusion of r (except for switch rules).

(Meta-)Structure occurrences in an inference $r \in R$ are in the (symmetric) relation of local congruence in r if they instantiate the same metavariable occurring in the same position in a premise and in the conclusion of R, or they instantiate nonparametric structures in the application of switch rules (namely, in the case of $\mathbf {A.L}\varSigma$, occurrences of labelled formulas $\textbf{j}\le A$ and $A\le \textbf{m}$, or occurrences of pure structures $\textbf{j}\le \textbf{T}$ and $\textbf{T}\le \textbf{m}$). Therefore, the local congruence is a relation between specifications.

Two occurrences instatiating a (meta-)structure are in the inference congruence relation if they are locally congruent in an inference r occurring in a proof $\pi$. The proof congruent relation is the transitive closure of the inference congruence relation in a derivation $\pi$.

Definition 2 (Position)

For any well-formed sequent $\varGamma \ \,{\vdash }\ \,\varDelta$,

• The occurrence of a labelled formula $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is in precedent position if $\textbf{j}\le A \in \varGamma$ (resp. $A \le \textbf{m}\in \varDelta$), and it is in succedent position if $\textbf{j}\le A \in \varDelta$ (resp. $A \le \textbf{m}\in \varGamma$);

• any occurrence of a pure structure $\textbf{j}\le \textbf{T}$ in $\varGamma$ (resp. $\varDelta$) is in precedent (resp. succedent) position; any occurrence of a pure structure $\textbf{T}\le \textbf{m}$ in $\varGamma$ (resp. $\varDelta$) is in succedent (resp. precedent) position.

We follow the notational conventions as stated in Definition 1, which provides the so-called analysis of the rules of any proper labelled calculus. In particular, according to Definition 1, notice that if an occurrence $\sigma$ is a substructure of $\varPi \in \{\varGamma , \varGamma ', \varDelta , \varDelta '\}$ occurring in an instantiation r of a rule $R \in \mathbf {A.L}$ (including axioms, namely rules with no premises), then $\sigma$ is a parameter of r and every other $\sigma '$ is nonparametric in r;⁴ moreover, if $\sigma$ occurs in a premise and in the conclusion of r in the same position (namely, in precedent versus in succedent position: see Definition 2), then these two occurrences of $\sigma$ are locally congruent in r.⁵ Notice that in the display calculi literature ‘being locally congruent’ usually presupposes ‘being parametric’, but in labelled calculi this is not anymore the case due to the presence of switch rules (see Remark 1).

The initial rules above encode identities for atomic propositions and zeroary connectives, namely the fact that the derivability relation $\ \,{\vdash }\ \,$ is reflexive. Identity sequents of the form $\textbf{j}\le A \ \,{\vdash }\ \,\textbf{j}\le A$ (resp. $A \le \textbf{m}\ \,{\vdash }\ \,A \le \textbf{m}$) are derivable in the calculus.

The initial rules for $\bot$ (resp. $\top$) above encodes the fact that $\bot$ is interpreted as the minimal element (resp. $\top$ as the maximal element) in the algebraic interpretation.

The cut rules below encode the fact that the derivability relation $\ \,{\vdash }\ \,$ is transitive. Notice that the notion of ‘cut formula’ in standard Gentzen sequent calculi corresponds to ‘labelled cut formula’ in the present setting. Before defining the cut rules, we need the following definition.

Definition 3

A labelled formula a is a $\textbf{j}$-labelled (resp. $\textbf{m}$-labelled) formula in a derivation $\pi$ if the uppermost labelled formulas congruent with a in $\pi$ are introduced via $\text {Id}_{\textbf{j}\le p}, \bot _{\textbf{j}}, \top _{\textbf{j}}, \wedge _P, \wedge _S, \Box _P, \Box _S$ (resp. $\text {Id}_{p \le \textbf{m}}, \bot _{\textbf{m}}, \top _{\textbf{m}}, \vee _P, \vee _S, \Diamond _P, \Diamond _S$).

The switch rules below encode elementary properties of pairs of inequalities with the same approximant (either a nominal $\textbf{j}$ or a conominal $\textbf{m}$) occurring in the same sequent with opposite polarity (namely, the first in precedent position and the second in succedent position: see Definition 2). Notice that we might use S as a generic name denoting a specific switch rule in the following set. If so, we rely on the context to disambiguate which rule we are referring to. In particular, the label S is unambiguous whenever we use it as the name for a rule application in a derivation.

Remark 1 (Analysis of switch rules)

For each instantiation r of $R \in \{\text {S}\textbf{T}\textbf{T}'\textbf{m}, \text {S}\textbf{j}\textbf{T}\textbf{T}'\}$, the instantiations of $\textbf{j}\le \textbf{T}''$ and $\textbf{T}'' \le \textbf{m}$ (where $\textbf{T}'' \in \{\textbf{T}, \textbf{T}'\}$) are nonparametric and locally congruent in r (see Definition 1). For each instantiation r of any other switch rule R, the instantiations of $\textbf{j}\le C$ and $C \le \textbf{m}$ (where $C \in \{A, B\}$) are nonparametric and locally congruent in r (see Definition 1).

The adjunction rules above encode the fact that unary modalities $\Diamond , \blacksquare$ and constitute pairs of adjoint operators. The structural rules $\top _\Box$ (resp. $\bot _\Diamond$) above encodes the fact that $\Box$ preserve $\top$ (resp. $\Diamond$ preserves $\bot$).

The logical rules below encode the minimal order-theoretic properties and the arity of propositional and modal connectives.

We consider the following logical rules for modalities, where $\Box _S$ and $\Diamond _P$ are invertible, but $\Box _P$ and $\Diamond _S$ are not. This choice facilitates a smoother analysis of the rules and therefore it is preferable whenever the goal is to provide a canonical cut elimination.

Remark 2

The invertible version of $\wedge _P$, $\vee _S$, f $\Box _P$ and $\Diamond _S$ are as follows:

Invertible rules can be used whenever the goal is to facilitate backwards-looking proof searches. In this case, the initial rules have to be generalized accordingly.

The table below collects the analytic rules, both in the format of display calculi and in the present format, generated by reading off the ALBA outputs of the corresponding axioms reported on in Sect. 2.3.

Where $\textbf{k}$ in rules C and D must not appear in $\varGamma , \varDelta$. For any $\varSigma \subseteq \{(T), (4), (B), (D), (C)\}$, we let $\mathbf {A.L}\varSigma$ be the calculus defined by the rules in the sections above plus the additional rules in the table above corresponding to the axioms in $\varSigma$. We let $\mathbf {A.L}: = \mathbf {A.L}\varnothing$.

4 Properties of the Calculus $\mathbf {A.L}\varSigma$

4.1 Soundness

In the present section, we show that, for any $\varSigma \subseteq \{(T), (4), (B), (D), (C)\}$, the rules of $\mathbf {A.L}\varSigma$ are sound on the class $\textsf{K}^\delta (\varSigma ): = \{\mathbb {A}^\delta \mid \mathbb {A}\models \varSigma \}$. Firstly, let us recall that, as usual, any $\mathbf {A.L}$-sequent $\varGamma \ \,{\vdash }\ \,\varDelta$ is to be interpreted as “any assignment of the variables in $\textsf{Prop}\cup \textsf{NOM}\cup \textsf{CNOM}$ under which all inequalities in $\varGamma$ are satisfied also satisfies some inequality in $\varDelta$”; in symbols: .

As to the basic calculus $\mathbf {A.L}$, the soundness of the initial rules, cut rules, adjunction rules, and logical rules for propositional connectives is straightforward. The soundness of the switch rules hinges on the fact that nominal and co-nominal variables range over completely join-generating and completely meet-generating subsets of $\mathbb {A}^\delta$ for any $\mathcal {L}$-algebra $\mathbb {A}$. For example, the soundness of S$\textbf{j}\textbf{m}$ follows from the following chain of equivalences:

Since $\textbf{m}$ does not occur in $\varGamma$ and $\varDelta$, the rule is also invertible. The verification of the soundness of the remaining switch rules is similar.

The soundness and invertibility of the introduction rules for the modal connectives hinge on the fact that the operation $\Diamond ^\sigma$ (resp. $\Box ^\pi$) is completely join-preserving (resp. completely meet preserving) and on the complete- join-generation and meet-generation properties of the subsets of $\mathbb {A}^\delta$ on which nominal and co-nominal variables are interpreted. For example, the soundness and invertibility of $\Box _S$ is verified via the following chain of equivalences:

The soundness of $\Box _P$ immediately follows from the monotonicity of $\Box ^\pi$. Indeed, fix an assignment of variables in $\textsf{Prop}\cup \textsf{NOM}\cup \textsf{CNOM}$ under which all inequalities in $\varGamma$ and $\textbf{j}\le \Box A$ are satisfied. If such assignment also satisfies $A\le \textbf{n}$, then, by monotonicity, $\textbf{j}\le \Box A\le \Box \textbf{n}$, as required. The proof for the rules $\Diamond _P$ and $\Diamond _S$ is similar.

As to the extended calculus $\mathbf {A.L}\varSigma$, the soundness of rule (4) is verified by the following chain of computations holding on the canonical extension of any $\mathcal {L}$-algebra $\mathbb {A}$ such that $\mathbb {A}\models \Diamond \Diamond p\le \Diamond p$:

The key step in the computation above is the one which makes use of the assumption of axiom (4) being valid on $\mathbb {A}$. Indeed, by the general theory of correspondence for LE-logics (cf. [7]), axiom (4) is canonical, hence the assumption implies that (4) is valid also on $\mathbb {A}^\delta$. Then, as is shown in the computation concerning axiom (4) in Sect. 2.3, the validity of (4) in $\mathbb {A}^\delta$ is equivalent to the condition $\forall \textbf{j}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow \Diamond \Diamond \textbf{j}\le \textbf{m})$ holding in $\mathbb {A}^\delta$, which justifies this key step. The verification of the remaining additional rules hinges on similar arguments and facts (in particular, all axioms we consider are canonical), so in what follows we only report on the corresponding computations.

The soundness of the rule (C) is verified by the following chain of computations holding on the canonical extension of any $\mathcal {L}$-algebra $\mathbb {A}$ such that $\mathbb {A}\models \Diamond \Box p\le \Box \Diamond p$:

Instantiating $\textbf{i}$ as $\textbf{h}$ completes the proof. The key step in the computation above is the one which makes use of the assumption of axiom (C) being valid on $\mathbb {A}$. Indeed, by the general theory of correspondence for LE-logics (cf. [7]), axiom (C) is canonical, hence the assumption implies that (C) is valid also on $\mathbb {A}^\delta$. Then, as is shown in the computation concerning axiom (C) in Sect. 2.3, the validity of (C) in $\mathbb {A}^\delta$ is equivalent to the condition holding in $\mathbb {A}^\delta$, which justifies this key step.

The soundness of the rules (D), (T), (B) is verified in a similar way.

4.2 Syntactic Completeness

In the present section, we show that all the axioms and rules of the basic logic are derivable in $\mathbf {A.L}$, and that for any $\varSigma \subseteq \{$(T), (4), (B), (D), (C)$\}$, the axioms and rules of $\textbf{L}\varSigma$ are derivable in $\mathbf {A.L}\varSigma$.⁶

The sequents $p \ \,{\vdash }\ \,p$, $\bot \ \,{\vdash }\ \,p$, $p \ \,{\vdash }\ \,\top$, $p \ \,{\vdash }\ \,p \vee q$ ($q \ \,{\vdash }\ \,p \vee q$), and $p \wedge q \ \,{\vdash }\ \,p$ ($q \wedge p \ \,{\vdash }\ \,q$) are trivially derivable with one single application of the rule $Id_{\textbf{j}\le q}$, $\bot _w$, $\top _w$, $\vee _S$, and $\wedge _P$, respectively. The derivability of the rules $\frac{\varphi \ \,{\vdash }\ \,\chi \ \chi \ \,{\vdash }\ \,\psi }{\varphi \ \,{\vdash }\ \,\psi }$, $\frac{\varphi \ \,{\vdash }\ \,\chi \ \psi \ \,{\vdash }\ \,\chi }{\varphi \vee \psi \ \,{\vdash }\ \,\chi }$, and $\frac{\chi \ \,{\vdash }\ \,\varphi \ \chi \ \,{\vdash }\ \,\psi }{\chi \ \,{\vdash }\ \,\varphi \wedge \psi }$ can be shown by derivations in which the cut rules, $\vee _P$, and $\wedge _S$, respectively, are applied. The two derivations below show the rules concerning the connectives $\Box$ and $\Diamond$:

To show the admissibility of the substitution rule $\frac{\varphi \ \,{\vdash }\ \,\psi }{\varphi (\chi /p) \ \,{\vdash }\ \,\psi (\chi /p)}$, a straightforward induction on the derivation height of $\varphi \ \,{\vdash }\ \,\psi$ suffices.

As to the axioms and rules of the basic logic $\textbf{L}$, below, we derive the axioms encoding the distributivity of $\Diamond$ over $\vee$ and $\bot$ in $\mathbf {A.L}$. The distributivity of $\Box$ over $\wedge$ and $\top$ is derived similarly.

The syntactic completeness for the other axioms and rules of $\textbf{L}$ can be shown in a similar way. In particular, the admissibility of the substitution rule can be proved by induction in a standard manner.

As to the axiomatic extensions of $\textbf{L}$, Let us consider the axiom $(4)\ \Diamond \Diamond A \vdash \Diamond A$. Using ALBA we generate the first order correspondent $\forall \textbf{j}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow \Diamond \Diamond \textbf{j}\le \textbf{m})$. Further processing the axiom (4) using ALBA we obtain the equivalent first order correspondent (in the so-called ‘flat form’): $\forall \textbf{j}\forall \textbf{h}\forall \textbf{m}\, (\Diamond \textbf{j}\le \textbf{m}\Rightarrow (\textbf{h}\le \Diamond \textbf{j}\Rightarrow \Diamond \textbf{h}\le \textbf{m}))$, which can be written as a structural rule in the language of ALBA labelled calculi as follows:

We now provide a derivation of the axiom (4) in the basic labelled calculus $\mathbf {A.L}$ expanded with the previous structural rule 4.

Analogously, we provide a derivation of the axioms (T), (B), (D), and (C) in the basic labelled calculus $\mathbf {A.L}$ expanded with the structural rules T, B, D, and C, respectively.

4.3 Conservativity

In the present section, we argue that, for any $\varSigma \subseteq \{(T), (4), (B), (D), (C)\}$ and all $\mathcal {L}$-formulas A and B, if the $\mathbf {A.L}$-sequent $\textbf{j}\le A\ \,{\vdash }\ \,\textbf{j}\le B$ is derivable in $\mathbf {A.L}\varSigma$, then the $\mathcal {L}$-sequent $A\ \,{\vdash }\ \,B$ is an $\textbf{L}.\varSigma$-theorem.

Indeed, because the rules of $\mathbf {A.L}$ are sound in the class $\textsf{K}^\delta (\varSigma )= \{\mathbb {A}^\delta \mid \mathbb {A}\models \varSigma \}$, the assumption implies that $\mathbb {A}^\delta \models \forall \overline{p}\forall \textbf{j}(\textbf{j}\le A\Rightarrow \textbf{j}\le B)$ which, by complete join-generation, is equivalent to $\mathbb {A}^\delta \models \forall \overline{p}( A\le B)$. Since, as discussed in Sect. 2.2, $\textbf{L}.\varSigma$ is complete w.r.t. $\textsf{K}^\delta (\varSigma )$, this implies that $A\ \,{\vdash }\ \,B$ is a theorem of $\textbf{L}.\varSigma$, as required.

4.4 Cut Elimination and Subformula Property

As usual in the tradition of display calculi, we first characterize a new class of calculi. The actual definition is given in Appendix A. Here we just mention that a proper labelled calculus is a proof systems satisfying the conditions C$_2$–C$_8$ of Definition 6. Then, in the appendix, we prove the following general result, namely a canonical cut elimination theorem à la Belnap for any calculus in this class:

Theorem 1

Any proper labelled calculus enjoys cut-elimination. If also the condition C$_1$ in Definition 6 is satisfied, then the proof system enjoys the subformula property.

Finally, we obtain that the calculi $\mathbf {A.L}\varSigma$ introduced in Sect. 3 enjoys cut elimination and subformula property thanks to the following result, proved in Sect. 5.

Corollary 1

$\mathbf {A.L}\varSigma$ is a proper labelled calculus.

5 $\mathbf {A.L}\varSigma$ Is a Proper Labelled Calculus

In this section we first show that $\mathbf {A.L}\varSigma$ has the display property and then we provide a proof of Corollary 1 as stated in Sect. 4.4.

Lemma 1

Let s be any derivable sequent in $\mathbf {A.L}\varSigma$. Then, up to renaming of the variables, every nominal or conominal occurring in s occurs in it exactly twice and with opposite polarity.

Proof

The proof is by induction on the height of the derivation. The statement is trivially true for the axioms. All the rules in the calculi with the exception of the cut-rules either (a) introduce two occurrences of a new label, (b) eliminate two occurrences of the same existing label, or (c) keep the labels in the sequent intact. Before applying the same reasoning to Cut$_{\,\textbf{j}\le A}$ and Cut$_{\,A\le \textbf{m}}$, we must take care of renaming nominals and conominals in $\varGamma ,\varGamma ',\varDelta ,\varDelta '$ to avoid conflicts. Thus, up to substitution, any variable occurring in a derivable sequent occurs exactly twice.

To prove that $\mathbf {A.L}\varSigma$ has the display property (see Definition 5) we need the following definition:

Definition 4

Let $s= \varGamma \ \,{\vdash }\ \,\varDelta$ be any sequent. For any structure $\sigma = \textbf{j}\le \textbf{T}$, (resp. $\sigma =\textbf{T}\le \textbf{m}$) in $\varGamma$, we say that it has a $\textbf{j}$-twin (resp. $\textbf{m}$-twin) iff there exists exactly one occurrence of $\textbf{j}$ (resp. $\textbf{m}$) in $\varDelta$.

Proposition 1

For any derivable sequent $s=\varGamma \ \,{\vdash }\ \,\varDelta$ and any structure $\sigma = \textbf{j}\le \textbf{T}$ (resp. $\sigma = \textbf{T}\le \textbf{m}$) in $\varGamma$ there exists a sequent $s' =\varGamma ' \ \,{\vdash }\ \,\varDelta '$ which is interderivable with s such that $\sigma \in \varGamma '$ and $\sigma$ has a $\textbf{j}$-twin (resp. $\textbf{m}$-twin) in $s'$.

Proof

A sequent s is said to have the $\textbf{j}$-twin property (resp. $\textbf{m}$-twin property) iff every structure of the form $\textbf{j}\le \textbf{T}$ (resp. $\textbf{T}\le \textbf{m}$) has a $\textbf{j}$-twin (resp. $\textbf{m}$-twin) in $\varDelta$. Notice that the conclusions of initial rules satisfy all twin properties trivially. We say that an inference rule preserves the twin property if the premises having a certain twin property implies that the conclusion has the same twin property.

All the rules in the basic calculus which do not involve switching of structural terms (i.e. all the rules except for the rules S$\textbf{T}\textbf{m}$, S$\textbf{m}\textbf{T}$, S$\textbf{T}\textbf{j}$, S$\textbf{j}\textbf{T}$, S$\textbf{T}\textbf{T}'\textbf{m}$, S$\textbf{j}\textbf{T}\textbf{T}'$) and the rules T, B, and C preserve the twin property, since, for each nominal $\textbf{j}$ or conominal $\textbf{m}$ in the rule, one of the following holds:

• 1. each occurrence of $\textbf{j}$ or $\textbf{m}$ remains on the same side in the conclusion as it was in the premise (adjunction rules, rules for propositional connectives, T, B);

• 2. exactly two occurrences of $\textbf{j}$ (resp. $\textbf{m}$) are eliminated (cut, S$\textbf{m}$, S$\textbf{j}$, $\Box _S$, $\Diamond _P$, D, C);⁷

• 3. $\textbf{j}$ (resp. $\textbf{m}$) does not occur in the premise, and exactly two occurrences of $\textbf{j}$ (resp. $\textbf{m}$) are added in the conclusion, one in the antecedent and one in the consequent of the conclusion ($\top _\Box$, $\bot _\Diamond$, $\Box _P$, $\Diamond _S$, C).

Notice that rule C occurs both in items 2 and 3 and, in particular, we can assume that the nominal $\textbf{h}$ in the conclusion of C is fresh (see the proof of Lemma 2).

In the case one of the S$\textbf{T}\textbf{m}$, S$\textbf{m}\textbf{T}$, S$\textbf{T}\textbf{j}$, S$\textbf{j}\textbf{T}$, S$\textbf{T}\textbf{T}'\textbf{m}$, S$\textbf{j}\textbf{T}\textbf{T}'$ rules is applied, the twin property can be broken, as nominals (resp. conominal) contained in the structural terms $\textbf{T},\textbf{T}'$ switch side without their twin nominals (resp. conominals) doing the same. Let $R=\frac{\varGamma _1 \ \,{\vdash }\ \,\varDelta _1}{\varGamma _2 \ \,{\vdash }\ \,\varDelta _2}$ be an application of any of these rules. Let $\sigma \in \varGamma _1 \cap \varGamma _2$ be a structure which has a twin in $\varDelta _1$ but not in $\varDelta _2$. This is only possible if $\sigma$ is of the form $\textbf{i}\le \textbf{T}_1$ (resp. $\textbf{T}_1 \le \textbf{n}$) and there exists a $\sigma '$ of the form $\textbf{T}\le \textbf{m}$ (resp.  $\textbf{j}\le \textbf{T}$) for some $\textbf{T}$ containing $\textbf{i}$ (resp. $\textbf{n}$) which will appear in $\varGamma _2$ with $\textbf{j}$ (resp. $\textbf{m}$) introduced fresh. We can switch the term $\textbf{T}$ back to the right by using the switch rule applicable to the conclusion of R, which gives a sequent of the same form as $\varGamma _1\ \,{\vdash }\ \,\varDelta _1$, but with a fresh conominal (resp. nominal) in the place of $\textbf{m}$ (resp. $\textbf{j}$). Here, we show the proof for the rules S$\textbf{T}\textbf{T}'\textbf{m}$ and S$\textbf{m}\textbf{T}$, the proof for other rules being similar.

Let $s' =\varGamma _3 \ \,{\vdash }\ \,\varDelta _3$ be any sequent derived from $\varGamma _2 \ \,{\vdash }\ \,\varDelta _2$ such that $\sigma \in \varGamma _3$. If $\sigma ' \notin \varGamma _3$, it must have been switched to the right by a switch rule, as all other rules leave pure structures on the left intact. However, whenever a switch rule is applied, the term $\textbf{T}$ occurs on the right of the sequent and has a twin. Thus, if the last rule of the derivation is such a switch rule, then $\sigma$ has a twin in $s'$. If $\sigma ' \in \varGamma _3$ and $\sigma '$ has a twin structure, then we can switch $\textbf{T}$ to right by the application of an appropriate switch rule leading to a interderivable sequent in which $\sigma$ has a twin. Thus, reasoning by induction, it is enough to show that $\sigma '$ has a twin when it occurs for the first time (by the application of the switch rule). This is immediate from the fact that the label occurring in $\sigma ' \in \varGamma _3$ in any switch rule is of the form $\textbf{j}\le \textbf{T}$ or $\textbf{T}\le \textbf{m}$ where $\textbf{j}$ or $\textbf{m}$ is fresh and also occurs in $\varDelta _3$. Thus switch rules preserve the twin property.

Let $R=\frac{\varGamma _1 \ \,{\vdash }\ \,\varDelta _1}{\varGamma _2 \ \,{\vdash }\ \,\varDelta _2}$ be an application of rule (4). Let $\sigma \in \varGamma _1 \cap \varGamma _2$ be a structure which has a twin in $\varDelta _1$ but not in $\varDelta _2$. This is only possible if $\sigma$ is of the form $\textbf{j}\le \textbf{T}\in \varGamma$ for some structure $\textbf{T}$. In this case, after the application of 4 we can reintroduce the relevant twin structure $\Diamond \textbf{j}\le \textbf{m}$ in the following way.

The rest of the proof now follows by the same inductive algorithm.

We can now prove the display property of the calculus.

Proposition 2

If $s =\varGamma \ \,{\vdash }\ \,\varDelta$ is a derivable $\mathbf {A.L}\varSigma$-sequent, then every structure $\sigma$ occurring in s is displayable (see Definition 5).

Proof

We prove the display property only for the structures of the form $\textbf{j}\le \textbf{T}$ and $\textbf{j}\le A$. The proof for structures of the form $\textbf{T}\le \textbf{m}$ and $A \le \textbf{m}$ are dual. Let $\sigma$ be a structure of the form $\textbf{j}\le \textbf{T}$ or $\textbf{j}\le A$. By Lemma 1, $\textbf{j}$ occurs exactly twice in any derivable sequent. Let $\sigma '$ be the structure containing the other occurrence of $\textbf{j}$. If $\sigma '$ is a labelled formula we are done. The set of well-formed pure structures containing $\textbf{j}$ is the following: . For any derivable sequent $s = \varGamma \vdash \varDelta$, it is easy to verify the following (by inspection of all the rules in $\mathbf {A.L}$):

• (a) if $\Diamond \textbf{j}\le \textbf{n}$ (resp. $\textbf{i}\le \Box \textbf{m}$) occurs in s, then it occurs in $\varDelta$, given that $\Diamond _S$ and $\bot _\Diamond$ (resp. $\Box _P$ and $\top _\Box$) are the only rules introducing such a structure;

• (b) if   (resp. $\textbf{i}\le \blacksquare \textbf{m}$) occurs in s, then it occurs in $\varDelta$, given that and $\blacksquare$ can be introduced only via adjunction rules to structures $\Diamond \textbf{j}\le \textbf{n}$ and $\textbf{i}\le \Box \textbf{m}$ which only occur in $\varDelta$ by (a);

• (c) if any pure structure occurs in s, then it occurs in $\varGamma$, given that they can only be introduced via a switch rule (namely, S$\textbf{T}\textbf{m}$, S$\textbf{T}\textbf{j}$, S$\textbf{T}\textbf{T}'\textbf{m}$, S$\textbf{j},\textbf{T}\textbf{T}'$).

Case (a) and (b). If $\textbf{j}$ (resp. $\textbf{m}$) occurs in some pure structure $\Diamond \textbf{j}\le \textbf{n}$ or (resp. $\textbf{i}\le \Box \textbf{m}$ or $\textbf{i}\le \blacksquare \textbf{m}$), then it occurs in $\varDelta$ and it is displayable through a single application of an adjunction rule.

Case (c). If $\textbf{j}$ (resp. $\textbf{m}$) occurs in some pure structure $\textbf{i}\le \Diamond \textbf{j}$, (resp. $\Box \textbf{m}\le \textbf{n}$, $\blacksquare \textbf{m}\le \textbf{n}$), then it occurs in $\varGamma$. If we can apply a switch rule moving the relevant complex term to $\varDelta$, we reduce ourselves to the previous cases (a) or (b) and we are done. We will consider the case where a pure structure $\textbf{i}\le \Diamond \textbf{j}$ occurs on the left. All the other cases are treated analogously. By Proposition 1, there exists a sequence $s' =\varGamma ' \ \,{\vdash }\ \,\varDelta '$ such that $s'$ is interderivable with s, $\textbf{i}\le \Diamond \textbf{j}$ occurs in $\varGamma '$ and has an $\textbf{i}$-twin (resp. $\textbf{n}$-twin) in $s'$. Thus, $\textbf{i}$ occurs in $\varDelta '$ by definition. By (a) and (b), $\textbf{i}$ can occur in $\varDelta '$ in one of the structures $\textbf{i}\le A$, $\textbf{i}\le \textbf{m}$ $\Diamond \textbf{i}\le \textbf{m}$, or . If $\textbf{i}$ occurs in $\textbf{i}\le A$ or $\textbf{i}\le \textbf{m}$, we can apply a switch rule with $\textbf{i}\le \Diamond \textbf{j}$ to reduce ourselves to previous cases. If $\textbf{i}$ occurs in the structure of the form $\Diamond \textbf{i}\le \textbf{m}$ or , we first apply adjunction and then proceed in the same way. This concludes the proof of display property for the basic calculus.

In case of the axiomatic extensions, we need to argue that the added rules preserve the property in Proposition 1. Notice that all the additional rules preserve the Lemma 1.

In case of rules (T), (B), and (C) no variables nominals or conominals switch side thus the twin structures are preserved by these rules. (4): The rule 4 moves $\Diamond \textbf{j}$ from the right to the left. Thus, the only structure in $\varGamma$ which loses the twin property is some structure $\sigma$ in $\varGamma$ containing $\textbf{j}$. However, just like in the case of the switch rules we can switch $\textbf{j}$ back to the right by applying an adjunction followed by a switch rule on $\textbf{h}$ as follows.

Thus, the twin of $\sigma$ reappears. We can now argue that the existence of an interderivable sequent with a twin is preserved in a derivation containing an application of this rule in similar way as we did with the switch rules.

(D): In case of rule D, as the premise contains the structure , there must be another structure $\sigma \in \varGamma$ containing $\textbf{j}$ of the form $\textbf{j}\le A$ or $\textbf{j}\le \textbf{T}$. The premise must be interderivable with a sequent in which $\sigma$ has a twin. However, in the conclusion $\textbf{k}$ does not occur and $\textbf{j}\le \Box \textbf{m}$ occurs on the right. Thus, $\sigma$ has a twin in the conclusion. All other nominals and conominals in the premise stay on the same side in the conclusion. Thus, rule D preserves the property of existence of interederivable sequent with the twin property.

To show that $\mathbf {A.L}\varSigma$ is a proper labelled calculus, we need to verify that $\mathbf {A.L}\varSigma$ satisfies each condition in Definition 6. The verification of the conditions C6 and C7 requires to preliminarily show the following:

Lemma 2 (Preservation of principal formulas’ approximants)

If the sequents s and $s'$ occur in the same branch b of an $\mathbf {A.L}\varSigma$-derivation $\pi$, $\textbf{j}\le A \in s$ and $\textbf{i}\le A \in s'$ (resp. $A \le \textbf{m}\in s$ and $A \le \textbf{n}\in s'$) are congruent in b (see Definition 5), $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is principal in s and $\textbf{i}\le A$ (resp. $A \le \textbf{n}$) is in display in $s'$, then the term occurring in $\textbf{i}\le A$ (resp. $A \le \textbf{n}$) in $\pi$ can be renamed in a way such that $\textbf{i}= \textbf{j}$ (resp. $\textbf{n}= \textbf{m}$), and the new derivation $\pi '$ is s.t. $\pi ' \equiv \pi$ modulo a renaming of some nominal or conominal.

Proof

Assume that $\textbf{j}\le A \in s$ and $\textbf{i}\le A \in s'$ (resp. $A \le \textbf{m}\in s$ and $A \le \textbf{n}\in s'$) are congruent in the branch b of a derivation $\pi$, $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is principal in s and $\textbf{i}\le A$ (resp. $A \le \textbf{n}$) is in display in $s'$. This means that there is a sub-branch $b' \subseteq b$ connecting s and $s'$ and the height of s is strictly smaller than the height of $s'$ in $\pi$, given that $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is principal in s. If $\textbf{j}\le A$ stays parametric in $b'$, then $\textbf{j}= \textbf{i}$ (resp. $\textbf{m}= \textbf{n}$). If not, it means that $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is nonparametric in an even number of applications of switch rules occurring in $b'$, given that $\textbf{j}\le A$ and $\textbf{i}\le A$ (resp. $A \le \textbf{m}$ and $A \le \textbf{n}$) are both approximated by a nominal (resp. conominal) and a single application of a switch rules changes the nominal (resp. conominal) approximating a formula into a conominal (resp. nominal). W.l.o.g. we can confine ourselves to consider a branch $b'$ with exactly two applications of switch rule involving $\textbf{j}\le A$ and $\textbf{i}\le A$ (resp. $\textbf{m}\le A$) as nonparametric structures. If a rule R is applied in $b'$, R is not a switch rule, and x is a nominal or conominal occurring in a nonparametric strucure in the conclusion of R but not necessarily occurring in the premise(s) of R, then we can pick x fresh in the entire sub-branch $b'' \subseteq b'$ connecting the conclusion of R with the sequent s. In the case of $\mathbf {A.L}\varSigma$, such rule R is either $\Box _P$, $\Diamond _S$, C, or 4. Therefore, $\textbf{j}$ (resp. $\textbf{m}$) occurs neither in the premise nor in any parametric structure in the conclusion of S, where S is any application of a switch rules in the branch $b'$ and s.t. $\textbf{i}\le A$ (resp. $A \le \textbf{n}$) is a nonparametric structure in the conclusion of S. So, the side conditions of switch rules are satisfied, and in any application of such S we can switch $\textbf{i}$ for $\textbf{j}$ (resp. $\textbf{n}$ for $\textbf{m}$).

We now proceed to check all the conditions C$_1$-C$_8$ defining proper labelled calculi.

Proof

The fact that $\mathbf {A.L}\varSigma$ satisfies condition C$'_5$ is proved in Proposition 2. To show that $\mathbf {A.L}\varSigma$ satisfies condition C$_8$ we need to consider all possible principal cuts.

Below we consider cut formulas introduced by initial rules and we exhibit a new cut-free proof that is an axiom as well (notice that axioms are defined with empty contexts). The principal cut formula is $\textbf{j}\le \top$ or $\textbf{j}\le p$, $R \in \{\text {Id}_{\textbf{j}\le p}, \text {Id}_\top , \top _w\}$, and x, y, z are instantiated accordingly to R (the proof for $\bot \le \textbf{m}$ or $p \le \textbf{m}$, and $R \in \{\text {Id}_{p\le m}, \text {Id}_\bot , \bot _w\}$ is similar and it is omitted).

Below we consider formulas introduced by logical rules. The side conditions on logical rules impose that the parametric structures are in display or can be displayed with a single application of an adjunction rule, therefore we can provide the following proof transformations where the newly generated cuts are well-defined (in particular the cut formulas are in display) and of lower complexity (the new cut formulas are immediate subformulas of the original cut formulas).

The principal cut formula is $\Box A$ and A is $\textbf{m}$-labelled formula (see Definition 3).

The principal cut formula is $\Box A$ and A is a $\textbf{j}$-labelled formula (see Definition 3): in this case the original cut is as in the proof above. The principal cut elimination transformation requires we perform a new cut on the immediate labelled subformulas $A \le \textbf{m}$, but, given A is a $\textbf{j}$-labelled formula by assumption, only Cut$_{\textbf{j}\le A}$ can be applied, so we need first to apply the appropriate switch rules changing the approximants of the immediate subformulas A on both branches. In branch $\pi _1$ of the original proof, we can apply adjunction and derive where is the twin structure (see Definition 4) of $A \le \textbf{m}$, so we can apply the rule S$\textbf{T}\textbf{j}$. In branch $\pi _2$, Proposition 1 ensures that $\varGamma ' \ \,{\vdash }\ \,A \le \textbf{m}, \varDelta '$ is interderivable with $\varGamma '', x \le \textbf{m}\ \,{\vdash }\ \,A \le \textbf{m}, \varDelta ''$ for some x formula or x pure structure, where $x \le \textbf{m}$ is the twin structure of $A \le \textbf{m}$. Therefore, we can apply the appropriate switch rule changing the approximant of A. The proof transformation is detailed below.

The principal cut formula is $A \wedge B$ and both immediate subformulas are $\textbf{j}$-labelled formulas (the case in which at least one immediate subformula is an $\textbf{m}$-labelled formula is analogous to the proof transformation step for $\Diamond A$ and it is omitted. The case for $A \vee B$ are similar and they are omitted).

To show that $\mathbf {A.L}\varSigma$ satisfies all the other conditions is immediate and it requires inspecting all the rules in $\mathbf {A.L}\varSigma$.

6 Conclusions

In the present paper, we have showcased a methodology for introducing labelled calculi for nonclassical logics (LE-logics) in a uniform and principled way, taking the basic normal lattice-based modal logic $\textbf{L}$ and some of its axiomatic extensions as a case study. This methodology hinges on the use of semantic information to generate calculi which are guaranteed by their design to enjoy a set of basic desirable properties (soundness, syntactic completeness, conservativity, cut elimination and subformula property). Interestingly, the methodology showcased in the present paper naturally imports the one developed and applied in [15] in the context of proper display calculi to the proof-theoretic format of labelled calculi. Specifically, just like the algorithm ALBA, the main tool in unified correspondence theory, was used in [1, 15] to generate proper display calculi for basic (D)LE-logics in arbitrary signatures and their axiomatic extensions defined by analytic inductive axioms, in the present paper, ALBA is used to generate labelled calculi for $\textbf{L}$ and 31 of its axiomatic extensions. Similarly to extant labelled calculi in the literature (viz. those introduced in [16]), the language of the calculi introduced in the present paper manipulate a language which properly extends the original language of the logic, and includes labels. However, the language of these labels is the same language manipulated by ALBA, the intended interpretation of which is provided by a suitable algebraic environment, rather than by a relational one; specifically, by the canonical extensions of the algebras in the class canonically associated with the given logic. Just like the use of canonical extensions as a semantic environment for unified correspondence theory has allowed for the mechanization and uniform generalization of correspondence arguments from classical normal modal logic to the much wider setting of normal LE-logics without relying on the availability of any particular relational semantics, this same semantic setting allows for the uniform generation of labelled calculi for LE-logics in a way that does not rely on a particular relational semantics. However, via general duality theoretic facts, these calculi will be sound also w.r.t. any relational semantic environment for the given logic, and can also provide a “blueprint” for the introduction of labelled calculi designed to capture the logics of specific classes of relational structures (cf. [20]). In future work, we will generalize the current results to arbitrary LE-signatures, and establish systematic connections, via formal translations, between proper display calculi and labelled calculi for LE-logics.

A Proper Labelled Calculi

In what follows we provide a formal definition of the display property and proper labelled calculi.

Definition 5 (Display)

A nominal $\textbf{j}$ (resp. conominal $\textbf{m}$) is always in display in a labelled formula $\textbf{j}\le A$ (resp. $A\le \textbf{m}$), and is in display in a pure structure t iff $t=\textbf{j}\le \textbf{T}$ (resp. $t=\textbf{T}\le \textbf{m}$) for some term $\textbf{T}$ such that $\textbf{j}$ does not occur in $\textbf{T}$.

A pure structure $\textbf{j}\le \textbf{T}$ (resp. $\textbf{T}\le \textbf{m}$) is in display in a sequent s if $\textbf{j}$ (resp. $\textbf{m}$) is in display in each structure of s in which it occurs.

A labelled formula $\textbf{j}\le A$ (resp. $A \le \textbf{m}$) is in display in a sequent s if $\textbf{j}$ (resp. $\textbf{m}$) is in display in each structure of s in which it occurs.

A proof system enjoys the display property iff for every derivable sequent $s = \varGamma \vdash \varDelta$ and every structure $\sigma \in s$, the sequent s can be equivalently transformed, using the rules of the system, into a sequent $s'$ s.t. $\sigma$ occurs in display in $s'$ (in this case we might say that $\sigma$ is displayable).⁸

Definition 6 (Proper labelled calculi)

A proof system is a proper labelled calculus if it satisfies the following list of conditions:

C$_1$ : Preservation of Formulas. Each formula occurring in a premise of an inference r is a subformula of some formula in the conclusion of r.

C$_2$ : Shape-Alikeness of Parameters and Formulas/Terms in Congruent Structures. (i) Congruent parameters are occurrences of the same (meta-)structure (i.e. instantiations of structure metavariables in the application of a rule R except for switch rules); (ii) instantiations of labelled formulas in the application of switch rules (in the case of $\mathbf {A.L}\varSigma$, occurrences of the form $\textbf{j}\le C$ and $C \le \textbf{m}$) are congruent and the formulas in these occurrences instantiate the same formula metavariable (namely C); (iii) instantiations of pure structures in the application of switch rules (in the case of $\mathbf {A.L}\varSigma$, occurrences of the form $\textbf{j}\le \textbf{T}''$ and $\textbf{T}'' \le \textbf{m}$) are congruent and exactly one term in these occurrences instantiate the same term metavariable (namely $\textbf{T}''$).

C$_3$ : Non-proliferation of Parameters and Congruent Structures. (i) Each parameter in an inference r is congruent to at most one constituent in the conclusion of r. (ii) Each nonparametric structure in the instantiation r of a switch rule R is congruent to at most one nonparametric structure in the conclusion of r.

C$_4$ : Position-Alikeness of Parameters and Congruent Structures. Congruent parameters and congruent structures occur in the same position (i.e. either in precedent position or in succedent position) in their respective sequents.

C$_5$ : Display of Principal Constituents. If a labelled formula a is principal in the conclusion of an inference r, then a is in display.

C$'_5$ : Display-Invariance of Axioms and Structural Rules. If a structure $\sigma$ occurs in the conclusion s of a structural rule (where R is an axiom whenever the set of premises is empty), then either $\sigma$ occurs in display in s, or a structure $\sigma '$ and a sequent $s'$ exist s.t. $\sigma '$ is in display in $s'$, and $s'$ is derivable from s via application of switch and adjunction rules only, and $\sigma$ and $\sigma '$ are congruent in this derivation. Moreover, if the rule R is an axiom, then is an axiom of the calculus as well.

C$_6$ : Closure Under Substitution for Succedent Parts. Each rule is closed under simultaneous substitution of (sets of) arbitrary structures for congruent labelled formulas occurring in succedent position.

C$_7$ : Closure Under Substitution for Precedent Parts. Each rule is closed under simultaneous substitution of (sets of) arbitrary structures for congruent labelled formulas occurring in precedent position.

where $\overline{\sigma }$ is a multi-set of structures and $\overline{\sigma }/a$ means that $\overline{\sigma }$ are substituted for a.

This condition caters for the step in the cut-elimination procedure in which the cut needs to be “pushed up” over rules in which the cut-formula in succedent position is parametric.

C$_8$ : Eliminability of Matching Principal Constituents. This condition requests a standard Gentzen-style checking, which is now limited to the case in which both cut formulas are principal, i.e. each of them has been introduced with the last rule application of each corresponding subdeduction. In this case, analogously to the proof Gentzen-style, condition C$_8$ requires being able to transform the given deduction into a deduction with the same conclusion in which either the cut is eliminated altogether, or is transformed in one or more applications of the cut rule(s), involving proper subformulas of the original cut-formula.

We now provide the proof of Theorem 1 stated in Sect. 4.4.

Proof

The proof is close to the proofs in [12] and [22, Section 3.3, Appendix A]. As to the principal move (i.e. both labelled cut formulas are principal), condition C$_8$ guarantees that this cut application can be eliminated. As to the parametric moves (i.e. at least one labelled cut formula is parametric), we are in the following situation:

where we assume that the cut labelled formula a is parametric in the conclusion of $\pi _2$ (the other case is symmetric), and $(\varGamma \vdash \varDelta )[a]^{pre}$ (resp. $(\varPi \vdash \varSigma )[a]^{suc}$) means that a occur in precedent (resp. succedent) position in $\varGamma \vdash \varDelta$ (resp. $\varPi \vdash \varSigma$).

Conditions C$_2$-C$_4$ make it possible to follow the history of that occurrence of a, since these conditions enforce that the history takes the shape of a tree, of which we consider each leaf. Let $a_{u_i}$ (abbreviated to $a_u$ from now on) be one such uppermost-occurrence in the history-tree of the parametric cut term a occurring in $\pi _2$, and let $\pi _{2.i}$ be the subderivation ending in the sequent $\varGamma _i \vdash \varDelta _i$, in which $a_u$ is introduced.

Wansing’s parametric case (1) splits into two subcases: (1a) $a_u$ is introduced in display; (1b) $a_u$ is not introduced in display. Condition C$'_5$ guarantees that (1b) can only be the case when $a_u$ has been introduced via an axiom.

If (1a), then we can perform the following transformation:

where $\pi _2 \,[\{\varPi , \varSigma \} /a]$ is the derivation obtained by $\pi _2$ by substituting $\varPi , \varSigma$ for a in $\pi _2$.⁹ Notice that the assumption that a is parametric in the conclusion of $\pi _2$ and that $a_u$ is principal implies that $\pi _2$ has more than one node, and hence the transformation above results in a cut application of strictly lower height. Moreover, condition C$_7$ implies that Cut’ is well defined and the substitution of $\{\varPi , \varSigma \}$ for a in $\pi _2$ gives rise to an admissible derivation $\pi _2 \,[\{\varPi , \varSigma \}/a]^{pre}$ in the calculus (use C$_6$ for the symmetric case). If (1b), i.e. if $a_u$ is the principal formula of an axiom, the situation is illustrated below in the derivation on the left-hand side:

where $(\varGamma _i \vdash \varDelta _i) [a_u]^{pre}[a]^{suc}$ is an axiom. Then, condition C$'_5$ implies that some sequent $(\varGamma '_i \vdash \varDelta '_i) [a_u]^{pre}[a]^{suc}$ exists, which is display-equivalent to the first axiom, and in which $a_u$ occurs in display. This new sequent can be either identical to $(\varGamma _i \vdash \varDelta _i) [a_u]^{pre}[a]^{suc}$, in which case we proceed as in case (1a), or it can be different, in which case, condition C$'_5$ guarantees that it is an axiom as well. Further, if $\pi$ is the derivation consisting of applications of adjunction and switch rules which transform the latter axiom into the former, then let $\pi ' = \pi \,[\{\varPi ,\varSigma \}/a_u]$. As discussed when treating (1a), the assumptions imply that $\pi _2$ has more than one node, so the transformation described above results in a cut application of strictly lower height. Moreover, condition C$_7$ implies that Cut’ is well defined and substituting $\{\varPi , \varSigma \}$ for $a_u$ in $\pi _2$ and in $\pi$ gives rise to admissible derivations $\pi _2 \,[\{\varPi , \varSigma \}/a_u]$ and $\pi '$ in the calculus (use C$_6$ for the symmetric case).

As to Wansing’s case (2), assume that $a_u$ has been introduced as a parameter in the conclusion of $\pi _{2.i}$ by an application r of the rule R.

Therefore, the transformation below yields a derivation where $\pi _1$ is not used at all and the cut is not applied.

From this point on, the proof proceeds like in [22].