Multi-type Display Calculus for Semi De Morgan Logic

Abstract

We introduce a proper multi-type display calculus for semi De Morgan logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Our proposal builds on an algebraic analysis of semi De Morgan algebras and applies the guidelines of the multi-type methodology in the design of display calculi.

A. Palmigiano—This research is supported 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.

Appendices

A Analytic Inductive Inequalities

In the present section, we specialize the definition of analytic inductive inequalities (cf. [11]) to the multi-type language $\mathcal {L}_\mathrm {MT}$, in the types $\textsf {DL}$ and $\textsf {DM}$, defined in Sect. 4 and reported below for the reader’s convenience.

$$\begin{aligned} \textsf {DL}\ni A \,{:}{:=}\,&\,p \mid \, e(\alpha ) \mid \top \mid \bot \mid A \wedge A \mid A \vee A \\ \textsf {DM}\ni \alpha \,{:}{:=}\,&\, h_1(A) \mid h_2(A) \mid 1 \mid 0 \mid {\sim } \alpha \mid \lnot \alpha \mid \alpha \cup \alpha \mid \alpha \cap \alpha \end{aligned}$$

We will make use of the following auxiliary definition: an order-type over $n\in \mathbb {N}$ is an n-tuple $\epsilon \in \{1, \partial \}^n$. For every order type $\epsilon$, we denote its opposite order type by $\epsilon ^\partial$, that is, $\epsilon ^\partial (i) = 1$ iff $\epsilon (i)=\partial$ for every $1 \le i \le n$. The connectives of the language above are grouped together into the families $\mathcal {F}: = \mathcal {F}_{\textsf {DL}}\cup \mathcal {F}_{\textsf {DM}}\cup \mathcal {F}_{\mathrm {MT}}$ and $\mathcal {G}: = \mathcal {G}_{\textsf {DL}}\cup \mathcal {G}_{\textsf {DM}} \cup \mathcal {G}_{\mathrm {MT}}$ defined as follows:

For any $f\in \mathcal {F}$ (resp. $g\in \mathcal {G}$), we let $n_f\in \mathbb {N}$ (resp. $n_g\in \mathbb {N}$) denote the arity of f (resp. g), and the order-type $\epsilon _f$ (resp. $\epsilon _g$) on $n_f$ (resp. $n_g$) indicate whether the ith coordinate of f (resp. g) is positive ($\epsilon _f(i) = 1$, $\epsilon _g(i) = 1$) or negative ($\epsilon _f(i) = \partial$, $\epsilon _g(i) = \partial$). The order-theoretic motivation for this partition is that the algebraic interpretations of $\mathcal {F}$-connectives (resp. $\mathcal {G}$-connectives), preserve finite joins (resp. meets) in each positive coordinate and reverse finite meets (resp. joins) in each negative coordinate.

For any term $s(p_1,\ldots p_n)$, any order type $\epsilon$ over n, and any $1 \le i \le n$, an $\epsilon$ -critical node in a signed generation tree of s is a leaf node $+p_i$ with $\epsilon (i) = 1$ or $-p_i$ with $\epsilon (i) = \partial$. An $\epsilon$-critical branch in the tree is a branch ending in an $\epsilon$-critical node. For any term $s(p_1,\ldots p_n)$ and any order type $\epsilon$ over n, we say that $+s$ (resp. $-s$) agrees with $\epsilon$, and write $\epsilon (+s)$ (resp. $\epsilon (-s)$), if every leaf in the signed generation tree of $+s$ (resp. $-s$) is $\epsilon$-critical. We will also write $+s'\prec *s$ (resp. $-s'\prec *s$) to indicate that the subterm $s'$ inherits the positive (resp. negative) sign from the signed generation tree $*s$. Finally, we will write $\epsilon (s') \prec *s$ (resp. $\epsilon ^\partial (s') \prec *s$) to indicate that the signed subtree $s'$, with the sign inherited from $*s$, agrees with $\epsilon$ (resp. with $\epsilon ^\partial$).

Definition 9

(Signed Generation Tree). The positive (resp. negative) generation tree of any $\mathcal {L}_\mathrm {MT}$-term s is defined by labelling the root node of the generation tree of s with the sign $+$ (resp. −), and then propagating the labelling on each remaining node as follows: For any node labelled with $\ell \in \mathcal {F}\cup \mathcal {G}$ of arity $n_\ell$, and for any $1\le i\le n_\ell$, assign the same (resp. the opposite) sign to its ith child node if $\epsilon _\ell (i) = 1$ (resp. if $\epsilon _\ell (i) = \partial$). Nodes in signed generation trees are positive (resp. negative) if are signed $+$ (resp. −).

Definition 10

(Good branch). Nodes in signed generation trees will be called $\Delta$ -adjoints, syntactically left residual (SLR), syntactically right residual (SRR), and syntactically right adjoint (SRA), according to the specification given in Table 1. A branch in a signed generation tree $*s$, with $*\in \{+, - \}$, is called a good branch if it is the concatenation of two paths $P_1$ and $P_2$, one of which may possibly be of length 0, such that $P_1$ is a path from the leaf consisting (apart from variable nodes) only of PIA-nodes⁹, and $P_2$ consists (apart from variable nodes) only of Skeleton-nodes.

Table 1. Skeleton and PIA nodes.

Definition 11

(Analytic inductive inequalities). For any order type $\epsilon$ and any irreflexive and transitive relation $<_\Omega$ on $p_1,\ldots p_n$, the signed generation tree $*s$ $(* \in \{-, + \})$ of an $\mathcal {L}_{MT}$ term $s(p_1,\ldots p_n)$ is analytic $(\Omega , \epsilon )$ -inductive if

• 1. every branch of $*s$ is good (cf. Definition 10);

• 2. for all $1 \le i \le n$, every SRR-node occurring in any $\epsilon$-critical branch with leaf $p_i$ is of the form $\circledast (s, \beta )$ or $\circledast (\beta , s)$, where the critical branch goes through $\beta$ and

  • (a) $\epsilon ^\partial (s) \prec *s$ (cf. discussion before Definition 10), and

  • (b) $p_k <_{\Omega } p_i$ for every $p_k$ occurring in s and for every $1\le k\le n$.

We will refer to $<_{\Omega }$ as the dependency order on the variables. An inequality $s \le t$ is analytic $(\Omega , \epsilon )$ -inductive if the signed generation trees $+s$ and $-t$ are analytic $(\Omega , \epsilon )$-inductive. An inequality $s \le t$ is analytic inductive if is analytic $(\Omega , \epsilon )$-inductive for some $\Omega$ and $\epsilon$.

In each setting in which they are defined, analytic inductive inequalities are a subclass of inductive inequalities (cf. [11]). In their turn, inductive inequalities are canonical (that is, preserved under canonical extensions, as defined in each setting).

B Completeness

Proposition 8

For every $A \in \mathrm {H.SDM}$, the sequent $A^{\tau } {\ \vdash \ }A_{\tau }$ is derivable in D.SDM.

Proof

By inducution on $A \in \mathcal {L}$. The proof of base cases: $A := \top$, $A := \bot$ and $A := p$, is straightforward, and is omitted.

Inductive cases: $A := B \wedge C$ and $A := B \vee C$ can be proved by the induction hypothesis and (w), (c), $(\vee )$ and $(\wedge )$ rules. As to $A := \lnot B$,

Proposition 9

For every $A, B \in \mathrm {H.SDM}$, if $A {\ \vdash \ }B$ is derivable in H.SDM, then $A^{\tau } {\ \vdash \ }B_{\tau }$ is derivable in D.SDM.

Proof

As page limited, we just show an example: .