Labelled Calculi for the Logics of Rough Concepts

Abstract

We introduce sound and complete labelled sequent calculi for the basic normal non-distributive modal logic $\textbf{L}$ and some of its axiomatic extensions, where the labels are atomic formulas of the first order language of enriched formal contexts, i.e., relational structures based on formal contexts which provide complete semantics for these logics. We also extend these calculi to provide a proof system for the logic of rough formal contexts.

Appendices

A Soundness of the Basic Calculus

Lemma 6

The basic calculus $\mathbf {R.L}$ is sound for the logic of enriched formal contexts.

Proof

The soundness of the axioms, cut rules and propositional rules is trivial from the definitions of satisfaction and refutation relation for enriched formal contexts. We now discuss the soundness for the other rules.

Adjunction rules. The soundness of the adjunction rules follows from the fact that $R_\blacksquare = R_\Diamond ^{-1}$, and .

Approximation rules. We only give proof for $approx_a$. The proof for $approx_x$ is similar. In what follows, we will refer to the objects (resp. features) occurring in $\varGamma$ and $\varDelta$ in the various rules with $\overline{d}$ (resp. $\overline{w}$).

Invertible rules for modal connectives. We only give proofs for $\Box _L$ and $\Box _R$. The proofs for $\Diamond _R$, $\Diamond _L$, $\rhd _R$, and $\rhd _L$ can be given in a similar manner.

The invertibility of the rule $\Box _L$ is obvious from the fact that the premise can be obtained from the conclusion by weakening.

Switch rules. Soundness of the rules Sxa and Sax follows from the fact that for any concepts $c_1$ and $c_2$ we have

$$\begin{aligned}{}[\![{c_1}]\!] \subseteq [\![{c_2}]\!] \quad \iff \quad (\![{c_2}]\!) \subseteq (\![{c_1}]\!). \end{aligned}$$

The soundness of all other switch rules follows from the definition of modal connectives and I-compatibility. As all the proofs are similar we only prove the soundness of S$a \Diamond x$ as a representative case. Soundness of other rules can be proved in an analogous manner.

Soundness of the axiomatic extensions considered in Sect. 3.2 is immediate from the Proposition 1.

B Syntactic completeness

As to the axioms and rules of the basic logic $\textbf{L}$, below, we only derive in $\mathbf {R.L}$ the axioms and rules encoding the fact that $\Diamond$ is a normal modal operator plus the axiom $p \ \,{\vdash }\ \,p \vee q$.

The syntactic completeness for the other axioms and rules of $\textbf{L}$ can be shown in a similar way. In particular, the admissibility of the substitution rule can be proved by induction in a standard manner.

We now consider the reflexivity axiom $p \ \,{\vdash }\ \,\Diamond p$ and the transitivity axiom $\Box p \ \,{\vdash }\ \,\Box \Box p$. The derivation for dual axioms $\Box p \ \,{\vdash }\ \,p$ and $\Diamond \Diamond p \ \,{\vdash }\ \,\Diamond p$ can be provided analogously.

Completeness for the other axiomatic extensions can be shown in a similar way.