Labelled Calculi for Lattice-Based Modal Logics

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. 1.

   For any complete lattice L, any \(j\in L\) is completely join-irreducible if \(j\ne \bot \) and for any \(S\subseteq L\), if \(j = \bigvee S\) then \(j\in S\). Dually, any \(m\in L\) is completely meet-irreducible if \(m\ne \top \) and for any \(S\subseteq L\), if \(m = \bigwedge S\) then \(m\in S\).

2. 2.

   The unary operations \(\blacksquare ^{\mathbb {A}^\delta }\) and on \(\mathbb {A}^\delta \) are the unique maps satisfying the equivalences \(\Diamond ^\sigma u\le v\) iff \(u\le \blacksquare ^{\mathbb {A}^\delta }v\) and iff \(u\le \Box ^\pi v\) for all \(u, v\in \mathbb {A}^\delta \).

3. 3.

   By the general theory of unified correspondence (cf. [7]), this is the case of every subset \(\varSigma \) of the set of axioms listed at the end of Sect. 2.1.

4. 4.

   Therefore, every instantiation of a labelled formula (resp. a pure structure) occurring in \(R \in \mathbf {A.L}\) is nonparametric. For instance, \(\textbf{j}\le p\) is nonparametric in Id\(_{\textbf{j}\le p}\), and \(A \le \textbf{m}, \textbf{j}\le \Box A, \textbf{j}\le \Box \textbf{m}\) are all nonparametric in \(\Box _P\). Moreover, according to Definition 1, every instantiation of a structure (resp. a labelled formula) in the conclusion of initial rules (resp. logical rules) is principal. For instance, \(\textbf{j}\le p\) is principal in Id\(_{\textbf{j}\le p}\) and \(\textbf{j}\le \Box A\) is principal in \(\Box _P\).

5. 5.

   For instance, given an instantiation r of the rule \(\wedge _S\), assuming \(\sigma \in \varGamma \) in the first (resp. second) premise of r, then it occurs in the same position in the conclusion of r, and these two occurrences of \(\sigma \) are locally congruent in r. Nonetheless, notice that the two occurrences of \(\sigma \) in the premises of r are not locally congruent in r.

6. 6.

   That is, we show that, for any \(\mathcal {L}\)-axiom \(s = A\vdash B \in \{\)(T), (4), (B), (D), (C)\(\}\), a derivation exists in \(\mathbf {A.L}\{s\}\) of the sequent \(\textbf{j}\le A\vdash \textbf{j}\le B\), or equivalently of \(B\le \textbf{m}\vdash A\le \textbf{m}\).

7. 7.

   Given the result in Lemma 1, notice that this is the same as saying that all occurrences of \(\textbf{j}\) (resp. \(\textbf{m}\)) are eliminated, except in the case of cut rules, which have two premises. But, if the cut formula has a \(\textbf{j}\)-twin (resp. \(\textbf{m}\)-twin) in \(\varGamma \) in the one premise and in \(\varDelta '\) in the other, the conclusion \(\varGamma ,\varGamma '\ \,{\vdash }\ \,\varDelta ,\varDelta '\) will still have the \(\textbf{j}\)-twin (resp. \(\textbf{m}\)-twin) property.

8. 8.

   Notice that we are not requiring that every meta-structure is displayable.

9. 9.

   Notice that the writing \(\pi _2 \,[\{\varPi , \varSigma \} /a]\) does not mean that \(\varPi \) and \(\varSigma \) remain untouched in \(\pi _2\), namely it does not mean that every sequent in \(\pi _2\) is of the form \(\varPi , \varGamma '' \vdash \varSigma , \varDelta ''\) for some \(\varGamma '', \varDelta ''\). Indeed, structures in \(\varPi \) or in \(\varSigma \) might play the role of active structures in some applications of switch rules occurring in \(\pi _2\), if any.

Authors and Affiliations

1. School of Business and Economics, Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

   Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, Krishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere

2. Department of Mathematics and Applied Mathematics, University of Johannesburg, Johannesburg, South Africa

   Alessandra Palmigiano

3. Department of Mathematical Sciences, Stellenbosch University, Stellenbosch, South Africa

   Ineke van der Berg

Corresponding author

Correspondence to Giuseppe Greco .

Editors and Affiliations

1. Indian Institute of Technology Kanpur, Kanpur, India

   Mohua Banerjee

2. Indian Institute of Technology Goa, Ponda, India

   A. V. Sreejith

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).^{Footnote 8}

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\).^{Footnote 9} 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].

Reprints and permissions

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics