Labelled Calculi for the Logics of Rough Concepts

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.

1. 1.

   When \(B=\{a\}\) (resp. \(Y=\{x\}\)) we write \(a^{\uparrow \downarrow }\) for \(\{a\}^{\uparrow \downarrow }\) (resp. \(x^{\downarrow \uparrow }\) for \(\{x\}^{\downarrow \uparrow }\)).

2. 2.

   These compositions and those defined in Sect. 2.2 are pairwise different, since each of them involves different types of relations. However, the types of the relations involved in each definition provides a unique reading of such compositions, which justifies our abuse of notation.

3. 3.

   Notice that E being I-compatible does not imply that \(S_{{\!\Box }}\) is. Let \(\mathbb {G} = (\mathbb {P}, E)\) s.t.  \(A: = \{a, b\}\), \(X: = \{x, y\}\), \(I: = \{(a, x), (a, y), (b, y)\}\), and \(E: = A\times A\). Then E is I-compatible. However, \(S_{{\!\Box }}= \{(a, y), (b, y)\}\) is not, as \(S_{{\!\Box }}^{(0)}[x] = \varnothing \) is not Galois stable, since \(\varnothing ^{\uparrow \downarrow } = X^{\downarrow } = \{a\}\). In [10], it was remarked that \(S_{{\!\Box }}\) being I-compatible does not imply that E is.

4. 4.

   The symbols and denotes a meta-linguistic conjunction and a disjunction, respectively.

5. 5.

   And also \([\![{A}]\!]_V\subseteq I^{0}[(\![{A}]\!)_V]\) holds in both the cases: the one where \([\![{A}]\!]\) is the extension of an arbitrary set of features, and when \((\![{A}]\!)\) is the intension of \([\![{A}]\!]\).

Authors and Affiliations

1. School of Business and Economics, Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

   Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, Krishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere

2. Department of Mathematics and Applied Mathematics, University of Johannesburg, Johannesburg, South Africa

   Alessandra Palmigiano

3. Department of Mathematical Sciences, Stellenbosch University, Stellenbosch, South Africa

   Ineke van der Berg

Corresponding author

Correspondence to Krishna B. Manoorkar .

Editors and Affiliations

1. Indian Institute of Technology Kanpur, Kanpur, India

   Mohua Banerjee

2. Indian Institute of Technology Goa, Ponda, India

   A. V. Sreejith

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

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.

Reprints and permissions

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics