Indiscernibility and complementarity relations in information systems

Stéphane Demri Ewa Orłowska Dimiter Vakarelov

Abstract

We present logical systems for an analysis of data that have the form of descriptions of some objects of an application domain in terms of their attributes. We analyse two types of relationships among objects referred to as indiscernibility and complementarity. We present a modal logic LIC for reasoning about indiscernibility, complementarity and relationships between them. We define a Kripke-style semantics for LIC as well as semantics determined by information systems. We present a sound and complete deduction system for LIC. We also investigate the complexity of the satisfiability problem for LIC.

Contents

1 Introduction 2

2 Information systems 2

3 Indiscernibility and complementarity derived from an information system 3

4 Frames with indiscernibility and complementarity 3

5 Applications of indiscernibility and complementarity 4

6 First-order characterization of IC-frames 5

7 The information logic LIC for indiscernibility and complementarity 8

8 Completeness of the logic LIC 9

9 Complexity of the satisfiability problem for LIC 11

1 Introduction

We present logical systems for an analysis of data that have the form of descriptions of some objects of an application domain in terms of their attributes. We analyse two types of relationships among objects referred to as indiscernibility and complementarity. Each of them separetely has been extensively studied in the literature (e.g. [Vak90, DO97, DO99]), but until now no formal attempt has been made toward a theory of interconnections between indiscernibility and complementarity. In this paper we concentrate on developing logical tools for dealing with problems that involve both indiscernibility and complementarity. Intuitively, the objects having the same description are indiscernible and the objects whose descriptions are complements of each other are complementary. We present a modal logic LIC for reasoning about indiscernibility, complementarity and relationships between them. We define a Kripke-style semantics for LIC as well as semantics determined by information systems. We present a sound and complete deduction system for LIC. We also investigate the complexity of the satisfiability problem for LIC. We briefly mention applications that require the computation of both indiscernibility and complementarity.

We dedicate this paper to Johan van Benthem. His important results on modal logics, their methodology and applications have been a source of inspiration for us.

2 Information systems

For algorithmic reasons information about objects is often presented in the form of a table. The rows of the table are labelled with objects, the columns are labelled with attributes, and the entries of the table are collections of sets of values of attributes. Formally, an information system is a structure of the form

⟨OB, AT, {V AL_{a} : a ∈ AT }, f⟩

where OB is a nonempty set of objects, AT is a nonempty set of attributes, V AL_{a} is a nonempty set of values of the attribute a and f is a total function OB×AT → P(⋃_{a∈AT} V al_{a}) such that for any ⟨x, a⟩ ∈ OB×AT, f(x, a) ⊆ V al_{a}. We shall also use the more concise notation ⟨OB, AT ⟩ for ⟨OB, AT, {V AL_{a} : a ∈ AT }, f⟩. An information system ⟨OB, AT ⟩ is total [resp. deterministic] ⇔^{def} for any a ∈ AT and for any x ∈ OB, f(x, a) ≠ ∅ [resp. card(f(x, a)) ≤ 1]. Consider a simple example [DO98]:

colour  size  d
x_{1}  green  small yes
x_{2} not green small yes
x_{3}  blue  medium no

The notion of a set-theoretical information system introduced in [Vak87] plays an important role in the developments of this paper. Let ⟨W, V ⟩ be a pair such that W is a non-empty set and V included in P(P(W)) is a non-empty set of families of subsets of W such that all elements of V are non-empty. We define the set-theoretical information system S = ⟨OB, AT ⟩ under ⟨W, V ⟩ as follows:

• OB =^{def} W;

• AT =^{def} {a^{X} : X ∈ V } such that a^{X} : W → P(P(W)) and for any x ∈ OB

a^{X}(x) =^{def} {Y : Y ∈ V, x ∈ Y }. So V AL_{a^{X}} = X for X ∈ V;

• for any x ∈ OB and for any a^{X} ∈ AT, f(x, a^{X}) =^{def} a^{X}(x).

Any set-theoretical information system ⟨OB, AT ⟩ under ⟨W, V ⟩ is sometime abusively denoted by ⟨W, V ⟩ itself.

3 Indiscernibility and complementarity derived from an information system

Let S = ⟨OB, AT ⟩ be an information system and A be a subset of AT. We define families of indiscernibility relations ≡_{A} and complementarity relations R_{A} on the set OB as follows: for all objects x, y ∈ OB

• x ≡_{A} y ⇔^{def} for all a ∈ A, f(x, a) = f(y, a);

• xR_{A}y ⇔^{def} for all a ∈ A, f(x, a) = V AL_{a} \ f(y, a).

If A = {a} is a singleton, we write ≡_{a} and R_{a}, respectively. If A = AT, we often write ≡_{S} and R_{S}, respectively. Sometimes, when this will not cause a confusion, we will omit the subscript S in the above relations.

Lemma 3.1. Let S = ⟨W, V ⟩ be a set-theoretical information system.

(I) x ≡_{S} y iff for all a ∈ V, for all v ∈ a, x ∈ v iff y ∈ v; (II) xR_{S}y iff for all a ∈ V, for all v ∈ a, x ∈ v iff y ∉ v; (III) S is deterministic iff for all x ∈ W, for all a ∈ V, for all v, v′ ∈ a, x ∈ (v∩v′)

implies v = v′.

As usual, for any relation S on W and for x ∈ W, we define S(x) =^{def} {y ∈ W : xSy}.

4 Frames with indiscernibility and complementarity

An IC-frame (Indiscernibility + Complementarity) is a relational system F = ⟨W, ≡, R⟩ such that W is a nonempty set and ≡ and R are binary relations on W satisfying the following conditions:

(S1) x ≡ x; (S2) x ≡ y implies y ≡ x; (S3) x ≡ y and y ≡ z imply x ≡ z; (S4) xRy implies yRx; (S5) xRy and y ≡ z imply xRz; (S6) xRy and yRz imply x ≡ z; (S7) not xRx. In any IC-frame ⟨W, ≡, R⟩, R is a complementarity relation in the sense of the definition given in [DO98], that is R is irreflexive, symmetric and 3-transitive. Given an information system S = ⟨OB, AT ⟩, the relations ≡_{S} and R_{S} satisfy the conditions (S1)-(S7). Hence, the relational system ⟨OB, ≡_{S}, R_{S}⟩ is an ICframe.

Any IC-frame with the relations derived from an information system in the above way is referred to as a standard IC-frame. In sections 7 and 8 the following classes of IC-frames will be investigated. Let K, KS, KSD, KST be the class of all the IC-frames, standard IC-frames, standard IC-frames derived from a deterministic information system, and standard IC-frames derived from a total information system, respectively. Furthermore, let KN S be the class of relational systems that satisfy conditions (S1),...,(S6). They are referred to as non-standard IC-frames.

5 Applications of indiscernibility and complementarity

Many applications of indiscernibility relations alone are known in the literature, see for example [BO97, DO97, Orło83, Orło90, OP84]. In this section we briefly describe applications which require both indiscernibility and complementarity. An information system S = ⟨OB, AT ⟩ such that the set of attributes is finite and is partitioned into two subsets AT = C ∪ D, C ∩ D = ∅, C and D are the set of condition attributes and the set of decision attributes, respectively, is referred to as decision table. Consider the information system from Section 2 and assume that C = {colour, size} and D = {d}.

¿From a decision table a set of decision rules can be derived relating descriptions of objects in terms of conditions to decisions about these objects. Let C = {c_{1}, ..., c_{n}}. For any object x ∈ OB, the rule r_{x} derived from S has the form:

r_{x}: if the value of c_{1} for y is f(x, c_{1}) and … and the value of c_{n} for y is

f(x, c_{n}) then y ∈ Y, where Y =≡_{D} (x).

In our example, the equivalence classes of ≡_{d} are Y_{1} = {x_{1}, x_{2}} and Y_{2} = {x_{3}}. The decision rule determined by an object x_{1} is:

r_{x_{1}}: if an object is green and small then it belongs to class Y_{1}. An object o supports a decision rule r_{x} if its description matches both the condition part and the decision part of the rule, that is if o ∈≡_{AT} (x). An important problem in designing algorithms for synthesis of decision rules is to find heuristics for making the rules sufficiently general, so that they will be supported by many objects. Reduction of attributes and reduction of values of attributes are often parts of these heuristics. Computation of indiscernibility and complementarity provides a tool for verification of the conditions of reducibility of the respective data. A condition attribute a is redundant in the rule r_{x} if there is an y ∈ OB such that:

1. xR_{a}y;

2. x ≡_{C−{a}} y;

3. for every b ∈ C − {a}, ≡_{b} (x) ⊆≡_{D} (x).

Intuitively, an attribute a is redundant in a rule if the decision made on the basis of that rule does not depend on a. Continuing our example, we can easily see that attribute colour is redundant in the rule r_{x_{1}}. The reduced rule is supported by x_{1} and x_{2}.

The process of reduction of values of attributes is referred to as contraction of attributes. An attribute b is a contraction of attribute a if there is a mapping α : V AL_{a} → V AL_{b} such that for every x ∈ OB, f(x, a) = α(f(x, b)). Of special importance is a contraction to features. An attribute a is referred to as a feature if V AL_{a} = {0, 1}. It is known that for every attribute a there is a set F (a) of features such that ≡_{a}=≡_{F (a)} [Iwi88]. It is easy to see that features can be characterised in terms of indiscernibility and complementarity.

Lemma 5.1. Let S = ⟨OB, AT ⟩ be a deterministic information system.

(I) If an attribute a is a feature then

(*) for every x, y ∈ OB either x ≡_{a} y or xR_{a}y; (II) If (*) holds then there is a feature b such that ≡_{a}=≡_{b}.

Consider the following decision table below left:

colour  d
x_{1} light green +
x_{2}  red  -
x_{3}  blue  -
x_{4} dark green +

c  d
x_{1} green +
x_{2} red -
x_{3} blue -
x_{4} green +

Suppose that we are not interested in the tints of colours, then we can contract the attribute colour and replace the first table by the table above right. This decision table leads to a smaller number of rules supported by more objects. If furthermore, we contract c to the attribute with values: green for x_{1} and x_{4} and not green for x_{2} and x_{3}, then we obtain two decision rules that are in agreement with the original data. Of course the real situations are much more involved and various other constraints have to be taken into account. Our only aim here is to give an intuitive account of the role of indiscernibility and complementarity.

6 First-order characterization of IC-frames

In this section we show that every IC-frame is a standard IC-frame that is derived from a deterministic information system. Let F = ⟨W, ≡, R⟩ be an IC-frame. A subset X ⊆ W is called an ≡-set ⇔^{def} for any x, y ∈ W, if x ∈ X and x ≡ y, then y ∈ X. Equivalently, X is an union of equivalence classes of ≡. A set X is called an R-set ⇔^{def} it is a ≡-set and for any x, y ∈ X, we have not xRy. X is called a good set ⇔^{def} it is an R-set and its complement W \ X is also an R-set. Obviously, ∅ is an R-set.

Lemma 6.1. Let F = ⟨W, ≡, R⟩ be an IC-frame.

(I) ≡ (x) is the smallest ≡-set containing x; (II) The set of all ≡-sets is closed under the operations of complementation

(wrt W), arbitrary unions and intersections; (III) if not xRy, then ≡ (x)∪ ≡ (y) is an R-set; (IV) for any x ∈ W, ≡ (x) is an R-set; (V) if (X_{i})_{i∈I} is a chain of R-sets, then ⋃_{i∈I} X_{i} is an R-set; (VI) If X is an ≡-set, then X∪ ≡ (y) is the smallest ≡-set containing X and y. (VII) If X is an R-set then X∪ ≡ (y) is an R-set iff for any x ∈ X, not xRy.

The proof is by an easy verification.

Lemma 6.2. Let F = ⟨W, ≡, R⟩ be an IC-frame and X and Y be R-sets such that X ∩Y = ∅. Then for any x ∈ W one of the following conditions is satisfied:

(I) X∪ ≡ (x) is an R-set and (X∪ ≡ (x)) ∩ Y = ∅; (II) Y ∪ ≡ (x) is an R-set and X ∩ (≡ (x) ∪ Y) = ∅;

Proof: Suppose that neither (I) nor (II) holds. ¿From not (I) and Lemma 6.1(VII), (i) there is x_{1} ∈ X such that x_{1}Rx or (ii) there is y_{1} ∈ Y such that x ≡ y_{1} (remember X ∩ Y = ∅). Similarly, from not (II) and Lemma 6.1(VII), (iii) there is x_{2} ∈ Y such that x_{2}Rx or (iv) there is y_{2} ∈ X such that x ≡ y_{2} (remember X ∩ Y = ∅). Four cases can be distinguised.

(i) and (iii): By (S4) and (S6), we obtain x_{1} ≡ x_{2}. So x_{2} ∈ X, a contradiction since X ∩ Y = ∅.

(i) and (iv): By (S5), x_{1}Ry_{2}, a contradiction since for all z, z′ ∈ X, not zRz′. (ii) and (iii): By (S5), x_{2}Ry_{1}, a contradiction since for all z, z′ ∈ X, not zRz′. (ii) and (iv): Since ≡ is an equivalence relation, y_{1} ≡ y_{2}. Since X and Y are R-sets, {y_{1}, y_{2}} ⊆ X ∩ Y, a contradiction. Q.E.D.

Theorem 6.3. (Separation theorem for R-sets) Let X and Y be R-sets such that X ∩ Y = ∅. Then there exists a good set Z such that X ⊆ Z and Y ⊆ (W \ Z).

Proof: Let M be the set of R-sets X′ such that X ⊆ X′ and X′ ∩Y = ∅. M is non-empty since X ∈ M. It is easy to see that if (X′_{i})_{i∈I} is a chain of elements of M then Y′ = ⋃_{i∈I} X′_{i} is an R-set in M. So, we may apply Zorn Lemma and hence M has a maximal element, say Z.

Let N be the set of R-sets X′ such that Y ⊆ X′ and X′ ∩ Z = ∅. By the same argument as above we may apply the Zorn Lemma to N and let Z′ be the maximal element of N. So, we have X ⊆ Z, Y ⊆ Z′ and Z and Z′ are R-sets. We shall show that Z ∪ Z′ = W, which will yield that Z′ = W \ Z and that Z and Z′ are good sets.

Let x be an arbitrary element of W. Then by Lemma 6.2, either (i) Z∪ ≡ (x) is an R-set and (Z∪ ≡ (x)) ∩ Z′ = ∅ or (ii) Z′∪ ≡ (x) is an R-set and (Z′∪ ≡ (x)) ∩ Z = ∅. In the case of (i), (Z∪ ≡ (x)) ∩ Y = ∅ because Y ⊆ Z′. Since X ⊆ Z ⊆ Z∪ ≡ (x) we obtain that Z∪ ≡ (x) ∈ M. By maximality of Z in M, x ∈ Z. In the case of (ii), Y ⊆ Z′ ⊆ Z′∪ ≡ (x), which implies that Z′∪ ≡ (x) ∈ N. By maximality of Z′ in N, x ∈ Z′. This completes the proof. Q.E.D.

Let GS(F) denote the set of all good sets of the IC-frame F.

Lemma 6.4. Let F = ⟨W, ≡, R⟩ be an IC-frame. Then,

(I) GS(F) is non-empty; (II) ⋃_{X∈GS(F)} X = W.

Proof: (I) We have seen that ∅ is an R-set. By applying Theorem 6.3 with X = Y = ∅, we obtain that there is a good set in GS(F). (II) Let us show that for any x ∈ W, there is a good set containing x. By Lemma 6.2(IV), ≡ (x) is an R-set. By applying Theorem 6.3 with X =≡ (x) and Y = ∅, we get that there is a good set containing x. Q.E.D.

Lemma 6.5. Let F = ⟨W, ≡, R⟩ be an IC-frame. Then, for any x, y ∈ W,

(I) x ≡ y iff for all X ∈ GS(F), x ∈ X iff y ∈ X; (II) xRy iff for all X ∈ GS(F), x ∈ X iff y ∉ X.

Proof: (I) (→) Assume x ≡ y and X ∈ GS(F). Then obviously, x ∈ X iff y ∈ X. (←) Assume for all X ∈ GS(F), x ∈ X iff y ∈ X and suppose not x ≡ y. Then, ≡ (x)∩ ≡ (y) = ∅. By Lemma 6.1(IV), ≡ (x) and ≡ (y) are R-sets. By Theorem 6.3, there is a good set Z such that ≡ (x) ⊆ Z and ≡ (y) ⊆ W \ Z. So, x ∈ Z and y ∉ Z, a contradiction. (ii) (→) Suppose xRy and X ∈ GS(F). Suppose x ∈ X. Then since X is an R-set, we obtain that y ∉ X. Now, suppose y ∉ X. So, y ∈ W \ X and W \ X is a good set and therefore x ∉ W \ X, that is x ∈ X. (←) Assume for all X ∈ GS(F), x ∈ X iff y ∉ X and suppose not xRy. Then by Lemma 6.2(III), ≡ (x)∪ ≡ (y) is an R-set. By applying Theorem 6.3 with X =≡ (x)∪ ≡ (y) and Y = ∅, there is a good set Z such that X ⊆ Z. So, x, y ∈ Z, which is in contradiction with the assumption. Q.E.D.

Theorem 6.6. (first-order characterization theorem for indiscernibility and complementarity) Each IC-frame is a standard IC-frame over some deterministic information system [resp. over some total information system].

Proof: Let F = ⟨W, ≡, R⟩ be an IC-frame. Let S be the set-theoretical information system ⟨W, V ⟩ such that V = {{X} : X ∈ GS(F)} [resp. V = {GS(F)}]. By Lemma 6.4(I), V is non-empty. Since each element of V is a singleton, then S is deterministic [resp. by Lemma 6.4(II), S is total]. We have to show that ≡ coincides with ≡_{S} and R coincides with R_{S}. Applying Lemma 3.1 and Lemma 6.5,

• x ≡_{S} y iff for all X ∈ V and for all v ∈ X, x ∈ v iff y ∈ v iff for all Y ∈ GS(F) x ∈ Y iff y ∈ Y iff x ≡ y; • xR_{S}y iff for all X ∈ V and for all v ∈ X, x ∈ v iff y ∉ v iff for all

Y ∈ GS(F) x ∈ Y iff y ∉ Y iff xRy.

When S is total, the end of the proof is similar. Q.E.D.

We shall show that indiscernibility and complementarity in property systems (see [Vak90, Vak91]) have the same first-order characterization as in information system. Let us recall the relevant definitions from [Vak91]. A property system S is a triple S = ⟨OB, P R, f⟩ where OB is a non-empty set of objects, P R is a non-empty set of elements called properties and f is a function which assigns to each object x ∈ OB a subset f(x) ⊆ P R called the set of properties of x. The relations of indiscernibility and complementarity derived from a property system S have the following definitions:

• x ≡_{S} y ⇔^{def} f(x) = f(y);

• xR_{S}y ⇔^{def} f(x) = P R \ f(y).

It is easy to see that the frame ⟨OB, ≡_{S}, R_{S}⟩ is an IC-frame and the theory of these frames can be applied to prove the following:

Theorem 6.7. Each IC-frame is a standard frame over some P-system.

Proof: Let F = ⟨W, ≡, R⟩ be an IC-frame. We define a property system S = ⟨OB, P R, f⟩ as follows:

• OB =^{def} W;

• P R =^{def} GS(F);

• for x ∈ W, f(x) =^{def} {X ∈ GS(F) : x ∈ X}.

Then, by using Lemma 6.5 we obtain:

• for all X ∈ GS(F), x ∈ X iff y ∈ X iff for all X ∈ GS(F), X ∈ f(x) iff X ∈ f(y) iff f(x) = f(y) iff x ≡_{S} y;

• for all X ∈ GS(F), x ∈ X iff y ∉ X iff for all X ∈ GS(F), X ∈ f(x) iff X ∉ f(y) iff f(x) = P R \ f(y) iff xR_{S}y.

Q.E.D.

7 The information logic LIC for indiscernibility and complementarity

Given a set PRP = {p_{1}, p_{2}, …} of atomic formulae, the formulae ϕ ∈ FML are inductively defined as follows for p_{i} ∈ PRP:

ϕ ::= p_{i} | ϕ_{1} ∧ ϕ_{2} | ¬ϕ | [≡]ϕ | [R]ϕ

Standard abbreviations include ⇔, ⟨R⟩, ⟨≡⟩.

A model M is a structure ⟨W, ≡, R, m⟩ such that F = ⟨W, ≡, R⟩ is a member of KN S and m is a meaning function m : PRP → P(W). M is said to be based on F. The satisfiability of formulas (written M, x ⊧ ϕ) is defined as usual. The logic LIC is a propositional modal logic whose set of formulae is FML and the semantic structures are models based on IC-frames. A formula ϕ is said to be true in the model M = ⟨W, ≡, R, m⟩ (written M ⊧ ϕ) ⇔^{def} for all x ∈ W, M, x ⊧ ϕ. A formula ϕ is said to be true in the frame F (written F ⊧ ϕ) ⇔^{def} ϕ is true in all the models based on F.

Let us define the Hilbert-style system HLIC as follows. The set of axiom schemes consists of the formulas of the following form:

(PC) the tautologies of the Propositional Calculus; (K) [a](ϕ ⇒ ψ) ⇒ ([a]ϕ ⇒ [a]ψ) for a ∈ {R, ≡}; (A1) [≡]ϕ ⇒ ϕ; (A2) ϕ ⇒ [≡]⟨≡⟩ϕ; (A3) [≡]ϕ ⇒ [≡][≡]ϕ; (A4) ϕ ⇒ [R]⟨R⟩ϕ; (A5) [≡]ϕ ⇒ [R][≡]ϕ; (A6) [≡]ϕ ⇒ [R][R]ϕ.

The inference rules of HLIC are the modus ponens (from ϕ and ϕ ⇒ ψ infer ψ) and necessitation (from ϕ infer [a]ϕ for a ∈ {R, ≡}). We write ϕ ∈ HLIC to denote that ϕ is a theorem of HLIC.

Let C be a class of non-standard IC-frames. HLIC is sound with respect to C ⇔^{def} for every formula ϕ, if ϕ ∈ HLIC, then ϕ is true in every frame from C. HLIC is complete with respect to C if for every formula ϕ, if ϕ is true in every frame from C then ϕ ∈ HLIC.

Lemma 7.1. For C in {K, KS, KSD, KST , KN S}, HLIC is sound with respect to C

8 Completeness of the logic LIC

In this section we investigate completeness of HLIC with respect to the classes of IC-frames defined in section 4.

Theorem 8.1. HLIC is complete with respect to the class KN S of non-standard IC-frames.

Proof: The proof can be obtained with a standard method of modal logic. The axiom schemes (A1)-(A6) modally define the conditions (S1)-(S6). All the axiom schemes (A1)-(A6) are Sahlqvist’s formulas, so completeness with respect to the non-standard semantics is immediate from Sahlqvist’s Theorem. Q.E.D.

Observe that (A1)-(A6) are equivalent to primitive modal formulae in the sense of [Kra96] and therefore a cut-free display calculus exists for the logic LIC and it is sound and complete with respect to the class KN S of nonstandard IC-frames.

The completeness of LIC with respect to the classes of standard IC-frames can be obtained by applying the copying method introduced in [Vak90].

Definition 8.1. (see e.g. [Vak90]) Let F = ⟨W, ≡, R⟩ and F′ = ⟨W′, ≡′, R′⟩ be frames and I be a class of maps from W into W′. I is a copying from F into

F′ ⇔^{def}

(I1) W′ = {f(x) : f ∈ I, x ∈ W }; (I2) for all x, y ∈ W and for all f, g ∈ I, if f(x) = g(y), then x = y; (I3) for all a ∈ {R, ≡}, for all x, y ∈ W and for any f ∈ I, if xay, then there is

g ∈ I such that f(x)a′g(y); (I4) for all a ∈ {R, ≡}, for all x, y ∈ W, and for all f, g ∈ I, if f(x)a′g(y), then

xay.

Lemma 8.2. [Vak90] Let I be a copying from F = ⟨W, ≡, R⟩ into F′ = ⟨W′, ≡′ , R′⟩, and M = ⟨W, ≡, R, m⟩ and M′ = ⟨W′, ≡′, R′, m′⟩ be models such that for p ∈ PRP, m′(p) = {f(x) : x ∈ m(p), f ∈ I}. Then, for x ∈ W, f ∈ I and for any formula ψ, M, x ⊧ ψ iff M′, f(x) ⊧ ψ.

The proof is by induction on the complexity of ψ.

Lemma 8.3. Let F = ⟨W, ≡, R⟩ be a non-standard IC-frame. Then, there exists an IC-frame F′ = ⟨W′, ≡′, R′⟩ and a copying from F to F′.

Proof: Let F′ = ⟨W′, ≡′, R′⟩ be the frame defined as follows:

• W′ =^{def} W × {−1, 1};

• for any ⟨x, i⟩, ⟨y, j⟩ ∈ W′, ⟨x, i⟩ ≡′ ⟨y, j⟩ ⇔^{def} x ≡ y and i = j;

• for any ⟨x, i⟩, ⟨y, j⟩ ∈ W′, ⟨x, i⟩R′⟨y, j⟩ ⇔^{def} xRy and i = −j.

Let I = {f_{−1}, f_{1}} be the set of maps such that for i ∈ {−1, 1}, f_{i} : W → W′ and for x ∈ W, f_{i}(x) = ⟨x, i⟩. It is easy to see that F′ is an IC-frame (satisfying the conditions (S1)-(S7)) and that I is indeed a copying. The satisfaction of (I1), (I2) and (I4) is straighforward. By way of example, let us show that (I3) holds with a = R. Let xRy and i ∈ {−1, 1}. So, f_{i}(x)R′f_{−i}(y). Q.E.D.

Theorem 8.4. HLIC is complete with respect to the class K of IC-frames.

Proof: Suppose ϕ is not a theorem of HLIC. Then by Theorem 8.1, ϕ is not true in some non-standard IC-frame F = ⟨W, ≡, R⟩, i.e. there is a model M = ⟨W, ≡, R, m⟩ based on F and x ∈ W such that M, x |̸= ϕ. By Lemma 8.3, there is an IC-frame F′ = ⟨W′, ≡′, R′⟩ and a copying I from F to F′. Then by Lemma 8.2, M′, x |̸= ϕ where M′ is a model based on F′ such that for any propositional variable p, m′(p) = {f(x) : x ∈ m(p), f ∈ I}. So, ϕ is not true in the class of IC-frames. Q.E.D.

Theorem 8.5 below is one of the main results in this paper:

Theorem 8.5. (Standard completeness) Let ϕ be a formula. The statements below are equivalent:

(I) ϕ is a theorem of HLIC; (II) ϕ is true in every frame from KS; (III) ϕ is true in every frame from KSD; (IV) ϕ is true in every frame from KST ; Proof: (I) → (II), (I) → (III) and (I) → (IV) are true by Lemma 7.1. (II) → (III) Every IC-frame derived from a deterministic information system is a standard frame. (II) → (IV) Every IC-frame derived from a total information system is a standard frame. For the implications (III) → (I) [resp. (IV) → (I)], suppose ϕ is not a theorem of HLIC. By Theorem 8.4, ϕ is not valid in some IC-frame F = ⟨W, ≡, R⟩. By Theorem 6.6, F is a standard frame over some deterministic [resp. total] information system. This proves (III) → (I) [resp. (IV) → (I)], which completes the proof. Q.E.D.

9 Complexity of the satisfiability problem for LIC

Lemma 9.1 is used in the proof of Lemma 9.2.

Lemma 9.1. Let F = ⟨W, ≡, R⟩ be an IC-frame, x ∈ W and F_{x} = ⟨W_{x}, ≡_{x}, R_{x}⟩ be the generated subframe from x. Then

(I) If there is an y ∈ W such that xRy, then W_{x} =≡ (x)∪ ≡ (y) and for all x′, y′ ∈ W_{x},

• x′ ≡_{x} y′ iff either {x′, y′} ⊆≡ (x) or {x′, y′} ⊆≡ (y);

• x′R′y′ iff either x′ ∈≡ (x) and y′ ∈≡ (y) or x′ ∈≡ (y) and y′ ∈≡ (x);

(II) if there is no y ∈ W such that xRy, then W_{x} =≡ (x), ≡_{x}= W_{x} × W_{x} and R_{x} = ∅.

Lemma 9.2. Any LIC-satisfiable formula ϕ is satisfiable in a LIC-model ⟨W, ≡ , R, m⟩ based on an IC-frame ⟨W, ≡, R⟩ such that card(W) ≤ 2 × |ϕ| + 2.

Here |ϕ| denotes the length of the formula ϕ, that is the number of symbols occurring in ϕ. Proof: Let M = ⟨W, ≡, R, m⟩ be an LIC-model, w_{0} ∈ W such that M, w_{0} ⊧ ϕ. Case 1: R(w_{0}) ≠ ∅ So let w_{1} be some element in R(w_{0}). Let X_{0}^{ϕ} be the set

X_{0}^{ϕ} =^{def} {ψ : [≡]ψ ∈ sub(ϕ), M, w_{0} |̸= [≡]ψ}∪{ψ : [R]ψ ∈ sub(ϕ), M, w_{1} |̸= [R]ψ}

where sub(ϕ) denotes the set of subformulae of ϕ. Let X_{1}^{ϕ} be the set

X_{1}^{ϕ} =^{def} {ψ : [R]ψ ∈ sub(ϕ), M, w_{0} |̸= [R]ψ}∪{ψ : [≡]ψ ∈ sub(ϕ), M, w_{1} |̸= [≡]ψ}

For each ψ ∈ X_{i}^{ϕ} (i ∈ {0, 1}), we choose some witness w_{i}^{ψ} ∈≡ (w_{i}), such that M, w_{i}^{ψ} |̸= ψ. Let M′ = ⟨W′, ≡′, R′, m′⟩ be the restriction of M to

W′ = {w_{0}, w_{1}} ∪ {w_{0}^{ψ} : ψ ∈ X_{0}^{ϕ}} ∪ {w_{1}^{ψ} : ψ ∈ X_{1}^{ϕ}}

Since the conditions (S1)-(S7) are universally quantified first-order formula, by Łos-Tarski preservation theorem, the class of IC-frames is closed under subframes. So M′ is a model based on an IC-frame and for any i ∈ {0, 1} and for any w′ ∈≡′ (w_{i}), w′′ ∈≡′ (w_{1−i}), w′R′w′′. Let us show by induction on the structure of formulae that for any ψ ∈ sub(ϕ) and for any w′ ∈ W′, M, w′ ⊧ ψ iff M′, w′ ⊧ ψ. We omit the cases when ψ is an atomic proposition or when the outmost connective of ψ is Boolean. Case 1.1: ψ = [≡]ψ′ Assume M, w′ ⊧ ψ for some w′ ∈ W′. So for all w′′ ∈≡ (w′), M, w′′ ⊧ ψ′. A fortiori, for all w′′ ∈≡′ (w′), M, w′′ ⊧ ψ′. By induction hypothesis, for all w′′ ∈≡′ (w′), M′, w′′ ⊧ ψ′. So, M′, w′ ⊧ ψ. Now assume, M, w′ |̸= ψ for some w′ ∈ W′. Let i ∈ {0, 1} be such that w′ ∈≡ (w_{i}). So there is w′′ ∈≡ (w_{i}) such that M, w′′ |̸= ψ′. By construction, M, w_{i}^{ψ′} |̸= ψ′. Since, w_{i}^{ψ′} ∈ W′, M′, w_{i}^{ψ′} |̸= ψ′ by induction hypothesis. By observing that w′ ≡′ w_{i}^{ψ′}, we have M′, w′ |̸= ψ. Case 1.2: ψ = [R]ψ′ Assume M, w′ ⊧ ψ for some w′ ∈ W′. So for all w′′ ∈ R(w′), M, w′′ ⊧ ψ′. A fortiori, for all w′′ ∈ R′(w′), M, w′′ ⊧ ψ′. By induction hypothesis, for all w′′ ∈ R′(w′), M′, w′′ ⊧ ψ′. So, M′, w′ ⊧ ψ. Now assume, M, w′ |̸= ψ for some w′ ∈ W′. Let i ∈ {0, 1} be such that w′ ∈≡ (w_{i}). So there is w′′ ∈≡ (w_{1−i}) such that M, w′′ |̸= ψ′. By construction, M, w_{1−i}^{ψ′} |̸= ψ′. Since, w_{1−i}^{ψ′} ∈ W′, M′, w_{1−i}^{ψ′} |̸= ψ′ by induction hypothesis. By observing that w′R′w_{1−i}^{ψ′}, then M′, w′ |̸= ψ. Case 2: R(w_{0}) = ∅. Let X^{ϕ} be the set X^{ϕ} = {ψ : [≡]ψ ∈ sub(ϕ), M, w_{0} |̸= [≡]ψ}. For each ψ ∈ X^{ϕ}, there is some witness w^{ψ} ∈≡ (w_{0}) such that M, w^{ψ} |̸= ψ. One can show that R(w^{ψ}) = ∅. w^{ψ} is a witness of that fact that M, w |̸= [≡]ψ. Let M′ = ⟨W′, ≡′, R′, m′⟩ be the restriction of M to

W′ = {w_{0}} ∪ {w^{ψ} : ψ ∈ X^{ϕ}}. That is R′ =^{def} R ∩ W′ × W′, ≡′=^{def}≡ ∩W′ × W′ and

for any atomic proposition p, m′(p) =^{def} m(p) ∩ W′. Observe that R′ = ∅. One can show by induction on the structure of formulae that for any ψ ∈ sub(ϕ) and for any w′ ∈ W′, M, w′ ⊧ ψ iff M′, w′ ⊧ ψ. Consequently, M′, w_{0} ⊧ ϕ and observe that M′ is also a model based on an IC-frame. The case 2 is indeed similar to the proof of [Lad77, Lemma 6.1]. Q.E.D.

In the proof of Lemma 9.2, we select a submodel that contains enough witnesses for the satisfaction of the diamond formulae. This technique has been already successfully applied to other logics such as in [Lad77, Dem98]. Given a finite structure ⟨W, ≡, R, m⟩ and a formula ϕ, it is known that checking whether ϕ is satisfiable in ⟨W, ≡, R, m⟩ can be done in time O(card(W)^{2} × |ϕ|). Consequently,

Theorem 9.3. The set of formulas that are true in all the IC-frames is decidable.

Observe that there exists a linear-time transformation from LIC-validity into F0^{3}-validity (the fragment of classical logic using only three individual variables) (see e.g. [Ben83]). However the exact fragment delineated by the relational translation belongs neither to F0^{2} [Mor75] nor to the loosely guarded fragment that are known to be decidable fragments [Mor75, ANB98].

Theorem 9.4. LIC-satisfiability is in NP, that is it can solved in polynomialtime by a non-deterministic Turing machine.

Observe that to check that a structure ⟨W, ≡, R⟩ is an IC-frame can be done in P-time. NP-hardness of LIC-satisfiability is simply due to the fact that the LIC-satisfiability problem contains SAT (satisfiability problem for the classical propositional calculus). The complexity upper bound from Theorem 9.4 should be compared with complexity lower bounds of other known bimodal logics (see e.g. [HM92, Spa93]) that can be for instance PSPACE-hard (for the bimodal logic with exactly two independent S5 modal operators) or EXPTIME-hard (for K plus the universal modal operator).

References

[ANB98] H. Andreka, I. Nemeti, and J. van Benthem. Modal languages and bounded fragments of predicate logic. J. of Philosophical Logic, 27(3):217–274, 1998.

[Ben83] J. van Benthem. Modal logic and classical logic. Bibliopolis, 1983.

[BO97] W. Buszkowski and E. Orłowska. Indiscernibility-based formalization of dependencies in information systems. In E. Orłowska, editor, Incomplete Information: Rough Set Analysis, pages 293–315. Physica Verlag, Heidelberg, 1997.

[Dem98] S. Demri. A class of decidable information logics. Theoretical Computer Science, 195(1):33–60, 1998.

[DO97] S. Demri and E. Orłowska. Logical analysis of indiscernibility. In E. Orłowska, editor, Incomplete Information: Rough Set Analysis, pages 347–380. Physica Verlag, Heidelberg, 1997.

[DO98] S. Demri and E. Orłowska. Complementarity relations: reduction of decision rules and informational representability. In L. Polkowski and A. Skowron, editors, Rough sets in Knowledge Discovery, pages 99–106. Physica Verlag, Heidelberg, 1998.

[DO99] I. Duentsch and E. Orlowska. Logics of complementarity in information systems, 1999. Submitted.

[HM92] J. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.

[Iwi88] T. Iwinski. Contraction of attributes. Bulletin of the PAS, Mathematics, 36(9/10):623–632, 1988.

[Kra96] M. Kracht. Power and weakness of the modal display calculus. In H. Wansing, editor, Proof theory of modal logic, pages 93–121. Kluwer Academic Publishers, 1996.

[Lad77] R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467–480, 1977.

[Mor75] M. Mortimer. On language with two variables. Zeit. für Math. Logik and Grund. der Math., 21:135–140, 1975.

[OP84] E. Orłowska and Z. Pawlak. Measurement and indiscernibility. Bulletin of the PAS, 32:617–624, 1984.

[Orło83] E. Orłowska. Semantics of vague concepts. In G. Dorn and P. Weingartner, editors, Foundations of Logic and Linguistics. Problems and Solutions. Selected contributions to the 7th International Congress of Logic, Methodology, and Philosophy of Science, Salzburg, pages 465–482. London-New-York, Plenum Press, 1983.

[Orło90] E. Orłowska. Verisimilitude based on concept analysis. Studia Logica,

XLIX:307–320, 1990.

[Spa93] E. Spaan. Complexity of Modal Logics. PhD thesis, ILLC, Amsterdam University, March 1993.

[Vak87] D. Vakarelov. Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information. In Ph. Jorrand and V. Sgurev, editors, Artificial Intelligence: Methodology, Systems, Applications, pages 255–260. Elsevier Science Publishers B.V. (North-Holland), 1987.

[Vak90] D. Vakarelov. Modal logics for knowledge representation systems. Theoretical Computer Science, 90:433–456, 1990.

[Vak91] D. Vakarelov. Logical analysis of positive and negative similarity relations in property systems. In M. de Glas and D. Gabbay, editors, First World Conference on the Fundamentals of Artificial Intelligence, pages 491-499, 1991.