Lattice Logic Properly Displayed

Abstract

We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.

This research has been funded by the NWO Vidi grant 016.138.314, the NWO Aspasia grant 015.008.054, and a Delft Technology Fellowship awarded to the second author in 2013.

1 Introduction

Lattice logic (i.e. the restriction of classical propositional logic to the $\{\wedge , \vee , \top , \bot \}$-fragment without distributivity) is the propositional base of many well known ‘lattice-based’ logics (e.g. the full Lambek calculus [31], bilattice logic [1], orthologic [35], linear logic [33]), and as such is hardly ever studied in isolation. An important question in structural proof theory concerns how to smoothly account for the transition between a given (lattice-based) logic and its axiomatic extensions and expansions [50, Chap. 1], [23, p. 352], [24, 27]. In the present paper, we introduce a calculus for lattice logic aimed at supporting this smooth transition for a class of lattice-based logics which is the widest so far.

Toward this goal, research in structural proof theory [24, 46, 50] has identified two general criteria: (a) all introduction rules for logical connectives are to have one and the same form; (b) the information on the distinctive features of each logical connective and on the interaction between connectives is to be encoded in structural rules satisfying certain requirements, captured by the notion of analiticity. These criteria are fulfilled, among others, by proper display calculi, a refinement of Belnap’s display calculi [2] introduced by Wansing [50]. However, in most calculi for lattice-based logics (cf. e.g. [47, 48]), including display calculi [3], the introduction rules for conjunction and disjunction have the so-called additive form, while those of the other connectives typically are in multiplicative form (see Sect. 2.2). More fundamentally, conjunction and disjunction do not have structural counterparts in these calculi. This non-standard treatment can be explained, in the setting of display calculi, by the following trade-off: introducing the structural counterparts of these connectives would require the addition of the display postulates in order to enforce the display property, which is key to the Belnap-style cut elimination metatheorem [2, 50]; however, the addition of display postulates would make it possible for the resulting calculus to derive the unwanted distributivity axioms as theorems. So, the need to block the derivation of distributivity is at the root of the non-standard design choice of having logical connectives without their structural counterpart (cf. [4]).

In the present paper, we introduce the proper display calculus D.LL for lattice logic which enjoys the full display property, and is such that all introduction rules have the same form (namely the multiplicative form). We succeed in circumventing the trade-off described above by introducing a richer language, with terms of different types. This solution applies the principles of a design for proof calculi (the multi-type display calculi) introduced in [25, 26, 28, 36] with the aim of displaying dynamic epistemic logic and propositional dynamic logic, then successfully applied to several other logics (such as linear logic with exponentials [39], inquisitive logic [29], semi De Morgan logic [34]) which are not properly displayable¹ in their single-type formulation, and has also served as a platform for the design of novel logics [5].

The main feature of D.LL is that it makes it possible to express the interactions between conjunction and disjunction and between them and other connectives at the structural level, by means of analytic structural rules. The remarkable property of these rules is that adding them to a given proper multi-type calculus preserves the package of basic properties of that calculus (soundness, completeness, conservativity, cut elimination and subformula property). This is all the more an advantage, because a uniform theory of analytic extensions of proper multi-type calculi is being developed thanks to the systematic connections established in [37] between proper display calculi and unified correspondence theory. These connections have made it possible to characterize the syntactic shape of axioms (the so-called analytic inductive axioms) which can be equivalently translated into analytic rules of a proper display calculus. Thus, the main feature of this calculus paves the way to the creation of the most comprehensive and modular proof theory of analytic extensions of lattice-based logics. The specific solution for lattice logic is justified semantically by Birkhoff’s representation theorem for complete lattices.

Structure of the Paper. In Sect. 2, we briefly report on a Hilbert-style presentation of lattice logic and its algebraic semantics, and discuss the issue of a modular account of its axiomatic extensions and expansions. In Sect. 3, we report on well known order-theoretic facts related with the representation of complete lattices, which help to introduce an equivalent multi-type semantic environment for lattice logic. In Sect. 4, we introduce the multi-type language naturally associated with the semantic environment of the previous section. In Sect. 5, we introduce the multi-type calculus D.LL for lattice logic which constitutes the core contribution of the present paper. In Sect. 6, we discuss the basic properties of D.LL (soundness, completeness, cut-elimination, subformula property, and conservativity). In Sect. B, we collect some derivations, and prove that (the translation of) the distributivity axiom is not derivable in D.LL.

2 Lattice Logic and Its Single-Type Proof Theory

2.1 Hilbert-Style Presentation of Lattice Logic and Its Algebraic Semantics

The language $\mathcal {L}$ of lattice logic over a set $\textsf {AtProp}$ of atomic propositions is so defined:

$A \,::= \,p \mid \top \mid \bot \mid A \wedge A \mid A \vee A.$

Lattice logic has the following Hilbert-style presentation:

where A[C / p] indicates that all occurrences of $p\in \textsf {AtProp}$ in A are replaced by C.

The algebraic semantics of lattice logic is given by the class of bounded lattices (cf. [6, 8]), i.e. (2, 2, 0, 0)-algebras $\mathbb {A} = (X, \wedge , \vee , \top , \bot )$ validating the following identities:

A bounded lattice is distributive if it validates the distributivity laws below. A bounded lattice is residuated (resp. dually residuated) if it validates the residuation law cR (resp. dR). If a lattice is (dually) residuated then is distributive (cf. [22, 31]).

2.2 Towards a Modular Proof Theory for Lattice Logic

To motivate the calculus introduced in Sect. 5, it is useful to discuss preliminarily the following Gentzen-style sequent calculus for lattice logic (cf. e.g. [49]):

• Identity and Cut rules

• Operational rules (where $i \in \{1,2\}$)

The calculus above, which we refer to as L0, is sound w.r.t. the class of lattices, complete w.r.t. the Hilbert-style presentation of lattice logic, and enjoys cut-elimination. Hence, L0 is perfectly adequate as a calculus for lattice logic, when this logic is regarded in isolation. However, as discussed in the introduction, the main interest of lattice logic lays in its serving as a base for its axiomatic extensions (cf. e.g. [40]) and language-expansions. Axiomatic extensions of lattice logic can be supported by L0 by adding suitable axioms. For instance, modular and distributive lattice logic can be respectively captured by adding the following axioms to L0:

However, cut elimination for the resulting calculi needs to be proved from scratch. More in general, we lack uniform principles or proof strategies aimed at identifying axioms which can be added to L0 so that cut elimination transfers to the resulting calculus. Another source of nonmodularity arises from the fact that L0 lacks structural rules. Indeed, the additive formulation of the introduction rules of L0 encodes the information which is stored in standard structural rules such as weakening, contraction, associativity, and exchange. Hence, L0 cannot be used as a base to capture logics aimed at ‘negotiating’ these rules, such as the Lambek calculus [41] and other substructural logics [31]. To remedy this, one can move to the following calculus L1, which fulfills the visibility property,² isolated by Sambin et al. in [47] to formulate a general strategy for cut elimination. Visibility generalizes Gentzen’s idea, realized in his calculus LJ, that intuitionistic logic could be captured by restricting the shape of sequents and admitting at most one formula in succedent position [32]. The calculus L1 has a structural language consisting of one structural constant ‘$\text {I}$’, interpreted as $\top$ (resp. $\bot$) when occurring in precedent (resp. succedent) position, and one binary connective ‘$\,,$’, interpreted as conjunction (resp. disjunction) in precedent (resp. succedent) position. The rules Exchange, Associativity, Weakening and Contraction are the usual ones and are not reported here.

• Identity and Cut rules

where $(Y {\ \vdash \ }Z)[A]^{pre}$ (resp. $(Y {\ \vdash \ }Z)[A]^{succ}$) indicates that the A occurs in precedent (resp. succedent) position in the sequent .

• Operational rules

Unlike the operational rules of L0 which are additive, the operational rules of L1 are multiplicative.³ The latter formulation is more general, and implies that weakening, exchange, associativity, and contraction are not anymore subsumed by the introduction rules.

The visibility of L1 blocks the derivation of the distributivity axiom. Hence, to be able to derive distributivity, one option is to relax the visibility constraint both in precedent and in succedent position. This solution is not entirely satisfactory, and suffers from the same lack of modularity which prevents Gentzen’s move from LJ to LK to capture intermediate logics. Specifically, relaxing visibility captures the logics of Sambin’s cube, but many other logics are left out. Moreover, without visibility, we do not have a uniform strategy for cut elimination.

To conclude, a proof theory for axiomatic extensions and expansions of general lattice logic is comparably not as modular as that of the axiomatic extensions and expansions of the logic of distributive lattices, which can rely on the theory of proper display calculi [37, 50]. The idea guiding the approach of the present paper, which we will elaborate upon in the next sections, is that, rather than trying to work our way up starting from a calculus for lattice logic, we will obtain a calculus for lattice logic from the standard proper display calculus for the logic of distributive lattices, by endowing it with a suitable mechanism to block the derivation of distributivity.

3 Multi-type Semantic Environment for Lattice Logic

In the present section, we introduce a class of heterogeneous algebras [7] which equivalently encodes complete lattices, and which will be useful to motivate the design of the calculus for lattice logic from a semantic viewpoint, as well as to establish its properties. This presentation takes its move from very well known facts in the representation theory of complete lattices, which can be found e.g. in [6, 22], formulated—however—in terms of covariant (rather than contravariant) adjunction. For every partial order $\mathbb {Q} = (Q, \le )$, we let $\mathbb {Q}^{op}: = (Q, \le ^{op})$, where $\le ^{op}$ denotes the converse ordering. If $\mathbb {Q} = (Q, \wedge , \vee , \bot , \top )$ is a lattice, we let $\mathbb {Q}^{op}: = (Q, \wedge ^{op}, \vee ^{op}, \bot ^{op}, \top ^{op})$ denote the lattice induced by $\le ^{op}$. Moreover, for any $b\in Q$, we let $b{\uparrow }: = \{c\mid c\in Q \text{ and } b\le c\}$ and $b{\downarrow }: = \{a\mid a\in Q \text{ and } a\le b\}$.

A polarity is a structure $\mathbb {P} = (X, Y, R)$ such that X and Y are sets and $R\subseteq X\times Y$. Every polarity induces a pair of maps $\rho : \mathcal {P}(Y)^{op}\rightarrow \mathcal {P}(X)$, $\lambda : \mathcal {P}(X)\rightarrow \mathcal {P}(Y)^{op}$, respectively defined by $Y'\mapsto \{x\in X\mid \forall y(y\in Y'\rightarrow xR y) \}$ and $X'\mapsto \{y\in Y\mid \forall x(x\in X'\rightarrow xR y) \}$. It is well known (cf. [22]) and easy to verify that these maps form an adjunction pair, that is, for any $X'\subseteq X$ and $Y'\subseteq Y$,

$$\begin{aligned} \lambda (X')\subseteq ^{op} Y'\quad \text{ iff } \quad X'\subseteq \rho (Y'). \end{aligned}$$

The map $\lambda$ is the left adjoint, and $\rho$ is the right adjoint of the pair. By general order-theoretic facts, this implies that $\lambda$ preserves arbitrary joins and $\rho$ arbitrary meets: that is, for any $S\subseteq \mathcal {P}(X)$ and any $T\subseteq \mathcal {P}(Y)$,

$$\begin{aligned} \lambda (\bigcup S) = \bigcup ^{op}_{s\in S}\lambda (s)\quad \text{ and } \quad \rho (\bigcap ^{op} T) = \bigcap _{t\in T} \rho (t). \end{aligned}$$

(1)

Other well known facts about adjoint pairs are that $\rho \lambda : \mathcal {P}(X)\rightarrow \mathcal {P}(X)$ is a closure operator and $\lambda \rho : \mathcal {P}(Y)^{op}\rightarrow \mathcal {P}(Y)^{op}$ an interior operator (cf. [22]). Moreover, $\lambda \rho \lambda = \lambda$, and $\rho \lambda \rho = \rho$ (cf. [22]). That is, $\lambda \rho$ restricted to $\textsf {Range}(\lambda )$ is the identity map, and likewise, $\rho \lambda$ restricted to $\textsf {Range}(\rho )$ is the identity map. Hence, $\textsf {Range}(\rho ) = \textsf {Range}(\rho \lambda )$, $\textsf {Range}(\lambda ) = \textsf {Range}(\lambda \rho )$ and

$$\begin{aligned} \mathcal {P}(X)\supseteq \textsf {Range}(\rho )\cong \textsf {Range}(\lambda )\subseteq \mathcal {P}(X)^{op}. \end{aligned}$$

Furthermore, $\rho \lambda$ being a closure operator on $\mathcal {P}(X)$ implies that $\textsf {Range}(\rho )= \textsf {Range}(\rho \lambda )$ is a complete sub $\bigcap$-semilattice of $\mathcal {P}(X)$ (cf. [22]), and hence $\mathbb {L} = \textsf {Range}(\rho )$ is endowed with a structure of complete lattice, by setting for every $S\subseteq \mathbb {L}$,

$$\begin{aligned} \bigwedge _{\mathbb {L}} S := \bigcap S\quad \text{ and } \quad \bigvee _{\mathbb {L}} S: = \rho \lambda (\bigcup S) \end{aligned}$$

(2)

Likewise, $\lambda \rho$ being an interior operator on $\mathcal {P}(Y)^{op}$ implies that $\textsf {Range}(\lambda )$ is a complete sub $\bigcup$-semilattice of $\mathcal {P}(Y)^{op}$, and hence $\mathbb {L} = \textsf {Range}(\lambda )$ is endowed with a structure of complete lattice, by setting

$$\begin{aligned} \bigvee _{\mathbb {L}} T := \bigcup ^{op} T\quad \text{ and } \quad \bigwedge _{\mathbb {L}} T: = \lambda \rho (\bigcap ^{op} T) \end{aligned}$$

(3)

for every $T\subseteq \mathbb {L}$. Finally, for any $S\subseteq \textsf {Range}(\rho )$,

and

which shows that the restriction of $\lambda$ to $\textsf {Range}(\rho )$ is a complete lattice homomorphism. Likewise, one can show that the restriction of $\rho$ to $\textsf {Range}(\lambda )$ is a complete lattice homomorphism, which completes the proof that the bijection

$$\begin{aligned} \mathcal {P}(X)\supseteq \textsf {Range}(\rho )\cong \textsf {Range}(\lambda )\subseteq \mathcal {P}(X)^{op} \end{aligned}$$

is an isomorphism of complete lattices, and justifies the abuse of notation which we made by denoting both the lattice $\textsf {Range}(\rho )$ and the lattice $\textsf {Range}(\lambda )$ by $\mathbb {L}$.

Conversely, for every complete lattice $\mathbb {L}$, consider the polarity $\mathbb {P}_{\mathbb {L}}: =(L, L, \le )$ where L is the universe of $\mathbb {L}$ and $\le$ is the lattice order. Then the maps $\lambda : \mathcal {P}(L)\rightarrow \mathcal {P}(L)^{op}$ and $\rho : \mathcal {P}(L)^{op}\rightarrow \mathcal {P}(L)$ are respectively defined by the assignments $S\mapsto \{a\in L\mid \forall b(b\in S\rightarrow b\le a) \} = (\bigvee S){\uparrow }$ and $T\mapsto \{a\in L\mid \forall b(b\in T\rightarrow a\le b) \} = (\bigwedge T){\downarrow }$ for all $S, T\subseteq L$. Since $\bigwedge ((\bigvee S){\uparrow }) = \bigvee S$ and $\bigvee ((\bigwedge T){\downarrow }) = \bigwedge T$, the closure operator $\rho \lambda : \mathcal {P}(L)\rightarrow \mathcal {P}(L)$ and the interior operator $\lambda \rho : \mathcal {P}(L)^{op}\rightarrow \mathcal {P}(L)^{op}$ are respectively defined by

$$\begin{aligned} S\mapsto (\bigvee S){\downarrow }\quad \text{ and } \quad T\mapsto (\bigwedge T){\uparrow }. \end{aligned}$$

(4)

The lattice $\mathbb {L}$ can be mapped injectively both into $\textsf {Range}(\rho ) = \textsf {Range}(\rho \lambda )$ and into $\textsf {Range}(\lambda ) = \textsf {Range}(\lambda \rho )$ by the assignments $a\mapsto a{\downarrow }$ and $a\mapsto a{\uparrow }$ respectively. Moreover, since $\mathbb {L}$ is complete, the maps defined by these assignments are also onto $\textsf {Range}(\rho \lambda )$ and $\textsf {Range}(\lambda \rho )$. Finally, for any $S\subseteq \mathbb {L}$,

which completes the verification that the map $\mathbb {L}\rightarrow \textsf {Range}(\rho )$ defined by the assignment $a\mapsto a{\downarrow }$ is a complete lattice isomorphism. Similarly, one verifies that the map $\mathbb {L}\rightarrow \textsf {Range}(\lambda )$ defined by the assignment $a\mapsto a{\uparrow }$ is a complete lattice isomorphism. The discussion so far can be summarized by the following.

Proposition 1

Any complete lattice $\mathbb {L}$ can be identified both with the lattice of closed sets of some closure operator $c: \mathbb {D}\rightarrow \mathbb {D}$ on a complete and completely distributive lattice $\mathbb {D} = (D, \cap , \cup , \wp , \varnothing )$, and with the lattice of open sets of some interior operator $i: \mathbb {E}\rightarrow \mathbb {E}$ on a complete and completely distributive lattice $\mathbb {E} = (E, \sqcap , \sqcup , \mathfrak {I}, \emptyset )$.

Hence, in what follows, $\mathbb {L}$ will be identified both with $\textsf {Range}(c)$ endowed with its structure of complete lattice defined as in (2) (replacing $\rho \lambda$ by c), and with $\textsf {Range}(i)$ endowed with its structure of complete lattice defined as in (3) (replacing $\lambda \rho$ by i). Taking these identifications into account, general order-theoretic facts (cf. [22, Chap. 7]) imply that $c = e_{\ell }\circ \gamma$, where $\gamma : \mathbb {D}\twoheadrightarrow \mathbb {L}$ is defined by $\alpha \mapsto c(\alpha )$ and $e_\ell : \mathbb {L}\hookrightarrow \mathbb {D}$ is the natural embedding, and moreover, these maps form an adjunction pair as follows: for any $a\in \mathbb {L}$ and any $\alpha \in \mathbb {D}$,

$$\begin{aligned} \gamma (\alpha )\le a\quad \text{ iff } \quad \alpha \le e_{\ell }(a), \end{aligned}$$

with the additional property that $\gamma \circ e_\ell = Id_{\mathbb {L}}$. Likewise, $i = e_{r}\circ \iota$, where $\iota : \mathbb {E}\twoheadrightarrow \mathbb {L}$ is defined by $\xi \mapsto i(\xi )$ and $e_r: \mathbb {L}\hookrightarrow \mathbb {E}$ is the natural embedding, and moreover, these maps form an adjunction pair as follows: for any $a\in \mathbb {L}$ and any $\xi \in \mathbb {E}$,

$$\begin{aligned} e_{r}(a)\le \xi \quad \text{ iff } \quad a\le \iota (\xi ), \end{aligned}$$

with the additional property that $\iota \circ e_r = Id_{\mathbb {L}}$.

Summing up, any complete lattice $\mathbb {L}$ can be associated with a heterogeneous LL-algebra, i.e.  a tuple $(\mathbb {L}, \mathbb {D}, \mathbb {E}, e_\ell , \gamma , e_r, \iota )$ such that:

• H1. $\mathbb {L} = (L, \le )$ is a bounded poset;⁴

• H2. $\mathbb {D}$ and $\mathbb {E}$ are complete and completely distributive lattices;

• H3. $\gamma : \mathbb {D}\rightarrow \mathbb {L}$ and $e_\ell : \mathbb {L}\rightarrow \mathbb {D}$ are such that $\gamma \dashv e_\ell$ and $\gamma \circ e_\ell = Id_{\mathbb {L}}$;

• H4. $\iota : \mathbb {E}\rightarrow \mathbb {L}$ and $e_r: \mathbb {L}\rightarrow \mathbb {E}$ are such that $e_r \dashv \iota$ and $\iota \circ e_r = Id_{\mathbb {L}}$.

Conversely, for any heterogeneous LL-algebra as above, the poset $\mathbb {L}$ can be endowed with the structure of a complete lattice inherited by being order-isomorphic both to the poset of closed sets of the closure operator $c: = \gamma \circ e_{\ell }$ on $\mathbb {D}$ and to the poset of open sets of the interior operator $i: = \iota \circ e_{r}$ on $\mathbb {E}$. Finally, no algebraic information is lost when presenting a complete lattice $\mathbb {L}$ as its associated heterogeneous LL-algebra. Indeed, the identification of $\mathbb {L}$ with $\textsf {Range}(c)$, endowed with the structure of complete lattice defined as in (2), implies that for all $a, b\in \mathbb {L}$,

$$\begin{aligned} a\vee b = \gamma (e_\ell (a)\cup e_\ell (b)). \end{aligned}$$

As discussed above, $e_\ell$ being a right adjoint and $\gamma$ a left adjoint imply that $e_\ell$ is completely meet-preserving and $\gamma$ completely join-preserving. Therefore, $e_\ell (\top ) = \wp$ and $\bot = \gamma (\varnothing )$. Moreover, $\gamma$ being both surjective and order-preserving implies that $\top = \gamma (\wp )$. Furthermore, for all $a, b\in \mathbb {L}$,

$$\begin{aligned} a\wedge b = \gamma \circ e_\ell (a\wedge b) = \gamma (e_\ell (a)\cap e_\ell (b)). \end{aligned}$$

Thus, the whole algebraic structure of $\mathbb {L}$ can be captured in terms of the algebraic structure of $\mathbb {D}$ and the adjoint maps $\gamma$ and $e_\ell$ as follows: for all $a, b\in \mathbb {L}$,

$$\begin{aligned} \bot = \gamma (\varnothing ) \quad \top = \gamma (\wp ) \quad a\vee b = \gamma (e_\ell (a)\cup e_\ell (b)) \quad a\wedge b = \gamma (e_\ell (a)\cap e_\ell (b)). \end{aligned}$$

(5)

Reasoning analogously, one can also capture the algebraic structure of $\mathbb {L}$ in terms of the algebraic structure of $\mathbb {E}$ and the adjoint maps $\iota$ and $e_r$ as follows: for all $a, b\in \mathbb {L}$,

$$\begin{aligned} \top = \iota (\mathfrak {I}) \quad \bot = \iota (\emptyset ) \quad a\wedge b = \iota (e_r(a)\sqcap e_r (b)) \quad a\vee b = \iota (e_r(a)\sqcup e_r (b)). \end{aligned}$$

(6)

4 Multi-type Language for Lattice Logic

In Sect. 3, heterogeneous LL-algebras have been introduced and shown to be equivalent presentations of complete lattices. The toggle between these mathematical structures is reflected in the toggle between the logical languages which are naturally interpreted in the two types of structures. Indeed, the heterogeneous LL-algebras of Sect. 3 provide a natural interpretation for the following multi-type language $\mathcal {L}_{\mathrm {MT}}$ over a set $\textsf {AtProp}$ of $\textsf {Lattice}$-type atomic propositions:

where $p\in \textsf {AtProp}$. The interpretation of $\mathcal {L}_{\mathrm {MT}}$-terms into heterogeneous LL-algebras is defined as the straightforward generalization of the interpretation of propositional languages in algebras of compatible signature. At the end of the previous section, we observed that the algebraic structure of the complete lattice $\mathbb {L}$ can be captured in terms of the algebraic structure of its associated heterogeneous LL-algebra. This observation serves as a base for the definition of the translations $(\cdot )^\ell , (\cdot )^r: \mathcal {L}\rightarrow \mathcal {L}_{\mathrm {MT}}$ between the original language $\mathcal {L}$ of lattice logic and $\mathcal {L}_{\mathrm {MT}}$:

For every complete lattice $\mathbb {L}$, let $\mathbb {L}^*$ denote its associated heterogeneous LL-algebra as defined in Sect. 3. The proof of the following proposition relies on the observations made at the end of Sect. 3.

Proposition 2

For all $\mathcal {L}$-formulas A and B and every complete lattice $\mathbb {L}$,

$$\begin{aligned} \mathbb {L}\models A\le B \quad \text{ iff } \quad \mathbb {L}^*\models A^\ell \le B^r. \end{aligned}$$

5 Proper Display Calculus for Lattice Logic

5.1 Language

The language of the calculus D.LL includes the types $\textsf {Lattice}$, $\textsf {Left}$, and $\textsf {Right}$, sometimes abbreviated as $\textsf {L}$, $\textsf {P}$, and $\textsf {P}^{\text {op}}$ respectively.

Our notational conventions assign different variables to different types. This allows us to drop the subscripts $^{\mathrm {op}}$, since the parsing of expressions such as $\bullet \Gamma$ and $\bullet \Pi$ is inherently unambiguous, and the parsing of e.g. $\circ X$ is contextually unambiguous.

• Structural and operational pure $\textsf {L}$-type connectives:⁵

• Structural and operational pure ${\textsf {P}}$-type and ${\textsf {P}}^{\text {op}}$-type connectives:

• Structural and operational multi-type connectives:

The connectives , , and are interpreted in heterogeneous LL-algebras as the maps $e_\ell$, $e_r$, $\gamma$, and $\iota$, respectively.

5.2 Rules

In what follows, structures of type $\textsf {L}$ are denoted by the variables X, Y, Z, and W; structures of type $\textsf {P}$ are denoted by the variables $\Gamma , \Delta , \Theta$, and $\Lambda$; structures of type $\textsf {P}^{\text {op}}$ are denoted by the variables $\Pi , \Sigma , \Psi$, and $\Omega$. Given the semantic environment introduced in Sect. 3, it will come as no surprise that there is a perfect match between the pure $\textsf {P}$-type rules and the pure $\textsf {P}^{\mathrm {op}}$-type rules. In order to achieve a more compact presentation of the calculus, in what follows we will also reserve the variables S, T, U, and V to denote either $\textsf {P}$-type structures or $\textsf {P}^{\text {op}}$-type structures, and s, t, u and v to denote operational terms of either $\textsf {P}$-type or $\textsf {P}^{\text {op}}$-type, with the proviso that they should be interpreted in the same type in the same pure type-rule.

• Multi-type display rules

• Pure $\textsf {P}$-type and $\textsf {P}^{\text {op}}$-type display rules

• Structural and operational pure $\textsf {P}$-type and $\textsf {P}^{\text {op}}$-type rules

• Structural and operational pure $\textsf {L}$-type rules

• Operational rules for multi-type connectives:

6 Properties

Soundness. First, structural symbols are interpreted as logical symbols according to their (precedent or succedent) position, as indicated in the tables of Sect. 5.1. Then, sequents are interpreted as inequalities, and rules as quasi-inequalities in heterogeneous LL-algebras. Rules of D.LL are sound if their corresponding quasi-inequalities are valid in heterogeneous LL-algebras. This verification is routine.

Conservativity. We need to show that, for all formulas A and B of the original language of lattice logic, if is a D.LL-derivable sequent, then is a theorem of the Hilbert-style presentation of lattice logic. The argument follows the standard proof strategy discussed in [36, 37], using the following facts: (a) the rules of D.LL are sound w.r.t. heterogeneous LL-algebras (cf. Sect. 6); (b) lattice logic is strongly complete w.r.t. the class of complete lattices, and (c) complete lattices are equivalently presented as heterogeneous LL-algebras (cf. Sect. 3), so that Proposition 2 holds.

Cut Elimination and Subformula Property. These can be inferred from the meta-theorem, in [26]; in [39, Theorem A.2] a restricted version of it is stated which specifically applies to proper multi-type display calculi (cf. [39, Definition A.1]). The verification is straightforward, and is omitted.

Completeness. First, we translate $\mathcal {L}$-sequents into D.LL-sequents , using the following translations:

Proposition 3

For every $A\in \mathcal {L}$, the multi-type sequent is derivable in D.LL.

Proof

By simultaneous induction on $A\in \textsf {L}$, $\alpha \in \textsf {P}$, and $\xi \in \textsf {P}^{{op}}$.

In what follows, we collect all the translations of the axioms involving conjunction,⁶ and derive some of them in D.LL (cf. Sect. A). The full set of derivations can be found in the extended version of the present paper [38]. All derivations are standard and make use only of Weakening, Contraction and Exchange as structural rules.

Appendices

A Completeness

In the cases of the Identity and Absorption laws a formula occurs in isolation on one side of the turnstile, therefore we need to proceed by cases according to the shape of A (we just show $A = C \wedge D$ and $A = \bot$, respectively).

B Distributivity Fails

We will show that all the paths in the backward proof-search of the translation of the distributivity axiom end in deadlocks. First, we apply exhaustively all invertible operational rules (modulo display rules):

There are no rules in which $\bullet$ and $\centerdot$ interact, hence we are reduced to either isolate

in precedent position by the backward application of a display rule, or isolate the following structure in succedent position:

We only treat the first case, the second being analogous. Once in isolation, we can act on X only via Exchange, Weakening or Residuation. In each case we reach a dead end:

• Case 1: (Exchange or) Residuation.

As an intermediate step, we can isolate any of the substructures of X via Residuation, or via Exchange and Residuation, as shown below. In each case we reach a dead end.

• Case 2: (Exchange or) Weakening.

As an intermediate step, we can try to isolate an immediate substructure of X by applying backward Weakening. By directly applying Weakening, we obtain

and by applying Exchange and Weakening, we obtain

Notice that the second subcase can be reduced to the first one as follows:

As to the proof of the first subcase, let us preliminarily perform the following steps:

Again, we are in a situation in which we can act on Y only via Exchange, Weakening or Residuation, and also in this case any option leads to a dead end. Indeed:

• Case 2.1: Exchange or Weakening. We can delete one of the immediate substructures of Y via Weakening or, respectively, Exchange and Weakening, obtaining

  

  In each case, we reach a dead end, as shown below:

  

• Case 2.2: Residuation. We can isolate any of the substructures of Y via Residuation, or via Exchange and Residuation. In each case we reach a dead end: