1 Introduction↩︎

Refutation calculi are formal systems which derive the invalid formulas of a given logic [1]. Starting with Lukasiewicz’s work [2], refutation calculi for various logics have been developed using different proof-theoretic formats, including Hilbert-style calculi [3], [4], Gentzen style sequent calculi [4], [5] and hypersequent calculi [6]. In this paper, we investigate refutation calculi based on display calculi.

Display calculi, introduced by Belnap [7], are deductive systems dealing with sequents \(\Pi \vdash \Sigma\) where \(\Pi\) and \(\Sigma\) are structures, i.e. syntactic objects inductively defined from formulas using so-called structural connectives. The rules that govern the interaction between these connectives ensure that any substructure of any sequent \(\Pi \vdash \Sigma\) can always be displayed, either only in precedent position or only in succedent position.

Display calculi have been applied to give cut-free presentations of many non-classical logics, including modal and substructural ones [8], [9]. In this paper, we focus on proper display calculi for the family of basic LE-logics, i.e. the logics canonically associated with basic normal lattice expansions of any signature [10]–[12]. Rather than employing display calculi in the usual role of proof construction, we investigate how they can be adapted for generating refutations – i.e., derivations of invalid sequents, or antisequents.

Specifically, we introduce refutation display calculi \(\mathrm{D.LE^{r}}\) for basic normal LE-logics. Starting from initial antisequents, these calculi derive new antisequents through the application of display rules, structural rules, and logical introduction rules. We establish soundness and completeness of each \(\mathrm{D.LE^{r}}\) calculus exploiting proof-analysis results on derivable sequents. Hence, we define inverse refutation systems for LE-logics by taking the contrapositive forms of the rules of \(\mathrm{D.LE^{r}}\) calculi. The resulting systems are terminating tableaux calculi for basic LE-logics: if a sequent is valid, then some branch exists in its tableau tree such that all the sequents at its terminal node are valid.

1.0.0.1 Structure of the paper.

Section 2 contains preliminaries on basic \(\mathrm{LE}\)-logics and their proper display calculi. In Section 3, we define the refutation display calculi \(\mathrm{D.LE^{r}}\). In Section 4, we prove that \(\mathrm{D.LE^{r}}\) calculi are sound and complete, and how consequently basic \(\mathrm{LE}\)-logics are syntactically decidable. In Section 5, we define tableaux systems for \(\mathrm{LE}\)-logics based on \(\mathrm{D.LE^{r}}\). We sketch directions for future research in Section 6.

2 Preliminaries↩︎

The present section adapts material from [13].

2.0.0.1 Basic normal \(\mathrm{LE}\)-logics.

Our basic language is an unspecified but fixed language \(\mathcal{L}_\mathrm{LE}\), to be interpreted over lattice expansions of compatible similarity type. This setting uniformly accounts for many well known logical systems, such as the basic orthomodular logic [14], the logic of the non-distributive de Morgan algebras [15], the full Lambek calculus [16] and the full Lambek-Grishin calculus [17], [18].

We use the following auxiliary definition: an order-type over \(n\in \mathbb{N}\) is an \(n\)-tuple \(\varepsilon\in \{1, \partial\}^n\). For every order-type \(\varepsilon\), we let \(\varepsilon^\partial\) denote its opposite order-type, that is, \(\;\varepsilon^\partial (i) = 1\) if and only if \(\varepsilon(i)=\partial\) for every \(1 \leq i \leq n\). The language \(\mathcal{L}_\mathrm{LE}(\mathcal{F}, \mathcal{G})\) (from now on abbreviated as \(\mathcal{L}_\mathrm{LE}\)) takes as parameters: a denumerable set of proposition letters \(\mathsf{AtProp}\), elements of which are denoted \(p,q,r\), possibly with indexes, and disjoint sets of connectives \(\mathcal{F}\) and \(\mathcal{G}\).¹ Each \(f\in \mathcal{F}\) and \(g\in \mathcal{G}\) has arity \(n_f\in \mathbb{N}\) (resp. \(n_g\in \mathbb{N}\)) and is associated with some order-type \(\varepsilon_f\) over \(n_f\) (resp. \(\varepsilon_g\) over \(n_g\)). The terms (formulas) of \(\mathcal{L}_\mathrm{LE}\) are defined recursively as follows: \[\varphi \coloncolonequals p \mid \bot \mid \top \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid f(\varphi_1, \ldots, \varphi_{n_f}) \mid g(\varphi_1, \ldots, \varphi_{n_g})\] where \(p \in \mathsf{AtProp}\), \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\). Terms in \(\mathcal{L}_\mathrm{LE}\) are denoted either by \(A,B,C\), or by lowercase Greek letters such as \(\varphi, \psi, \gamma\).

In the remainder of the paper, we extend the \(\{1,\partial\}\)-notation to the symbols \(\vee,\wedge,\bot,\top,\le,\vdash\) by stipulating that the superscript \(^1\) denotes the identity map, that \(\varphi\vdash^\partial \psi\) stands for \(\psi\vdash \varphi\), and defining \[\vee^\partial=\wedge,\qquad \wedge^\partial=\vee,\qquad \bot^\partial=\top,\qquad \top^\partial=\bot,\qquad {\le^\partial}={\ge}.\]

Henceforth, the adjective ‘normal’ referred to LEs will typically be dropped. In what follows, for every \(k \in \mathcal{F} \cup \mathcal{G}\) we let \(k(\overline{\varphi})[\psi]_i\) indicate that \(\psi\) occurs in the \(i\)-th coordinate of the vector of arguments \(\overline{\varphi}\).

The generic LE-logic is not equivalent to a sentential logic. Hence, the consequence relation of these logics needs to be captured in terms of sequents, motivating the following definition:

2.0.0.2 The fully residuated language \(\mathcal{L}_\mathrm{LE}^*\).

Any language \(\mathcal{L}_\mathrm{LE} = \mathcal{L}_\mathrm{LE}(\mathcal{F}, \mathcal{G})\) can be associated with the language \(\mathcal{L}_\mathrm{LE}^* = \mathcal{L}_\mathrm{LE}(\mathcal{F}^*, \mathcal{G}^*)\), where \(\mathcal{F}^*\supseteq \mathcal{F}\) and \(\mathcal{G}^*\supseteq \mathcal{G}\) are obtained by expanding \(\mathcal{L}_\mathrm{LE}\) with:

1. an \(n_f\)-ary connective \(f^\sharp_i\) for \(1 \leq i \leq n_f\), interpreted as the right residual of \(f\in\mathcal{F}\) in its \(i\)th coordinate if \(\varepsilon_{f}(i) = 1\) (resp. its Galois-adjoint if \(\varepsilon_{f}(i) = \partial\));

2. an \(n_g\)-ary connective \(g^\flat_i\) for \(1 \leq i \leq n_g\), interpreted as the left residual of \(g\in\mathcal{G}\) in its \(i\)th coordinate if \(\varepsilon_{g}(i) = 1\) (resp. its Galois-adjoint if \(\varepsilon_{g}(i) = \partial\)).

We let \(f^\sharp_i\in\mathcal{G}^*\) if \(\varepsilon_{f}(i) = 1\), and \(f^\sharp_i\in\mathcal{F}^*\) if \(\varepsilon_{f}(i) = \partial\). Dually, \(g^\flat_i\in\mathcal{F}^*\) if \(\varepsilon_{g}(i) = 1\), and \(g^\flat_i\in\mathcal{G}^*\) if \(\varepsilon_{g}(i) = \partial\). The order-type of additional connectives agrees with that of their intended interpretations. That is, for any \(f\in \mathcal{F}\) and \(g\in\mathcal{G}\),

• \(\varepsilon_{f_i^\sharp}(i) = \varepsilon_{f}(i)\) and \(\varepsilon_{f_i^\sharp}(j) = \varepsilon_{f}(j) \cdot \varepsilon_{f}^\partial(i)\) for any \(j\neq i\),

• \(\varepsilon_{g_i^\flat}(i) = \varepsilon_{g}(i)\) and \(\varepsilon_{g_i^\flat}(j) = \varepsilon_{g}(j) \cdot \varepsilon_{g}^\partial(i)\) for any \(j\neq i\).

where the product between \(1\) and \(\partial\) is isomorphic to the restriction of the product on integers to \(\{1, -1\}\). For instance, if \(f\) and \(g\) are binary connectives such that \(\varepsilon_f = (1, \partial)\) and \(\varepsilon_g = (\partial, 1)\), then \(\varepsilon_{f^\sharp_1} = (1, 1)\), \(\varepsilon_{f^\sharp_2} = (1, \partial)\), \(\varepsilon_{g^\flat_1} = (\partial, 1)\) and \(\varepsilon_{g^\flat_2} = (1, 1)\).²

2.0.0.3 Display calculi for basic normal LE-logics.

Let \(\mathcal{L} = \mathcal{L} (\mathcal{F}, \mathcal{G})\) be a fixed but arbitrary LE-signature. Let \(S_{\mathcal{F}} \colonequals\{\hat{f}\mid f\in \mathcal{F}^*\}\) and \(S_{\mathcal{G}}\colonequals\{\check{g}\mid g\in \mathcal{G}^*\}\) be the sets of structural connectives associated with \(\mathcal{F}^*\) and \(\mathcal{G}^*\) respectively.³ Each structural connective inherits the arity and order-type of its associated operational connective in \(\mathcal{F}^*\) and \(\mathcal{G}^*\).

For convenience, we set \(\mathcal{F}^\partial:=\mathcal{G}\) and \(\mathcal{G}^\partial:=\mathcal{F}\), and for any order-type \(\varepsilon\) on \(n\), we let \(\mathsf{Str}_\mathcal{F}^{\varepsilon} : = \prod_{i = 1}^{n}\mathsf{Str}_{\mathcal{F}^{\varepsilon(i)}}\) and \(\mathsf{Str}_\mathcal{G}^{\varepsilon} : = \prod_{i = 1}^{n}\mathsf{Str}_{\mathcal{G}^{\varepsilon(i)}}\), where the sets \(\mathsf{Str}_\mathcal{F}\) (resp. \(\mathsf{Str}_\mathcal{G}\)) of precedent (resp. succedent) structures are defined recursively as follows:

with \(\varphi\in \mathcal{L}_\mathrm{LE}\), and \(\hat{f}\in S_{\mathcal{F}}\), \(\check{g}\in S_{\mathcal{G}}\), \(\overline{\Pi}^{(\varepsilon_f)}\in \mathsf{Str}_\mathcal{F}^{\varepsilon_f}\) and \(\overline{\Sigma}^{(\varepsilon_g)} \in \mathsf{Str}_\mathcal{G}^{\varepsilon_g}\).

In what follows, we use \(\Upsilon_1, \ldots, \Upsilon_n\) as structure metavariables in \(\mathsf{Str} \mathrel{\vcenter{:}}= \mathsf{Str}_\mathcal{F} \cup \mathsf{Str}_\mathcal{G}\). The introduction rules of the calculus below ensures that \(\Upsilon \in \mathsf{Str}_\mathcal{F}\) (resp. \(\Upsilon \in \mathsf{Str}_\mathcal{G}\)) whenever it occurs in precedent (resp. succedent) position. The calculus \(\mathrm{D.LE} = \mathrm{D.LE}_{\mathcal{L}}\) manipulates sequents \(\Pi \vdash \Sigma\), and consists of the following rules:

• Identity and cut rules:

• Display postulates for \(f\in \mathcal{F}\) and \(g\in \mathcal{G}\): for any \(1\leq i,j\leq n_f\) and \(1\leq h,k\leq n_g\),

 

• If \(\varepsilon_{f}(i) = 1\) and \(\varepsilon_{g}(h) = 1\),

• If \(\varepsilon_{f}(j) = \partial\) and \(\varepsilon_{g}(k) = \partial\),

The structural connectives of the form \(\hat{f}^{\,\sharp}\) and \(\check{g}^{\,\flat}\) are referred to as residuals.

• Structural rules for lattice connectives:

• Logical introduction rules for lattice connectives:

• Logical introduction rules for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

If \(f\) and \(g\) are \(0\)-ary (i.e. they are constants), the rules \(f_R\) and \(g_L\) above reduce to the axioms (aka \(0\)-ary rules) \(\hat{f}{\ \vdash\ }f\) and \(g {\ \vdash\ }\check{g}\).

The calculus \(\mathrm{D.LE}\) is sound and complete w.r.t. the class of complete \(\mathcal{L}\)-algebras [13].⁴

Moreover, it is a proper display calculus (cf. [11]), and hence cut elimination holds for it as a consequence of a Belnap-style cut elimination metatheorem (cf. [11] and [19]).

3 Refutation display calculi for LE-logics↩︎

The refutation calculus D.LE\(^r\) manipulates antisequents – i.e., syntactic objects of the form \(\Pi\nvdash \Sigma\), where \(\Pi\in \mathsf{Str}_\mathcal{F}^{\varepsilon}\) and \(\Sigma\in \mathsf{Str}_\mathcal{G}^{\varepsilon}\). Intuitively, an antisequent \(\Pi\nvdash \Sigma\) is derivable if and only if the sequent \(\Pi\vdash\Sigma\) is invalid.⁷ In what follows, we list the rules of D.LE\(^r\) using the same notational conventions introduced in the previous section, with the addition that \(\varphi\nvdash^\partial \psi\) stands for \(\psi \nvdash \varphi\), and \(\check{\bot}^\partial = \hat{\top}\) and \(\hat{\top}^\partial = \check{\bot}\).

• Axiomatic rules:

• Display rules for \(f\in \mathcal{F}\) and \(g\in \mathcal{G}\): for any \(1\leq i \leq n_f\) and \(1\leq j \leq n_g\),

 

• if \(\varepsilon_{f}(i) = 1\) and \(\varepsilon_{g}(j) = 1\),

• if \(\varepsilon_{f}(i) = \partial\) and \(\varepsilon_{g}(j) = \partial\),

• Structural rules\(^\ast\) for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

\(^\ast\)Side condition: in each rule above, the endsequent should not contain residuals.

• Logical introduction rules\(^{\ast\ast}\) for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

Where \(j\) in \(f_R\) (resp. \(g_L\)) is some index in \(\{1,\ldots,n_f\}\) (resp. \(\{1,\ldots,n_g\}\)).

\(^{\ast\ast}\)Side condition: \(f_{1}\not=f_{2}\) and \(g_{1}\not=g_{2}\). Furthermore, we require that the endsequents of the rules \(f_R\), \(f^\neq_R\), \(g_L\), and \(g^\neq_L\) not contain residuals.

• Logical introduction rules\(^{\ast\ast\ast}\) for lattice connectives:

\(^{\ast\ast\ast}\)Side condition: \(\Pi'\) and \(\Sigma'\) are not branching (see Definition 3). Furthermore, we require that the endsequents of the rules \(\wedge_L\) and \(\vee_R\) not contain residuals.

4 Soundness and completeness of the refutation calculus↩︎

Let the complexity of a sequent be defined as the number of logical connectives plus the number of connectives (both logical and structural) plus twice the number of propositional atoms.

In what follows, we write \(\Upsilon[\Upsilon']\) to indicate that \(\Upsilon'\) is a substructure of \(\Upsilon\). When \(\Upsilon\) occurs in an (anti)sequent \(S\), we write \(\Upsilon[\Upsilon']^{pre}\) (resp. \(\Upsilon[\Upsilon']^{suc}\)) to indicate that \(\Upsilon'\) is a substructure of \(\Upsilon\) and occurs in precedent (respectively, succedent) position, that is, \(S\) is display-equivalent to some (anti)sequent \(S'\) (notation: \(S\equiv S'\)) in which \(\Upsilon\) is the sole structure on the left-hand (respectively, right-hand) side of \(\vdash\) or of \(\nvdash\). The symbol \(\Upsilon[\Upsilon''/\Upsilon']\) denotes the substitution of \(\Upsilon''\) for the substructure \(\Upsilon'\) within \(\Upsilon\).

We preliminarily recall that if \(\Pi\vdash\Sigma\equiv \Pi'\vdash\Sigma'\) then one of the following cases occurs:

For axiomatic rules, it suffices to consider an interpretation \(v\) such that \(v(p)=\top\) and \(v(q)=\bot\). For display postulates, reasoning by contraposition (both top-down and bottom-up) is sufficient. For \(0\)-ary introduction rules for \(f\) and \(g\) it is enough to take \(v\) such that \(v(g(\overline{\psi})) = \top\) and \(v(f(\overline{\psi})) = \bot\) for all input \(\overline{\psi}\). The soundness of \(f_L\) and \(g_R\) follows contrapositively from the fact that the following rules are derivable in D.LE:

A similar argument proves the soundness of \(\top_L\) and \(\bot_R\). As for the soundness of \(\wedge_{R_i}\) and \(\vee_{L_i}\), it is enough to notice that for all elements \(a,b,c\) of an arbitrary lattice, \(a\nleq b\) implies both \(a \nleq b \wedge c\) and \(a \vee c \nleq b\). Now, to prove the soundness of \(\hat{f}\check{\bot}\):

we argue contrapositively, by induction on the complexity of \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\), that if \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) is cut-free derivable, then \(\Upsilon_i \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) is derivable for some \(i\). Since \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) is not display-equivalent to any initial sequent, it must either result from a logical rule or from \(\top_W\) or \(\bot_W\), modulo application of display postulates. We analyze each case. Case \(\wedge_{L_i}\). Assume that \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) contains a conjunction \(A_1 \wedge A_2\) in precedent position, and suppose \(A_1\wedge A_2\) is the principal formula in the last (non-display) rule applied in the derivation of \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\). For some structure \(\Sigma[\check{\bot}]\), we have:

where, above and throughout this section, the dashed line stands for a finite number of applications of display postulates and \(A_i \vdash \Sigma[\check{\bot}] \equiv \hat{f}(\overline{\Upsilon})[A_i/A_1\wedge A_2]^{suc} \vdash \check{\bot}\) is derivable. By inductive hypothesis, \(\Upsilon_j[A_i/A_1\wedge A_2]^{pre} \vdash^{\varepsilon_f(j)} \check{\bot}^{\varepsilon_f(j)}\) is derivable for some \(j\). If \(A_1\wedge A_2\) is not present in \(\Upsilon_j\), then \(\Upsilon_j[A_i/A_1\wedge A_2] = \Upsilon_j\) and there is nothing else to prove. Otherwise, for some structure \(\Sigma'\) we have

Since \(\Upsilon_j[A_1\wedge A_2/A_1\wedge A_2]^{pre} = \Upsilon_j\), we are done.

Cases \(\vee_{R_i}\), \(f_L\), \(g_R\), \(\top_L\), and \(\bot_R\) are analogous to the previous case and therefore omitted. In all of them except \(\vee_R\), we apply the inductive hypothesis relying on the fact that the complexity decreases whenever a logical connective becomes structural.

Case \(\wedge_R\). Assume the structure \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) contains a conjunction \(A \wedge B\) in succedent position, and \(A\wedge B\) is the principal formula in the last logical rule (modulo display postulates) applied in the derivation of \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\). For some structure \(\Pi\), we have

where \(\Pi \vdash A \equiv \hat{f}(\overline{\Upsilon})[A/A\wedge B]^{suc} \vdash \check{\bot}\) and \(\Pi \vdash B \equiv \hat{f}(\overline{\Upsilon})[B/A\wedge B]^{suc} \vdash \check{\bot}\) are derivable. We apply the inductive hypothesis twice to obtain \(\Upsilon_i[A/A\wedge B]^{suc} \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) and \(\Upsilon_j[B/A\wedge B]^{suc} \vdash^{\varepsilon_f(j)} \check{\bot}^{\varepsilon_f(j)}\) for some \(i\) and \(j\). The only nontrivial case is when \(i=j\) and \(\Upsilon_i\) contains the aforementioned instance of \(A\wedge B\). In this scenario, for some structure \(\Sigma'\),

which proves the statement. The case \(\vee_L\) is analogous to \(\wedge_R\) and is therefore omitted.

Cases \(f_R\) and \(g_L\) are excluded by virtue of the side condition of \(\hat{f}\check{\bot}\).

Case \(\bot_W\). Assume that for some structures \(\Pi\) and \(\Sigma\) the sequent \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) is derived as follows, where \(\Pi \vdash \check{\bot}\) is a derivable sequent.

We need to consider four cases. In Case 1 , \(\Sigma[\check{\bot}]\) and \(\hat{f}(\overline{\Upsilon})[\Pi]\), assume that \(\Pi\) is different from \(\hat{f}(\overline{\Upsilon})\) (otherwise \(\bot_W\) is applied vacuously), i.e. \(\Upsilon_i[\Pi]\) for some \(i\). Hence, \(\Upsilon_i \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)} \equiv \Pi \vdash \Sigma'\) for some \(\Sigma'\), and the following derivation establishes our thesis:

Case 2 where \(\check{\bot}[\Sigma]\) and \(\Pi[\hat{f}(\overline{\Upsilon})]\) is trivial, as the premise coincides with the endsequent. Case 3 in which \(\check{\bot}[\Pi]\) and \(\Sigma[\hat{f}(\overline{\Upsilon})]\) cannot arise: \(\Pi\) (\(\Sigma\)) is in precedent (resp., succedent) position and display rules preserve structure positions. Finally, as to Case 4 , if \(\Pi[\check{\bot}]\) and \(\hat{f}(\overline{\Upsilon})[\Sigma]\), i.e. \(\Pi \vdash \check{\bot}\equiv \hat{f}(\overline{\Upsilon})[\check{\bot}/\Sigma]^{suc} \vdash \check{\bot}\) and \(\Upsilon_j[\Sigma]\) for some \(j\), then \(\Sigma\) must be different from an instance of \(\check{\bot}\) (if not, rule \(\bot_W\) would have been applied vacuously), hence \(\Sigma\) has a higher complexity than \(\check{\bot}\). Hence, the inductive hypothesis yields \(\Upsilon_i[\check{\bot}/\Sigma]^{suc} \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) for some \(i\). If \(i\neq j\) then \(\Upsilon_i[\Sigma]\) does not hold, so the substitution is vacuous and there is nothing else to prove; if \(i = j\), then for some \(\Pi'\in \mathsf{Str}_{\mathcal{F}}\),

where the active instance of \(\check{\bot}\) in the rule \(\bot_W\) is the instance of \(\check{\bot}\) that substitutes \(\Sigma\) in the previous proof section.

Case \(\top_W\) is similar to the previous case and is therefore omitted.

The proofs of the soundness of \(\hat{f}p\) and \(f^\neq_R\) closely mirror that of \(\hat{f}\check{\bot}\), except in the \(\bot_W\) case with \(\Pi[\hat{f}(\overline{\Upsilon})]\), illustrated below.

In both cases, we rely on the soundness of \(\hat{f}\check{\bot}\). To prove the soundness of \(f_R\) contrapositively, we must show that if \(\hat{f}(\overline{\Upsilon}) \vdash f(\overline{\varphi})\) is derivable, then either \(\Upsilon_i \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) holds for some \(i\), or \(\Upsilon_j \vdash^{\varepsilon_f(i)} \varphi_j\) for all \(j\). The proof parallels that for \(\hat{f}p\) and \(f^\neq_R\), with the added case where the last rule in the derivation of \(\hat{f}(\overline{\Upsilon}) \vdash f(\overline{\varphi})\) is

If that is the case, then clearly \(\Upsilon_j \vdash^{\varepsilon_f(i)} \varphi_j\) is derivable for all \(j\), as desired. The proofs of the soundness of \(\hat{\top}\check{g}\), \(p\check{g}\), \(g^\neq_L\), \(g_L\), and \(\hat{f}\check{g}\) are analogous to the cases above.

Finally, a similar argument proves the soundness of the rules \(\wedge_L\) and \(\vee_R\), but with fewer cases to consider, due to their side conditions: if \(\varphi \wedge \psi \vdash \Sigma'\) (resp. \(\Pi' \vdash \varphi \vee \psi\)) is derivable, then the last non-display rule applied cannot be \(\vee_L\) or \(\wedge_R\).

By induction on the complexity of the sequent \(\Pi \vdash \Sigma\), considering all cases.

If \(\Pi \mathrel{\vcenter{:}}= \bot\) or \(\Sigma \mathrel{\vcenter{:}}= \top\), the conclusion holds vacuously.

If \(\Pi \vdash \Sigma\equiv \Pi' \vdash A \wedge B\), either \(\Pi' \vdash A\) or \(\Pi' \vdash B\) is not derivable. If (say) \(\Pi' \vdash A \equiv (\Pi \vdash \Sigma)[A/A\wedge B]^{suc}\) is not derivable, by inductive hypothesis we get \(\Pi \nvdash \Sigma[A/A\wedge B]^{suc}\). Via display postulates we obtain \(\Pi' \nvdash A\), and thus \(\Pi' \nvdash A \wedge B\). Hence, we apply the display postulates to get \(\Pi \nvdash \Sigma\). The case in which \(\Pi \vdash \Sigma\equiv A \vee B \vdash \Sigma'\) is analogous.

If \(\Pi\vdash\Sigma\equiv f(\overline{\varphi})\vdash\Sigma'\), then \(\hat{f}(\overline{\varphi})\vdash\Sigma' \equiv (\Pi\vdash \Sigma)[\hat{f}(\overline{\varphi})/f(\overline{\varphi})]^{pre}\) is not derivable, and by inductive hypothesis we get \(\hat{f}(\overline{\varphi})\nvdash\Sigma'\). We apply \(f_L\) and display postulates to get \(\Pi\nvdash\Sigma\). The cases in which \(\Pi\vdash\Sigma\) is display-equivalent either to \(\Pi'\vdash g(\overline{\varphi})\), \(\Pi'\vdash\bot\), or \(\top \vdash \Sigma'\), are analogous.

Given the previous cases, we assume that \(\Pi \vdash \Sigma\) is non-branching and displays no \(f \in \mathcal{F}\) or \(\top\) (resp. \(g \in \mathcal{G}\) or \(\bot\)) in precedent (resp. succedent) position. Let us treat the case of \(\Sigma \mathrel{\vcenter{:}}= \check{\bot}\) (the case of \(\Pi\mathrel{\vcenter{:}}=\hat{\top}\) is analogous) and consider the possible subcases.

– If \(\Pi \mathrel{\vcenter{:}}= \hat{\top}\), \(\Pi \mathrel{\vcenter{:}}= p\), and \(\Pi \mathrel{\vcenter{:}}= g(\overline{\varphi})\), then \(\Pi \nvdash \Sigma\) is derivable via \(\mathrm{Ax}1\), \(\mathrm{Ax}2\), and \(g \check{\bot}\), respectively.

– \(\Pi \mathrel{\vcenter{:}}= \hat{f}(\overline{\Upsilon})\). By assumption, \(\hat{f}(\Upsilon_1,\ldots,\Upsilon_{n_f})\vdash \check{\bot}\) is not derivable. Let \(\upsilon_i\in \mathcal{L}\) be the operational counterpart of \(\Upsilon_i\) for every \(i\) in \(\{1,\ldots,n_f\}\) (\(\upsilon_i\) exists since \(\Upsilon_i\) does not contain residuals). Hence, \(\hat{f}(\overline{\Upsilon})\vdash f(\overline{\upsilon})\) is derivable and, for every \(\Sigma'\), if \(\Upsilon_i\vdash\Sigma'\) is derivable, so is \(\upsilon_i\vdash\Sigma'\). We claim that \(\Upsilon_i \vdash^{\varepsilon_f(i)}\check{\bot}^{\varepsilon_f(i)}\) is not derivable, for any \(1\leq i\leq n_{f}\). Assume the contrary, and, w.l.o.g., that \(i=1\) and \(\varepsilon_f(1)=1\) (the other cases being analogous). Then we can derive \(\hat{f}(\Upsilon_1,\ldots,\Upsilon_{n_f})\vdash \check{\bot}\) as follows, against our assumption.

Hence, no sequent \(\Upsilon_i \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) is derivable: then, by inductive hypothesis, \(\Upsilon_i \nvdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\), for any \(1\leq i\leq n_{f}\). Finally, we apply \(\bot_{f}\) to derive \(\Pi \nvdash \Sigma\).

– \(\Pi \mathrel{\vcenter{:}}= A \wedge B\). If \(A \wedge B \vdash \check{\bot}\) is not derivable, then neither of \(A \vdash \check{\bot}\) and \(B \vdash \check{\bot}\) are. Then by inductive hypothesis, \(A \nvdash \check{\bot}\) and \(B \nvdash \check{\bot}\), and an application of \(\wedge_L\) yields \(A \wedge B \nvdash \check{\bot}\).

Next, we assume that \(\Sigma \mathrel{\vcenter{:}}= p\) (the case of \(\Pi \mathrel{\vcenter{:}}= p\) is similar) and distinguish such subcases.

– \(\Pi \mathrel{\vcenter{:}}= q \neq p\) and \(\Pi \mathrel{\vcenter{:}}= g(\overline{\varphi})\). The antisequent \(\Pi \nvdash \Sigma\) is derivable via \(\mathrm{Ax}4\) and \(g p\), respectively.

– \(\Pi \mathrel{\vcenter{:}}= \hat{f}(\overline{\Upsilon})\) and \(\Pi \mathrel{\vcenter{:}}= A \wedge B\). Similar to the subcases \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) and \(A \wedge B \vdash \check{\bot}\) above.

Let us now assume that \(\Sigma \mathrel{\vcenter{:}}= f(\overline{\varphi})\) (the case in which \(\Pi \mathrel{\vcenter{:}}= g(\overline{\varphi})\) is analogous).

– \(\Pi \mathrel{\vcenter{:}}= g(\overline{\varphi'})\). The antisequent \(\Pi \nvdash \Sigma\) is derivable via the initial rule \(g f\).

– \(\Pi \mathrel{\vcenter{:}}= \hat{f'}(\overline{\Upsilon})\) with \(f' \neq f\). Similar to the subcase \(\hat{f}(\Upsilon) \vdash \check{\bot}\) analyzed above.

– \(\Pi \mathrel{\vcenter{:}}= \hat{f}(\overline{\Upsilon})\). As in the previous \(\hat{f}(\Upsilon_1,\ldots,\Upsilon_{n_f})\vdash \check{\bot}\) case, if \(\Pi\vdash\Sigma\) is not derivable, then \(\Upsilon_i \vdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) is not derivable for all \(i\) in \(\{1,\ldots,n_f\}\). Moreover, for some \(j\), the sequent \(\Upsilon_j \vdash^{\varepsilon_f(j)} \varphi_j\) is also not derivable, for otherwise one would get \(\hat{f}(\Upsilon_1,\ldots,\Upsilon_{n_f})\vdash f(\varphi_1, \ldots, \varphi_{n_{f}})\) as shown below:

By the inductive hypothesis, we conclude \(\Upsilon_i \nvdash^{\varepsilon_f(i)} \check{\bot}^{\varepsilon_f(i)}\) and \(\Upsilon_j \nvdash^{\varepsilon_f(j)} \varphi_j\) for all \(j\) and some \(i\), yielding \(\Pi \nvdash \Sigma\) via \(f_R\).

– \(\Pi \mathrel{\vcenter{:}}= A \wedge B\). Similar to the subcase \(A\wedge B \vdash \check{\bot}\) analyzed above.

Now, suppose that \(\Sigma \mathrel{\vcenter{:}}= A \vee B\) (the case in which \(\Pi\mathrel{\vcenter{:}}= A\wedge B\) is analogous).

– \(\Pi \mathrel{\vcenter{:}}= \hat{f}(\overline{\Upsilon})[C_i\wedge D_i]^{pre}_{i\in I}[C'_j\vee D'_j]^{suc}_{j\in J}\). None of the sequents \[\hat{f}(\overline{\Upsilon}) \vdash A,\quad \hat{f}(\overline{\Upsilon}) \vdash B,\quad \hat{f}(\overline{\Upsilon})[C_i]^{pre}_i \vdash A \vee B,\quad \hat{f}(\overline{\Upsilon})[D_i]^{pre}_i \vdash A \vee B,\] \[\hat{f}(\overline{\Upsilon})[C'_j]^{suc}_j \vdash A \vee B,\quad \hat{f}(\overline{\Upsilon})[D'_j]^{suc}_j \vdash A \vee B,\] are derivable for all \(i \in I\) and \(j \in J\), for otherwise, one would be able to derive \(\hat{f}(\overline{\Upsilon}) \vdash A \vee B\) applying the appropriate lattice rules modulo zero or more display postulates. By inductive hypothesis, all the sequents \[\hat{f}(\overline{\Upsilon}) \nvdash A,\quad \hat{f}(\overline{\Upsilon}) \nvdash B,\quad \hat{f}(\overline{\Upsilon})[C_i]^{pre}_i \nvdash A \vee B,\quad \hat{f}(\overline{\Upsilon})[D_i]^{pre}_i \nvdash A \vee B,\] \[\hat{f}(\overline{\Upsilon})[C'_j]^{suc}_j \nvdash A \vee B,\quad \hat{f}(\overline{\Upsilon})[D'_j]^{suc}_j\nvdash A \vee B,\] are derivable for all \(i\in I\) and \(j \in J\), thus we get \(\hat{f}(\overline{\Upsilon}) \nvdash A \vee B\) via the rule \(\vee_R\).

– \(\Pi \mathrel{\vcenter{:}}= C \wedge D\). This subcase is similar to the previous one.

Finally, if \(\Pi \vdash \Sigma\) is \(\hat{f}(\Upsilon_{1},\ldots,\Upsilon_{n_f})\vdash\check{g}\, (\Upsilon'_1,\ldots, \Upsilon'_{n_g})\), we proceed as in the case of \(\hat{f}(\overline{\Upsilon}) \vdash \check{\bot}\) to get the conclusion.

The first part is immediate from Theorem 2 and the completeness of D.LE. As to the second part, for any pair of structures \(\Pi,\Sigma\) without residuals, completeness of D.LE and Theorem 2 ensure that either \(\Pi\vdash\Sigma\) is derivable in \(\mathrm{D.LE}\) or \(\Pi\nvdash\Sigma\) in \(\mathrm{D.LE^{r}}\). The thesis follows from the observation that \(\mathbf{L}_{\mathrm{LE}}\)-sequents do not contain residuals.

5 Tableaux for LE-logics↩︎

In this section, we define tableaux rules for LE-logics by considering contrapositive versions of \(\mathrm{D.LE}^r\) rules. A refutation in the tableaux presentation of the calculus is a rooted graph where every node is labelled with a sequent, the root is labelled with the sequent to be refuted, and each other node is introduced using a rule of the calculus.⁸ As usual in the case of tableaux, if two nodes are introduced in different branches in the conclusion of a rule, then the reading is disjunctive; if two nodes are introduced on the same branch in the conclusion of a rule, then the reading is conjunctive.⁹

• Display rules\(^{\star}\) for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

\(^{\star}\)Notational convention: \(1\leq i\leq n_{f}\), \(1\leq j\leq n_{g}\). Furthermore, \(\mathring{f}^{\,\sharp}_{i}\) (resp. \(\mathring{g}^{\,\flat}_{i}\)) is \(\check{f}^{\,\sharp}_{i}\) (resp. \(\hat{g}^{\,\flat}\)) if \(\varepsilon_{f}(i) = 1\), and \(\hat{f}^{\,\sharp}_{i}\) (resp. \(\check{g}^{\,\flat}\)) otherwise.

\(^{\star}\)Side condition: any residuation rule can be applied if the conclusion has not been obtained by some previous rule application.

• Structural rules\(^{*}\) for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

\(^{*}\)Side condition: in each rule above, the premise should not contain residuals.

• Logical rules\(^{**}\) for \(f\in\mathcal{F}\) and \(g\in\mathcal{G}\):

\(^{**}\)Side condition: \(f_{1}\not=f_{2}\) and \(g_{1}\not=g_{2}\), and the premises of all the other rules above should not contain residuals.

• Rules\(^{***}\) for lattice connectives:

\(^{***}\)Notational convention: \(I=\{1,\ldots,m\}\) and \(J=\{1,\ldots,n\}\). Furthermore, \(k\) ranges in \(\{1,2\}\) (meaning that the last two rules above create \(2m +2n +2\) new branches).

\(^{***}\)Side condition: \(\Pi'\) and \(\Sigma'\) are not branching, and \(\varphi_{1} \wedge \varphi_{2} \vdash \Sigma'[A_{1i}\wedge A_{2i}]_{i\in I}^{pre}[B_{1j}\vee B_{2j}]_{j\in J}^{suc}\) and \(\Pi'[A_{1i}\wedge A_{2i}]_{i\in I}^{pre}[B_{1j}\vee B_{2j}]_{j\in J}^{suc} \vdash \varphi_{1}\vee\varphi_{2}\) do not contain residuals.

A branch of a tableau tree is terminated if for any sequent \(\Pi'\vdash\Sigma'\) belonging to a node along the branch, no tableau rule can be applied to \(\Pi'\vdash\Sigma'\) without generating a sequent that already occurs in the branch. A tableau tree is terminated if and only if each of its branches is terminated.

We say that a terminated branch is open whenever it contains (at least) one sequent of one of the following forms: \[\hat{\top}\vdash \check{\bot}\quad p \vdash \check{\bot}\quad \hat{\top}\vdash q \quad p \vdash q\] \[g(\overline{\psi}) \vdash \check{\bot}\quad g(\overline{\psi}) \vdash p \quad g(\overline{\psi}) \vdash f(\overline{\varphi}) \quad p\vdash f(\overline{\psi}) \quad \hat{\top}\vdash f(\overline{\psi})\] A terminated branch is closed if it is not open. We say that a terminated tableau tree is closed exactly when it has (at least) one closed branch, and open otherwise.

For any tableau rule different from a residuation one, the number of connectives in each conclusion is lower than the number of connectives in the premise. Moreover, each sequent has finitely many display-equivalent sequents, and the side condition on the applicability of display rules prevents cycles. Hence, for any sequent \(\Pi\vdash\Sigma\), there exists (at least) one terminated tableau tree. We leverage Theorem 1 and Corollary 1 to complete the proof.

6 Conclusions↩︎

This work opens several directions for future research in the study of refutation display calculi. Starting from LE-logics appears to be a promising first step, given their general semantic framework. It would also be valuable to extend the current platform to refutation display calculi for distributive LE-logics. Moreover, a broader perspective might involve addressing axiomatic extensions of LE-logics, potentially through the use of hybrid refutation rules that incorporate both sequents and antisequents.

The main technical motivation for employing display calculi stems from the metatheorem in [7], which establishes sufficient conditions under which a sequent calculus admits Gentzen-style cut elimination. In systems that include both sequents and antisequents, it becomes possible to define anticut rules – that is, contrapositive analogues of the standard cut rule [20]. It would be intriguing to determine whether sufficient conditions can be specified to support a uniform set of transformation steps enabling anticut elimination.

References↩︎

---

1. The assumption that the sets \(\mathcal{F}\) and \(\mathcal{G}\) are disjoint does not harm generality. For those connectives whose order-theoretic properties make them belong to both \(\mathcal{F}\) and \(\mathcal{G}\) (this is the case e.g. of the Boolean negation \(\neg\)), we can define two copies \(\neg_\mathcal{F}\in\mathcal{F}\) and \(\neg_\mathcal{G}\in\mathcal{G}\), and introduce structural rules which encode the fact that these two copies coincide.↩︎

2. This notation depends on the choice of the primitive connective and must be carefully adapted to well-known cases. For instance, the ‘fusion’ connective \(\circ\) (which, when denoted as \(f\), is such that \(\varepsilon_f = (1, 1)\)) has residuals \(f_1^\sharp\) and \(f_2^\sharp\), usually written as \(/\) and \(\backslash\) respectively. However, if \(\backslash\) is taken as the primitive \(g\), then \(g_2^\flat\) is \(\circ = f\), and \(g_1^\flat(x_1, x_2): = x_2/x_1 = f_1^\sharp (x_2, x_1)\). This example shows that, when identifying \(g_1^\flat\) and \(f_1^\sharp\), the conventional order of the coordinates is not preserved and depends on the chosen primitive.↩︎

3. For any connective \(h\) of arity \(n \geq 1\), the symbol \(\hat{h}\) (resp. \(\check{h}\)) conveys the information that \(h\) is a left (resp. right) adjoint/residual.↩︎

4. A complete \(\mathcal{L}\)-algebra is a complete lattice endowed with \(n_f\)-ary (resp. \(n_g\)-ary) operations \(f\) (resp. \(g\)) for each \(f\in \mathcal{F}\) (resp. \(g\in \mathcal{G}\)) which are completely join-preserving (resp. meet-preserving) in any coordinate \(i\) s.t. \(\varepsilon_f(i) = 1\) (resp. \(\varepsilon_g(i) = 1\)), and completely meet-reversing (resp. join-reversing) in any coordinate \(i\) s.t. \(\varepsilon_f(i) = \partial\) (resp. \(\varepsilon_g(i) = \partial\)). By well known order theoretic facts, complete algebras are also completely residuated, that is, the residuals \(f^\sharp_i\) and \(g^\flat_h\) exist for any \(f\in \mathcal{F}\) and \(g\in\mathcal{G}\) in each coordinate.↩︎

5. The definition of branching sequents captures non-definite inequalities in [10]; the difference is that, here, both structural and operational connectives are considered. Hence, every branching sequent is equivalent to a set of non-branching ones (cf. [10]).↩︎

6. In the context of a sequent \(\Pi\vdash \Sigma\), the signed generation trees of \(\Pi\) and \(\Sigma\) are defined by assigning \(+\) (resp. \(-\)) to the root of the generation tree of \(\Pi\) (resp. \(\Sigma\)), and then propagating the sign according to the order-type of both structural and operational connectives in the generation trees of \(\Pi\) and \(\Sigma\) and of the formulas therein: a child-node corresponding to a coordinate of the parent node of order-type \(1\) (resp. \(\partial\)) inherits the same sign as (resp. opposite sign to) the sign of the parent node.↩︎

7. In writing antisequents, we employ \(\nvdash\) rather than the standard \(\dashv\) to avoid a clash of notation with the symbol denoting adjunction.↩︎

8. We opted to directly manipulate sequents rather than (labelled) formulas, since this presentation is more compact and facilitates the comparison with the sequent calculus \(\mathrm{D.LE}^r\).↩︎

9. Notice that the conclusion of each display rule depends on the order type of the \(i\)-th (resp. \(j\)-th) coordinate, therefore each rule is a shorthand for two rules.↩︎