Non Normal Logics: Semantic Analysis and Proof Theory

Abstract

We introduce proper display calculi for basic monotonic modal logic, the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our proposal applies the multi-type methodology in the design of display calculi, starting from a semantic analysis based on the translation from monotonic modal logic to normal bi-modal logic.

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 third author.

Appendices

A Analytic Inductive Inequalities

In the present section, we specialize the definition of analytic inductive inequalities (cf. [20]) to the multi-type languages $\mathcal {L}_{MT\nabla }$ and $\mathcal {L}_{MT>}$ reported below.

An order-type over $n\in \mathbb {N}$ is an n-tuple $\epsilon \in \{1, \partial \}^n$. If $\epsilon$ is an order type, $\epsilon ^\partial$ is its opposite order type; i.e. $\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}_{\mathsf {S}}\cup \mathcal {F}_{\mathsf {N}}\cup \mathcal {F}_{\text {MT}}$ and $\mathcal {G}: = \mathcal {G}_{\mathsf {S}}\cup \mathcal {G}_{\mathsf {N}} \cup \mathcal {G}_{\text {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$).

Definition 8

(Signed Generation Tree). The positive (resp. negative) generation tree of any $\mathcal {L}_\text {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. −).

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

(Good branch). Nodes in signed generation trees will be called $\varDelta$-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 10

(Analytic inductive inequalities). For any order type $\epsilon$ and any irreflexive and transitive relation $<_\varOmega$ 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 $(\varOmega , \epsilon )$-inductive if

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

• 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 9), and

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

An inequality $s \le t$ is analytic $(\varOmega , \epsilon )$-inductive if the signed generation trees $+s$ and $-t$ are analytic $(\varOmega , \epsilon )$-inductive. An inequality $s \le t$ is analytic inductive if is analytic $(\varOmega , \epsilon )$-inductive for some $\varOmega$ and $\epsilon$.

B Algorithmic Proof of Theorem 1

In what follows, we show that the correspondence results collected in Theorem 1 can be retrieved as instances of a suitable multi-type version of algorithmic correspondence for normal logics (cf. [5, 6]), hinging on the usual order-theoretic properties of the algebraic interpretations of the logical connectives, while admitting nominal variables of two sorts. For the sake of enabling a swift translation into the language of m-frames and c-frames, we write nominals directly as singletons, and, abusing notation, we quantify over the elements defining these singletons. These computations also serve to prove that each analytic structural rule is sound on the heterogeneous perfect algebras validating its correspondent axiom. In the computations relative to each analytic axiom, the line marked with $(\star )$ marks the quasi-inequality that interprets the corresponding analytic rule. This computation does not prove the equivalence between the axiom and the rule, since the variables occurring in each starred quasi-inequality are restricted rather than arbitrary. However, the proof of soundness is completed by observing that all ALBA rules in the steps above the marked inequalities are (inverse) Ackermann and adjunction rules, and hence are sound also when arbitrary variables replace (co-)nominal variables.