Dual Tableaux for Information Logics of Relative Frames

Abstract

In the preceding chapter in Sect. 11.3 we demonstrated that a specification of information relations which would be meaningful for information systems with incomplete information requires an explicit reference to a set of attributes with respect to which the relations are defined. In order to incorporate in a logical formalism the sets of attributes which determine the relations, the notions of a relative relation and a relative frame i.e., the frame whose relations are relative, were introduced in [Orł88], see also [DO02]. More precisely, a relative frame consists of a family, or several families of relations such that the relations within the family are indexed with subsets of a set of parameters, intuitively understood as attributes of an information system. Apart from the ordinary properties of relations such as, for example, symmetry or transitivity, relative relations may have some properties which refer to the family of relations as a whole. These properties are collectively named global properties of relations. For example, one of the typical global property says that a relation indexed with the union of two sets equals intersection of relations indexed with the components of the union. Such an assumption is relevant, among others, when the family consists of equivalence relations.

1 Introduction

In the preceding chapter in Sect. 11.3 we demonstrated that a specification of information relations which would be meaningful for information systems with incomplete information requires an explicit reference to a set of attributes with respect to which the relations are defined. In order to incorporate in a logical formalism the sets of attributes which determine the relations, the notions of a relative relation and a relative frame i.e., the frame whose relations are relative, were introduced in [Orł88], see also [DO02]. More precisely, a relative frame consists of a family, or several families of relations such that the relations within the family are indexed with subsets of a set of parameters, intuitively understood as attributes of an information system. Apart from the ordinary properties of relations such as, for example, symmetry or transitivity, relative relations may have some properties which refer to the family of relations as a whole. These properties are collectively named global properties of relations. For example, one of the typical global property says that a relation indexed with the union of two sets equals intersection of relations indexed with the components of the union. Such an assumption is relevant, among others, when the family consists of equivalence relations. Assuming that the equivalence of objects is established whenever they have the same features corresponding to the set of attributes declared in the definition of this relation, then clearly taking more attributes into account we get a finer granulation of the set of objects than in the case of any smaller number of attributes.

In a full generality, relative frames have families of relations indexed by elements from any level of the powerset hierarchy of a set of parameters. The relative frames of that kind are a convenient tool for specification of hierarchical information such as, for example, a subject classification system. A discussion of these applications of relative frames can be found in [DO02], Chaps. 7–;9. Relative frames and their logics are studied, among others, in [DS02b, Bal02, DO07].

In this chapter we confine ourselves to a simple case of indices which are finite subsets of parameters. We present relative versions of the frames considered in the preceding chapter and information logics based on those frames. We construct dual tableaux for these logics focusing on the treatment of global conditions assumed in the models of the logics. The method of construction of those dual tableaux can be extended to the theories of relative frames determined by a powerset hierarchy of sets of attributes.

2 Relative Frames

Let Par be a non-empty set of parameters intuitively interpreted as a set of attributes of an information system. A relative frame is a structure:

$$\mathcal{F} = (U,{({R}_{P}^{1})}_{ P\in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})},\ldots,{({R}_{P}^{n})}_{ P\in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})}),$$

where relations from ${({R}_{P}^{i})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})}$, i ∈ { 1, …, n}, are indexed with finite subsets of a non-empty set Par.

Typically, these relations satisfy either of the following postulates:

For all $P,Q \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$,

(S1) R _{P ∪Q} = R _P ∩ R _Q ;(W1) R _{P ∪Q} = R _P ∪R _Q .These conditions are referred to as global conditions, because they refer to a family of relations as a whole. The properties of relations listed in Proposition 11.2.1 will be called local conditions.The characterization of a family of relative relations often requires special postulates for the relations indexed with the empty set. The typical condition for the relation R _∅ is either of the following:(S2) R _∅ = U ²;(W2) R _∅ = ∅.

Conditions (S1) and (S2) reflect the behaviour of strong relations derived from an information system, and conditions (W1) and (W2) reflect the behaviour of weak relations.

Typically, information logics of relative frames are based on the following classes of frames:

• FS – the class of relative frames in which the families of relative relations satisfy conditions (S1) and (S2). The members of FS are called FS-frames or relative frames with strong relations;

• FW – the class of relative frames in which the families of relative relations satisfy conditions (W1) and (W2). The members of FW are called FW-frames or relative frames with weak relations.

Frames with indistinguishability and distinguishability relations listed below provide examples of members of the FS and FW families.

Frames with Indistinguishability Relations:

• FS−IND is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is an equivalence relation. Consequently, for every P ⊆ Par, R _P is an equivalence relation, since reflexivity, symmetry, and transitivity are preserved under intersection. The members of FS−IND are called strong indiscernibility frames;

• FS−SIM is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is weakly reflexive and symmetric. Consequently, for every P ⊆ Par, R _P is weakly reflexive and symmetric. The members of FS−SIM are called strong similarity frames;

• FS−ICOM is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is reflexive, symmetric, and co-3-transitive. Consequently, for every P ⊆ Par, R _P is reflexive and symmetric. The property of co-3-transitivity is not preserved under intersection. The members of FS−ICOM are called strong incomplementarity frames;

• FS−IN is the class of FS-frames (U, (R _P ) _{P ⊆ Par}, (Q _P ) _{P ⊆ Par}) with two families of relative relations such that for every p ∈ Par, R _{p} and Q _{p} are reflexive and transitive, and ${R}_{\{p\}} = {Q}_{\{p\}}^{-1}$. Consequently, for every P ⊆ Par, R _P and Q _P are reflexive and transitive, and ${R}_{P} = {Q}_{P}^{-1}$. The members of FS−IN are called strong inclusion frames;

• FW−IND is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is an equivalence relation. Consequently, for every non-empty P ⊆ Par, R _P is reflexive and symmetric. Transitivity is not preserved under union. The members of FW−IND are called weak indiscernibility frames;

• FW−SIM is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is weakly reflexive and symmetric. Consequently, for every P ⊆ Par, R _P is weakly reflexive and symmetric. The members of FW−SIM are called weak similarity frames;

• FW−ICOM is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is reflexive, symmetric, and co-3-transitive. Consequently, for every non-empty P ⊆ Par, R _P is reflexive, symmetric, and co-3-transitive, since all these properties are preserved under union. The members of FW−ICOM are called weak incomplementarity frames;

• FW−IN is the class of FW-frames (U, (R _P ) _{P ⊆ Par}, (Q _P ) _{P ⊆ Par}) with two families of relative relations such that for every p ∈ Par, R _{p} and Q _{p} are reflexive and transitive, and ${R}_{\{p\}} = {Q}_{\{p\}}^{-1}$. Consequently, for every P ⊆ Par, ${R}_{P} = {Q}_{P}^{-1}$ and if P≠∅, then R _P and Q _P are reflexive. Transitivity is not preserved under union. The members of FW−IN are called weak inclusion frames.

Frames with Distinguishability Relations:

• FS−DIV is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is irreflexive, symmetric, and co-transitive. Consequently, for every P ⊆ Par, R _P is symmetric, and if P≠∅, then R _P is irreflexive. Co-transitivity is not preserved under intersection. The members of FS−DIV are called strong diversity frames;

• FS−RORT is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is co-weakly reflexive and symmetric. Consequently, for every P ⊆ Par, R _P is co-weakly reflexive and symmetric. The members of FS−RORT are called strong right orthogonality frames;

• FS−COM is the class of FS-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is irreflexive, symmetric, and 3-transitive. Consequently, for every P ⊆ Par, R _P is symmetric and 3-transitive, and if P≠∅, then R _P is irreflexive. The members of FS−COM are called strong complementarity frames;

• FW−DIV is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is irreflexive, symmetric, and co-transitive. Consequently, for every P ⊆ Par, R _P is irreflexive, symmetric, and co-transitive. Co-transitivity is preserved under union. The members of FW−DIV are called weak diversity frames;

• FW−RORT is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is co-weakly reflexive and symmetric. Consequently, for every P ⊆ Par, R _P is co-weakly reflexive and symmetric. The members of FW−RORT are called weak right orthogonality frames;

• FW−COM is the class of FW-frames (U, (R _P ) _{P ⊆ Par}) such that for every p ∈ Par, R _{p} is irreflexive, symmetric, and 3-transitive. Consequently, for every P ⊆ Par, R _P is irreflexive and symmetric. 3-transitivity is not preserved under union. The members of FW−COM are called weak complementarity frames.

The languages of information logics with semantics of relative frames, referred to as Rare-logics, are the multimodal languages with modal operations determined by relations indexed with finite subsets of a set Par.

3 Relational Formalizations of the Logics of Strong and Weak Relative Frames

As a first case study we present logics L _FS and L _FW based on FS-frames and FW-frames, respectively. The choice of modal operations usually depends on the global conditions assumed in the models. Typically, logic L _FS has the sufficiency operations in its language and logic L _FW the necessity operations determined by the relational constants. We recall that satisfaction of a formula built with the sufficiency operation, [[T]]φ, by a state s in a model $\mathcal{M}$ is defined as:

• $\mathcal{M},s\models [[T]]\varphi$ iff for every s′ ∈ U, if $\mathcal{M},s\prime\models \varphi$, then (s, s′) ∈ T.

Let L ∈ {L _FS , L _FW }. An L-model is a structure $\mathcal{M} = (U,{({R}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}\mbox{ (Par)}},m)$ such that U is a non-empty set, R _P are binary relations on U indexed with finite subsets of a set Par, and m is a meaning function such that:

• m(p) ⊆ U, for any propositional variable p;

• R _∅ = \begin{array}{ll} U ×U, if L =L _FS , \\ ∅, if L =L _FW ; \end{array}

• R _{p} ⊆ U ×U, for every p ∈ Par;

• for all $P,Q \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}$:

  $${R}_{P\cup Q} = \left \{\begin{array}{ll} {R}_{P} \cap {R}_{Q},&\mbox{ if $\mathsf{L} ={ \mathsf{L}}_{\mathsf{FS}}$}, \\ {R}_{P} \cup {R}_{Q},&\mbox{ if $\mathsf{L} ={ \mathsf{L}}_{\mathsf{FW}}$.}\end{array} \right.$$

If a Rare-logic L is based on any of the subclasses of FS or FW of frames listed in Sect. 12.2, then the appropriate local conditions should be assumed in the corresponding L-models.

The relational language corresponding to an L-language is an RL(1, 1′)-language endowed with the set $\{{R{}_{P}\}}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})}$ of relational constants. The set of relational terms and formulas are defined as in RL(1, 1′)-logic (see Sect. 2.3).

The RL _L -models are structures of the form:

$$\mathcal{M} = (U,{({R}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m),$$

where (U, m) is an RL(1, 1′)-model and R _P = m(R _P ) are binary relations on U satisfying the same conditions as in L-models. As usual, we denote relations in the language and in the models with the same symbols.

The translation of L-formulas into relational terms of the logic RL _L starts, as usual, with a one-to-one assignment of relational variables to the propositional variables and then the translation τ is defined inductively as in Sect. 7.4. As in classical modal logics, we can prove that for L ∈ {L _FS , L _FW } and for every L-formula, L-validity is equivalent to RL _L -validity (see Theorem 7.4.1):

Theorem 12.3.1.

For every L-formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is L-valid;

• 2. xτ(φ)y is RL _L -valid.

Dual tableau systems for Rare-logics are constructed in a similar way as those for information logics of plain frames. Namely, to the RL(1, 1′)-dual tableau we add the rules corresponding to the global conditions assumed in a given logic. The rules corresponding to conditions (S1) and (W1) have the following forms:

For all object variables x and y,

$$\mbox{ (rS1$ \supseteq $)}\quad \frac{x{R}_{P\cup Q}y} {x{R}_{P}y\,\vert \,x{R}_{Q}y}\qquad \mbox{ (rS1$ \subseteq $)}\quad \frac{x-{R}_{P\cup Q}y} {x-{R}_{P}y,x-{R}_{Q}y}$$

$$\mbox{ (rW1$ \supseteq $)}\quad \frac{x{R}_{P\cup Q}y} {x{R}_{P}y,x{R}_{Q}y}\qquad \mbox{ (rW1$ \subseteq $)}\quad \frac{x-{R}_{P\cup Q}y} {x-{R}_{P}y\,\vert \,x-{R}_{Q}y}$$

The rule corresponding to the condition (S2) has the following form:

$$\mbox{ (rS2)}\quad \frac{} {x-{R}_{\varnothing }y}\qquad \mbox{ $x,y$ are any object variables}$$

The rule corresponding to the condition (W2) is:

$$\mbox{ (rW2)}\quad \frac{} {x{R}_{\varnothing }y}\qquad \mbox{ $x,y$ are any object variables}$$

If some of the local conditions are assumed in L-models, then we add the rules reflecting them. The examples of the rules corresponding to the local conditions can be found in Sect. 11.3.

The specific rules of relational proof systems for the logics L _FS and L _FW are:

• The specific ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-rules: (rS2), (rS1 ⊇ ), and (rS1 ⊆ );

• The specific ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$-rules: (rW2), (rW1 ⊇ ), and (rW1 ⊆ );

The notions of an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-set, an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$-set, and correctness of a rule are defined as in Sect. 2.4. Then, the following holds:

Proposition 12.3.1.

• 1. The specific ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$ -rules are ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$ -correct;

• 2. The specific ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$ -rules are ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$ -correct.

Proof.

By way of example, we prove ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-correctness of the rule (rS2). Let X be any set of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-formulas. Assume X ∪{ x − R _∅ y} is an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-set. Suppose that X is not an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-set, that is there exist an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-model $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that for every φ ∈ X, $\mathcal{M},v\nvDash \varphi$. By the assumption, $\mathcal{M},v\models x-{R}_{\varnothing }y$, thus (v(x), v(y)) ∉ R _∅ . However, in all ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-models, R _∅ = U ×U, a contradiction. The preservation of validity from the upper set to the bottom set is obvious. □

Let L ∈ {L _FS , L _FW }. The notions of an RL _L-proof tree, a closed branch of such a tree, a closed RL _L-proof tree, and RL _L-provability are defined as in Sect. 2.4.

A branch b of an RL _L-proof tree is complete whenever it is closed or it satisfies the completion conditions of RL(1, 1′)-dual tableau adjusted to the language of RL _L and the following completion conditions corresponding to the rules (rS1 ⊇ ), (rS1 ⊆ ), (rW1 ⊇ ), (rW1 ⊆ ), (rS2), and (rW2):

For all object variables x and y,

Cpl(rS1 ⊇ ) If xR _{P ∪Q} y ∈ b, then either xR _P y ∈ b or xR _Q y ∈ b, obtained by an application of the rule (rS1 ⊇ );Cpl(rS1 ⊆ ) If x − R _{P ∪Q} y ∈ b, then both x − R _P y ∈ b and x − R _Q y ∈ b, obtained by an application of the rule (rS1 ⊆ );Cpl(rW1 ⊇ ) If xR _{P ∪Q} y ∈ b, then both xR _P y ∈ b and xR _Q y ∈ b, obtained by an application of the rule (rW1 ⊇ );Cpl(rW1 ⊆ ) If x − R _{P ∪Q} y ∈ b, then either x − R _P y ∈ b or x − R _Q y ∈ b, obtained by an application of the rule (rW1 ⊆ );Cpl(rS2) For all objects variables x and y, x − R _∅ y ∈ b, obtained by an application of the rule (rS2);Cpl(rW2) For all objects variables x and y, xR _∅ y ∈ b, obtained by an application of the rule (rW2).

The notions of a complete RL _L-proof tree and an open branch of an RL _L-proof tree are defined as in RL-logic (see Sect. 2.5).

The following form of the closed branch property holds:

Fact 12.3.1 (Closed Branch Property).

For every branch b of an RL _L -proof tree, if xR _{p} y ∈ b and x−R _{p} y ∈ b, for p ∈ Par, or xR _∅ y ∈ b and x−R _∅ y ∈ b, then branch b is closed.

Although, it does not concern relational constants indexed with P ∪Q, for P, Q ⊆ Par, it is sufficient for proving satisfaction in branch model property (Proposition 12.3.3). The reason being that the rules for these constants reflect their corresponding definitions in logic L.

Let L ∈ {L _FS , L _FW }. The branch structure determined by an open branch of an RL _L -proof tree is a structure ${\mathcal{M}}^{b} = ({U}^{b},{({R}_{P}^{b})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{m}^{b})$ satisfying the following conditions:

• ${U}^{b} ={ \mathbb{O}\mathbb{V}}_{\mathsf{R{L}_{L}}}$;

• m ^b(S) = { (x, y) ∈ U ^b ×U ^b : xSy ∉ b}, for every $S \in { \mathbb{R}\mathbb{V}}_{\mathsf{R{L}_{L}}} \cup \{ 1,1\prime\}$;

• ${R}_{\varnothing }^{b} = {m}^{b}({R}_{\varnothing }) =\{ (x,y) \in {U}^{b} \times {U}^{b} : x{R}_{\varnothing }y\not\in b\}$;

• ${R}_{\{p\}}^{b} = {m}^{b}({R}_{\{p\}}) =\{ (x,y) \in {U}^{b} \times {U}^{b} : x{R}_{\{p\}}y\not\in b\}$, for any p ∈ Par;

• For all $P,Q \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}$:

  $${R}_{P\cup Q}^{b} = {m}^{b}({R}_{ P\cup Q}) = \left \{\begin{array}{ll} {R}_{P}^{b} \cap {R}_{Q}^{b},&\mbox{ if $\mathsf{L} ={ \mathsf{L}}_{\mathsf{FS}}$} \\ {R}_{P}^{b} \cup {R}_{Q}^{b},&\mbox{ if $\mathsf{L} ={ \mathsf{L}}_{\mathsf{FW}}$;}\end{array} \right.$$

• m ^b extends to all the compound relational terms as in RL(1, 1′)-models.

As usual, valuation v ^b in ${\mathcal{M}}^{b}$ is the identity valuation.

Proposition 12.3.2 (Branch Model Property).

Let L ∈{L _FS ,L _FW } and let b be a complete branch of an RL _L -proof tree. Then ${\mathcal{M}}^{b}$ is an RL _L -model.

Proof.

By way of example, we show that if L-models satisfy the condition (Si) (resp. (Wi)), i ∈ { 1, 2}, then the branch model satisfies this condition as well. If conditions (S1) or (W1) are assumed, then these properties are satisfied due to the definition of the branch model. Assume that L-models satisfy the condition (S2). By the completion condition Cpl(rS2), for all object variables x, y ∈ U ^b, x − R _∅ y ∈ b. Therefore, for all object variables x, y ∈ U ^b, xR _∅ y ∉ b, thus (x, y) ∈ R _∅ ^b. Hence, the branch model satisfies the condition (S2). The proof for condition (W2) is similar. All the remaining conditions of RL _L-models are clearly satisfied by ${\mathcal{M}}^{b}$. □

If any local condition is assumed in RL _L-models, then we also need to show that ${\mathcal{M}}^{b}$ satisfies them.

Next, we show:

Proposition 12.3.3 (Satisfaction in Branch Model Property).

Let L ∈{L _FS ,L _FW } and let ${\mathcal{M}}^{b}$ be the branch model determined by an open branch b of an RL _L -proof tree. Then, for every RL _L -formula φ, if ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ , then φ∉b.

Proof.

By way of example, consider logic L _FS . Assume that the branch model satisfies a formula xR _{P ∪Q} y. By the definition of the branch model, (x, y) ∈ R _P ^b and (x, y) ∈ R _Q ^b. Suppose xR _{P ∪Q} y ∈ b. Then, by the completion condition Cpl(rS1 ⊇ ), either xR _P y ∈ b or xR _Q y ∈ b. By the induction hypothesis, either (x, y) ∉ R _P ^b or (x, y) ∉ R _Q ^b, a contradiction. □

Thus, we obtain:

Theorem 12.3.2(Soundness and Completeness of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$ and ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$).

Let L ∈{L _FS ,L _FW } and let φ be an RL _L -formula. Then, the following conditions are equivalent:

• 1. φ is RL _L -valid;

• 2. φ is true in all standard RL _L -models;

• 3. φ is RL _L -provable.

Recall that an RL _L model is standard whenever 1′ is interpreted as the identity. By the above theorem and Theorem 12.3.1, we get:

Theorem 12.3.3 (Relational Soundness and Completeness of Logics L _FS and L _FW ).

Let L ∈{L _FS ,L _FW } and let φ be an L-formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. φ is L-valid;

• 2. xτ(φ)y is RL _L -provable.

Example.

Consider an L _FS -formula φ and an L _FW -formula ψ:

$$\begin{array}{c} \varphi =\langle \!\langle {R}_{P\cup Q}\rangle \!\rangle p \rightarrow (\langle \!\langle {R}_{P}\rangle \!\rangle p \vee \langle \!\langle {R}_{Q}\rangle \!\rangle p),\\ \psi = [{R}_{\empty }](p \wedge \neg p). \end{array}$$

The translations of these formulas into relational terms are:

$$\begin{array}{c} \tau (\varphi ) = -(-{R}_{P\cup Q}\,;\,-T) \cup (-{R}_{P}\,;\,-T) \cup (-{R}_{Q}\,;\,-T), \\ \tau (\psi ) = -({R}_{\empty }\,;\,-(T \cap -T)), \end{array}$$

where for simplicity of notation τ(p) = T. L _FS -validity of φ is equivalent to ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{FS}}}$-provability of the formula xτ(φ)y. Its ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{FS}}}$-proof is presented in Fig. 12.1. L _FW -validity of ψ is equivalent to ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$-provability of the formula xτ(ψ)y. Its proof is presented in Fig. 12.2.

4 Relational Formalization of the Logic Rare-NIL

The second case study of Rare-logics is a relative version of the logic NIL, Rare-NIL. Let Par be a non-empty set of parameters. The vocabulary of the language of Rare-NIL consists of symbols from the following pairwise disjoint sets:

Fig. 12.1

A relational proof of L _FS -formula ⟨​⟨R _{P ∪Q} ⟩​⟩p → (⟨​⟨R _P ⟩​⟩p ∨ ⟨​⟨R _Q ⟩​⟩p)

Fig. 12.2

A relational proof of L _FW -formula [R _∅ ](p ∧ ¬p)

• $\mathbb{V}$ – a countable infinite set of propositional variables;

• $\{{\leq {}_{P}\}}_{P} \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$, $\{{\geq {}_{P}\}}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})}$, $\{{\sigma {}_{P}\}}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})}$ – three families of relational constants;

• ¬, ∨, ∧ } ∪{ [T] : T is a relational constant} – a set of propositional operations.

A Rare-NIL-model is a structure

$$\mathcal{M} = (U,{({\leq }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({\geq }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({\sigma }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m),$$

such that $(U,{({\#}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m)$ is an L _FS -model, for every # ∈ { ≤, ≥, σ}, and the following conditions are satisfied:

For every $P \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$ and for all x, y, z ∈ U,

• ${\leq }_{P} = {({\geq }_{P})}^{-1}$;

• ≤ _P is reflexive and transitive;

• σ _P is reflexive and symmetric;

• if (x, y) ∈ σ _P and (y, z) ∈ ≤ _P , then (x, z) ∈ σ _P .

Observe that the relations in Rare-NIL-models are constrained in two ways. The three families of relations satisfy the global conditions (S1) and (S2) and the local conditions analogous to the conditions in NIL-models.

In [DO07] it is shown that Rare-NIL-satisfiability (possibly) differs from NIL-satisfiability, namely we have:

Theorem 12.4.1.

• 1. Satisfiability problem of Rare- NIL is decidable;

• 2. Rare- NIL satisfiability is EXPTIME-complete.

The relational language corresponding to Rare-NIL-language is the RL(1, 1′)- language endowed with the set $\{{r{}_{P}\}}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})}$, r ∈ { ≤, ≥, σ} of relational constants. RL _Rare-NIL -models are structures of the form

$$\mathcal{M} = (U,{({\leq }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({\geq }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({\sigma }_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m),$$

such that (U, m) is an RL(1, 1′)-model, r _P = m(r _P ), for r ∈ { ≤, ≥, σ}, are binary relations on U indexed with finite subsets of the set Par, and moreover, relations r _P satisfy all the constraints assumed in Rare-NIL-models.

A dual tableau for Rare-NIL is constructed as in the case of the previous logics. Namely, to the RL(1, 1′)-dual tableau we add the rules corresponding to the global and local conditions assumed in this logic. More precisely, we add the following rules: For r ∈ { ≤, ≥, σ}, and for all $P,Q \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}$, the rules of the forms (rS1 ⊇ ), (rS1 ⊆ ), and (rS2) for the relational constants r _{P ∪Q} and r _∅ , respectively;For r ∈ { ≤, σ}, and for every $P \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}$, the rules (rI1 ⊆ ), (rI1 ⊇ ), (ref R), (tran R) for the relational constants ≤ _P and ≥ _P , and (ref R), (sym R), (rI6) for the relational constants σ _P ; these rules can be found in Sect. 11.4.By Theorem 11.4.2 and Proposition 12.3.1, it can be easily proved that all the specific RL _Rare-NIL -rules are RL _Rare-NIL -correct. Completeness can be proved in a similar way to completeness of RL _NIL -dual tableau and ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$-dual tableau. Thus, we obtain:

Theorem 12.4.2 (Soundness and Completeness of RL _Rare-NIL ).

For every RL _Rare-NIL -formula φ, the following conditions are equivalent:

• 1. φ is RL _Rare-NIL -valid;

• 2. φ is true in all standard RL _Rare-NIL -models;

• 3. φ is RL _Rare-NIL -provable.

By the above theorem and Theorems 11.4.1 and 12.3.1, we have:

Theorem 12.4.3 (Relational Soundness and Completeness of Rare-NIL).

For every Rare- NIL-formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is Rare- NIL-valid;

• 2. xτ(φ)y is RL _Rare-NIL -provable.

5 Relational Formalization of the Logic Rare-CI

Now, we consider a relational formalization of the logic of relative complementarity and incomplementarity, Rare-CI. The language of this logic is the multimodal language with the symbols from the following pairwise disjoint sets:

• $\mathbb{V}$ – a countable infinite set of propositional variables;

• $\{{R}_{P} : P \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}\} \cup \{ {S}_{P} : P \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}\}$ – the set of relational constants;

• $\{\neg,\vee,\wedge \}\cup \{ [{R}_{P}],[[{S}_{P}]] : P \in {\mathcal{P}}_{\mathit{fin}}\mbox{ (Par)}\}$ – the set of propositional operations.

A Rare-CI-model is a structure:

$$\mathcal{M} = (U,{({R}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({S}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m),$$

such that U is a non-empty set, R _P and S _P are binary relations on U indexed with finite subsets of Par, m is a meaning function such that for every $P \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$ the following conditions are satisfied:

• m(p) ⊆ U, for every propositional variable p;

• relations R _P satisfy the conditions (S1) and (S2), and relations S _P satisfy the conditions (W1) and (W2);

• R _P are symmetric and 3-transitive; these relations are counterparts to the strong complementarity relations derived from an information system;

• S _P are reflexive; these relations are counterparts to the weak incomplementarity relations derived from an information system;

• R _P ∪S _P = U ×U and R _P ∩ S _P = ∅.

It follows that relations R _P are strong relations and relations S _P are weak relations.

The relational language corresponding to Rare-CI-language is the RL(1, 1′)-language endowed with relational constants R _P and S _P , for $P\,\in \,{\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})\}$. RL _Rare-CI -models are structures of the form:

$$\mathcal{M} = (U,{({R}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},{({S}_{P})}_{P\in {\mathcal{P}}_{\mathit{ fin}}(\mbox{ Par})},m),$$

such that (U, m) is an RL(1, 1′)-model, R _P = m(R _P ) and S _P = m(S _P ) are binary relations on U indexed with finite subsets of a non-empty set Par, and moreover, relations R _P and S _P satisfy all the conditions assumed in Rare-CI-models.

A dual tableau for Rare-CI is constructed from the RL(1, 1′)-proof system. We add to it the rules corresponding to the global and local conditions assumed in Rare-CI-logic. Thus, the rules corresponding to the global conditions for relations R _P , $P \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$, are the instances of the rules of logic ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS}}}$, and the rules for relations S _P , $P \in {\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$, are the instances of the rules of logic ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FW}}}$. The rules reflecting the local conditions posed on relations R _P and S _P are those presented in Sect. 11.5 in the models of logic RL _CI .

RL _Rare-CI -axiomatic sets are those that include either of the following subsets:

For all object symbols x and y, and for every relational term T,

(Ax1) {xTy, x − Ty};

(Ax2) {xS _P x};

(Ax3) {xR _P y, xS _P y}.

By Propositions 11.5.1 and 12.3.1, we obtain:

Proposition 12.5.1.

• 1. The RL _Rare-CI -rules are RL _Rare-CI -correct;

• 2. The RL _Rare-CI -axiomatic sets are RL _Rare-CI -sets.

The completion conditions determined by the rules reflecting the global conditions are the instances of those presented in Sect. 12.3. The completion conditions determined by the rules that reflect the local conditions are the instances of those presented in Sect. 11.5.

The completeness proof is based on the same ideas as the completeness proofs of RL _CI , ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{FS}}}$, and ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{FW}}}$ dual tableaux. Namely, by Propositions 11.5.2 and 12.3.2, the branch model property holds. The satisfaction in branch model property is due to Proposition 12.3.3. Finally, by Theorems 11.5.2 and 12.3.2, we get:

Theorem 12.5.1 (Soundness and Completeness of RL _Rare-CI ).

Let φ be an RL _Rare-CI -formula. Then the following conditions are equivalent:

• 1. φ is RL _Rare-CI -valid;

• 2. φ is true in all standard RL _Rare-CI -models;

• 3. φ is RL _Rare-CI -provable.

By the above theorem and Theorems 11.5.1 and 12.3.1, we have:

Theorem 12.5.2 (Relational Soundness and Completeness of Rare-CI).

For every Rare- CI-formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is Rare- CI-valid;

• 2. xτ(φ)y is RL _Rare-CI -provable.

6 Relational Formalization of the Logic of Strong Complementarity Frames

Now, we present the relational formalization of the multimodal logic L _FS−COM based on a family FS−COM of complementarity frames. The logic L _FS−COM is defined as the L _FS -logic with the following additional semantic conditions: R _{p} is irreflexive, symmetric, and 3-transitive, for every parameter p ∈ Par. The same conditions are assumed in the models of the corresponding relational logic RL _FS−COM . A dual tableau for ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS-COM}}}$ includes all the rules and the axiomatic sets of the dual tableau for L _FS -logic presented in Sect. 12.3 and in addition the rules reflecting irreflexivity, symmetry, and 3-transitivity, for every relational constant R _{p}. The rule for symmetry can be found in Sect. 6.6 and the rule for 3-transitivity in Sect. 11.5. The rule reflecting irreflexivity of relation R has the following form:

For all object variables x and y,

$$(\mbox{ irref }R)\qquad \frac{} {xRy}$$

Example.

It is easy to show that in L _FS−COM -models a relation R _P is symmetric, for every $P\,\in \,{\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$. Therefore, the formula $x(-{R}_{P} \cup {R}_{P}^{-1})y$ is valid in all ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS-COM}}}$-models, for every $P\,\in \,{\mathcal{P}}_{\mathit{fin}}(\mbox{ Par})$. By way of example, in Fig. 12.3 we present an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS-COM}}}$-proof of the formula $x(-{R}_{\{p\}\cup \{q\}} \cup {R}_{\{p\}\cup \{q\}}^{-1})y$, for p, q ∈ Par.

Fig. 12.3

An ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{FS-COM}}}$-proof of symmetry of the relation R _{{p} ∪{q}}