Dual Tableaux for Logics of Classical Algebras of Binary Relations

Abstract

The first steps in developing a mathematical theory of binary relations were taken by Augustus De Morgan in 1864 [Mor64]. His work was based on an earlier development by George Boole[Boo47] of a calculus of sets understood as an algebra of logic. Next, the theory was extensively developed by Charles Sanders Peirce [Pei83] and Ernst Schröder [Sch91]. This early theory studied binary relations between elements of a set and their properties. The research was mainly concerned with the arithmetic of binary relations and the relational notions that are expressible as equations in the calculus of relations. Alfred Tarski [Tar41] proposed a modern reformulation of the calculus of binary relations as a theory of abstract algebras called relation algebras. A relation algebra is a kind of a join of a Boolean algebra and an involuted monoid. The monoid operation of product is an abstract counterpart of the composition of two relations, the involution models the operation of forming the converse of a relation, and the neutral element of the product corresponds to the identity relation. An extensive study of the theory of relation algebras and the recent developments can be found in [TG87, HH02, Mad06], among others.

1 Introduction

The first steps in developing a mathematical theory of binary relations were taken by Augustus De Morgan in 1864 [Mor64]. His work was based on an earlier development by George Boole[Boo47] of a calculus of sets understood as an algebra of logic. Next, the theory was extensively developed by Charles Sanders Peirce [Pei83] and Ernst Schröder [Sch91]. This early theory studied binary relations between elements of a set and their properties. The research was mainly concerned with the arithmetic of binary relations and the relational notions that are expressible as equations in the calculus of relations. Alfred Tarski [Tar41] proposed a modern reformulation of the calculus of binary relations as a theory of abstract algebras called relation algebras. A relation algebra is a kind of a join of a Boolean algebra and an involuted monoid. The monoid operation of product is an abstract counterpart of the composition of two relations, the involution models the operation of forming the converse of a relation, and the neutral element of the product corresponds to the identity relation. An extensive study of the theory of relation algebras and the recent developments can be found in [TG87, HH02, Mad06], among others.

Many theories from a variety of fields, in particular from computer science and logic, can be interpreted as theories of algebras of relations. The fundamental relational structure consisting of a Boolean algebra together with a monoid constitutes a common core of a great variety of these theories. In Parts II, III, IV, and V of this book the relational interpretability of theories is a basis for the construction of dual tableau systems for them in a systematic modular way.

In this chapter we present a basic logic of binary relations which provides a framework for the relational interpretation of the theories considered in the book. The logic can be viewed as a generic logic for the development of dual tableaux for these theories. The rules of the dual tableau of the basic relational logic are included in all the proof systems presented in the chapters of the parts of the book listed above. For each particular theory we need, first, to expand the basic relational logic with specific relational constants and/or operations satisfying the appropriate axioms which enable us to prove relational interpretability of the given theory. Next, a dual tableau of the basic relational logic is extended with the rules characterizing those specific constants and operations. The method of proving correctness and completeness of dual tableaux presented in this book follows the major steps of the corresponding proofs for the dual tableau of the basic relational logic. In this way, the developments of this chapter establish the tools for relational interpretability of theories and for construction of their relational proof systems.

Some other proof systems for relation algebras are presented in [Wad75, Hen80, Sch82, Mad83, Gor95, Gor97, Gor01].

2 Algebras of Binary Relations

The full algebra of binary relations on a set U is a structure of the form:

$$\mathfrak{R}(U) = (\mathcal{P}(U \times U),\cup, \cap, -,\varnothing, U \times U,\,;\,{,}^{-1},Id),$$

where $(\mathcal{P}(U \times U),\cup, \cap, -,\varnothing, U \times U)$ is the Boolean algebra of all the subsets of U ×U, ‘; ’ is the relative product of relations defined for all relations R, S on U as R ; S = { (x, y) ∈ U ×U : ∃z ∈ U (xRz ∧ zSy)}, ‘^{− 1}’ is the converse of relations defined as ${R}^{-1} =\{ (x,y) \in U \times U : yRx\}$, and Id is the identity on U, i.e., Id = { (x, x) : x ∈ U}.

A proper algebra of binary relations is an algebra $(W,\cup, \cap, -,\varnothing, 1,;{,}^{-1},1^{\prime})$ whose elements are binary relations, ∪, ∩, ;, ^{− 1}, ∅ are as above, 1 is an equivalence relation and the largest element of W, 1′ is the identity on the field of 1, and the complement operation ‘ − ’ is defined with respect to 1.

A generalization of algebras of binary relations is provided by the notion of relation algebra [Tar41].

A relation algebra is a structure of the form:

$$\mathfrak{A} = (W,+,\cdot, -,0,1,;,\breve{\;},1^{\prime}),\mbox{ where} :$$

• $(W,+,\cdot, -,0,1)$ is a Boolean algebra,

• ; is an associative binary operation that distributes over +, i.e., $(x + y)\,;\,z = x\,;\,z + y\,;\,z$ and $x\,;\,(y + z) = x\,;\,y + x\,;\,z$,

• $\breve{\;}$ is an unary operation that distributes over +, i.e., $(x + y)\breve{\;} = x\breve{\;} + y\breve{\;}$, and satisfies $(x\breve{\;})\breve{\;} = x$ and $(x\,;\,y)\breve{\;} = y\breve{\;}\,;\,x\breve{\;}$, for all x, y ∈ W,

• $1^{\prime}\,;\,x = x\,;\,1^{\prime} = x$, for every x ∈ W,

• $x\breve{\;};(-(x;y)) \leq -y$, for all x, y, z ∈ W.

The class of relation algebras is denoted by RA. Clearly, every algebra of binary relations is a relation algebra. The similarity type of relation algebras usually contains the three constants 0, 1, and 1′. However, 0 and 1 can be defined as $0\stackrel{\mathrm{df}}{=}1^{\prime} \cdot (-1^{\prime})$ and $1\stackrel{\mathrm{df}}{=}1^{\prime} + (-1^{\prime})$. We may also define $0^{\prime}\stackrel{\mathrm{df}}{=}-1^{\prime}$. The relation 0′ is called the diversity relation.

A relation algebra is said to be representable whenever it is isomorphic to a proper algebra of binary relations. The class of all representable relation algebras is denoted by RRA. There exist relation algebras $\mathfrak{A}$ (both finite and infinite) such that $\mathfrak{A} \in \mathsf{RA}$ and $\mathfrak{A}\not\in \mathsf{RRA}$. Such algebras can be found in [Lyn50]. Some representation theorems, where each algebra from the class RA is embeddable into an algebra which is not necessarily an algebra of binary relations, can be found in [Dun01a]. In that paper each element of a relation algebra is mapped into a set of binary relations, not necessarily to a single relation. It is known that RRA is not finitely axiomatizable. Moreover, an infinite axiomatization of RRA requires infinitely many relation variables [Mon64]. RRA is a variety with a recursively enumerable but undecidable equational theory.

A relation R on U is said to be a right (resp. left) ideal relation whenever R ; 1 = R (resp. 1 ; R = R). Right ideal relations play an important role in relational formalization of logics discussed in Parts III, IV, and V of the book. Various properties of right ideal relations are presented in the relevant chapters, see e.g., Propositions 7.4.1 and 16.4.1.

Proposition 2.2.1.

For all relations R,S ∈ ℜ(U), the following conditions are satisfied:

• 1. R ⊆ S iff $-R \cup S = 1,$

• 2. R = S iff $(-R \cup S) \cap (-S \cup R) = 1$,

• 3. R≠∅ iff 1 ; R ; 1 = 1,

• 4. R≠1 iff $1\,;\,(-R)\,;\,1 = 1$,

• 5. R = 1 and S = 1 iff R ∩ S = 1,

• 6. R = 1 or S = 1 iff $1\,;\,-(1\,;\,(-R)\,;\,1)\,;\,1 \cup S = 1$,

• 7. R = 1 implies S = 1 iff $(1\,;\,(-R)\,;\,1) \cup S = 1.$

Some arithmetic laws of relation algebras are collected in the following theorem:

Theorem 2.2.1.

The following are true in all relation algebras:

• 1. $r\,;\,0 = 0\,;\,r = 0,$

• 2. $1\breve{\;} = 1$,

• 3. 1 ; 1 = 1,

• 4. If r ≤ 1′, then $r\breve{\;} = r$,

• 5. If r,s ≤ 1′, then r ; s = r ⋅ s,

• 6. If r ≤ 1′, then (r ; 1) ⋅ s = r ; s and (1 ; r) ⋅ s = s ; r,

• 7. $(-r)\breve{\;} = -(r\breve{\;}),$

• 8. (r ⋅ s) ; t ≤ (r ; t) ⋅ (s ; t) and r ; (s ⋅ t) ≤ (r ; s) ⋅ (r ; t),

• 9. If t ≤ 1′, then (t ; r) ⋅ s = t ; (r ⋅ s) and (r ; t) ⋅ s = (r ⋅ s) ; t,

• 10. If s is right ideal, then r ⋅ s = (s ⋅ 1′) ; r,

• 11. If s is left ideal, then r ⋅ s = r ; (s ⋅ 1′).

Example.

We present two examples of relation algebras quoted from [Mad91]. The full algebra of binary relations on a three element set {0, 1, 2}, $\mathfrak{R}(\{0,1,2\})$, has 512 elements and 9 atoms. Its atoms are {(0, 0)}, {(0, 1)}, {(0, 2)}, {(1, 0)}, {(1, 1)}, {(1, 2)}, {(2, 0)}, {(2, 1)}, and {(2, 2)}.

The pentagonal relation algebra $\mathfrak{B}$ has three atoms 1′, a, and b. The elements of $\mathfrak{B}$ are $0,1^{\prime},a,b,1^{\prime} + b = -a,1^{\prime} + a = -b,a + b = 0^{\prime}$, and $1 = 1^{\prime} + a + b$. The compositions of atoms are given in Table 2.1. This table determines all the compositions of elements of $\mathfrak{B}$, since every element is a join of atoms and the composition ; distributees over +.

The algebra $\mathfrak{B}$ is representable, that is it can be embedded in some $\mathfrak{R}(U)$. It turns out that this is possible only if card(U) = 5. A copy of $\mathfrak{B}$ inside $\mathfrak{R}(\{0,\ldots, 4\})$ can be defined as follows:

$$\begin{array}{rcl} 1^{\prime}& =& \{(0,0),(1,1),(2,2),(3,3),(4,4)\}; \\ a& =& \{(0,1),(1,0),(1,2),(2,1),(2,3),(3,2),(3,4),(4,3),(4,0),(0,4)\}; \\ b& =& \{(0,2),(2,0),(1,3),(3,1),(2,4),(4,2),(3,0),(0,3),(4,1),(1,4)\}.\end{array}$$

A picture of this representation in Fig. 2.1 shows a as a pentagon and b as a pentagram.

Table 2.1 Compositions of atoms of the pentagonal algebra

3 Logics of Binary Relations

In this chapter we present a general form of logics of binary relations considered in the book. There are two kinds of expressions of relational languages: terms and formulas.Terms represent relations and formulas express the facts that a pair of objects belongs to a relation.

Fig. 2.1

Representation of the pentagonal algebra

Most of the relational logics of binary relations considered in the book are defined according to the following scheme. The vocabulary of the language of a relational logic L consists of the symbols from the following pairwise disjoint sets:

• ${\mathbb{O}\mathbb{V}}_{\mathsf{L}}$ – a countable infinite set of object variables;

• ${\mathbb{O}\mathbb{C}}_{\mathsf{L}}$ – a countable (possibly empty) set of object constants;

• ${\mathbb{R}\mathbb{V}}_{\mathsf{L}}$ – a countable infinite set of binary relational variables;

• ${\mathbb{R}\mathbb{C}}_{\mathsf{L}}$ – a countable (possibly empty) set of binary relational constants;

• A set of relational operations including the standard operations −, ∪, ∩, ;, and ^{− 1}.

Object constants are needed for relational representation of theories in Chap. 3, Chap. 15, and Sect. 16.5. Relational representations of all the theories of Parts III, IV, and V require specific relational constants.

The set ${\mathbb{R}\mathbb{A}}_{\mathsf{L}} ={ \mathbb{R}\mathbb{V}}_{\mathsf{L}} \cup { \mathbb{R}\mathbb{C}}_{\mathsf{L}}$ is called the set of atomic relational terms. The set ${\mathbb{O}\mathbb{S}}_{\mathsf{L}} ={ \mathbb{O}\mathbb{V}}_{\mathsf{L}} \cup { \mathbb{O}\mathbb{C}}_{\mathsf{L}}$ is called the set of object symbols. The set ${\mathbb{R}\mathbb{T}}_{\mathsf{L}}$ of relational termsis the smallest (with respect to inclusion) set of expressions that includes all the atomic relational terms and is closed with respect to all the relational operations. L-formulas are of the form xRy, where $x,y \in { \mathbb{O}\mathbb{S}}_{\mathsf{L}}$ and $R \in { \mathbb{R}\mathbb{T}}_{\mathsf{L}}$. An L-formula xRy is said to be atomic whenever $R \in { \mathbb{R}\mathbb{A}}_{\mathsf{L}}$.

With an L-language a class of L-structures is associated. An L-structure has the form $\mathcal{M} = (U,m)$, where U is a non-empty set and m is a meaning function which assigns:

• (m1) Elements of U to object constants, that is m(c) ∈ U, for every $c \in { \mathbb{O}\mathbb{C}}_{\mathsf{L}}$;

• (m2) Binary relations on U to atomic relational terms, that is m(R) ⊆ U ×U, for every $R \in { \mathbb{R}\mathbb{A}}_{\mathsf{L}}$.

m extends to all the compound relational terms, in particular:

• (m3) $m(-R) = (U \times U) \setminus m(R)$;

• (m4) m(R ∪S) = m(R) ∪m(S);

• (m5) m(R ∩ S) = m(R) ∩ m(S);

• (m6) $m({R}^{-1}) = {(m(R))}^{-1}$= {(x, y) ∈ U ×U : (y, x) ∈ m(R)};

• (m7) $m(R\,;\,S) = m(R)\,;\,m(S) =\{ (x,y) \in U \times U : \exists z \in U,\ (x,z) \in m(R)\mbox{ and }(z,y) \in m(S)\}$.

So, for L-structures we only require that object constants are interpreted as elements of their universes, relational constants are interpreted as binary relations, and standard relational operations receive their usual meaning.

L-models are L-structures, where meaning function m satisfies the conditions specific for logic L. The conditions concern interpretation of relational operations specific for the given logic and/or interpretation of specific relational and/or object constants of the logic. Relational logics considered in the book are always defined in terms of their languages and the classes of models.

In order to avoid a confusion between syntactic objects in the languages of theories and semantic constraints on relations in the models of the theories, we write xRy for the former, where x, y are object symbols and R is a relational term of a language, and (x, y) ∈ R for the latter, where x and y are objects from the universe of a model and R is a relation in the model.

Let $\mathcal{M} = (U,m)$ be an L-structure. A valuation in $\mathcal{M}$ is any function $v\,: \,{\mathbb{O}\mathbb{S}}_{\mathsf{L}}\,\rightarrow \,U$ such that v(c) = m(c), for every $c \in { \mathbb{O}\mathbb{C}}_{\mathsf{L}}$. Satisfaction of an L-formula xRy by a valuation v in an L-structure $\mathcal{M}$ is defined as:

• $\mathcal{M},v\models xRy$ iff (v(x), v(y)) ∈ m(R).

An L-formula xRy is true in $\mathcal{M}$ whenever it is satisfied by all the valuations in $\mathcal{M}$. If $\mathcal{K}$ is a class of L-structures, then an L-formula xRy is said to be $\mathcal{K}$ -valid whenever it is true in every structure of $\mathcal{K}$, and it is L-valid whenever it is true in all L-models.

Fact 2.3.1.

Let L and L′ be relational logics such that every L-structure is an L′-structure. Then for any relational formula xRy, if xRy is L′-valid, then it is L-valid.

4 Relational Dual Tableaux

Relational dual tableaux are founded on the Rasiowa–Sikorski system for the first-order logic presented in Chap. 1. They are powerful tools for performing the four major reasoning tasks: verification of validity, verification of entailment, model checking, and verification of satisfaction. Relational proof systems are determined by their axiomatic sets of formulas and rules which most often apply to finite sets of relational formulas. Some relational proof systems with infinitary rules are known in the literature (see Sect. 19.2), but in the present chapter we confine ourselves to finitary rules only. The axiomatic sets take the place of axioms. The rules are intended to reflect properties of relational operations and constants. There are two groups of rules: decomposition rules and specific rules. Given a formula, the decomposition rules of the system enable us to transform it into simpler formulas, or the specific rules enable us to replace a formula by some other formulas. The rules have the following general form:

$$\mbox{ (rule)}\qquad \frac{\Phi (\overline{x})} {{\Phi }_{1}({\overline{x}}_{1},{\overline{u}}_{1},{\overline{w}}_{1})\,\vert \,\ldots \,\vert \,{\Phi }_{n}({\overline{x}}_{n},{\overline{u}}_{n},{\overline{w}}_{n})}$$

where $\Phi (\overline{x})$ is a finite (possibly empty) set of formulas whose object symbols are among the elements of set$(\overline{x})$, where $\overline{x}$ is a finite sequence of object symbols and set$(\overline{x})$ is a set of elements of sequence $\overline{x}$; every ${\Phi }_{j}({\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j})$, 1 ≤ j ≤ n, is a finite non-empty set of formulas, whose object symbols are among the elements of $\mbox{ set}({\overline{x}}_{j}) \cup \mbox{ set}({\overline{u}}_{j}) \cup \mbox{ set}({\overline{w}}_{j})$, where ${\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j}$ are finite sequences of object symbols such that $\mbox{ set}({\overline{x}}_{j}) \subseteq \mbox{ set}(\overline{x})$, $\mbox{ set}({\overline{u}}_{j})$ consists of the variables that may be instantiated to arbitrary object symbols when the rule is applied (usually to the object symbols that appear in the set to which the rule is being applied), $\mbox{ set}({\overline{w}}_{j})$ consists of the variables that must be instantiated to pairwise distinct new variables (not appearing in the set to which the rule is being applied) and distinct from any variable of sequence ${\overline{u}}_{j}$. A rule of the form (rule) is the n-fold branching rule, where the jth successor of $\Phi (\overline{x})$ is the set ${\Phi }_{j}({\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j})$. A rule of the form (rule) is applicable to a finite set X of formulas whenever $\Phi (\overline{x}) \subseteq X$. As a result of an application of a rule of the form (rule) to set X, we obtain the sets $(X \setminus \Phi (\overline{x})) \cup {\Phi }_{j}({\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j})$, j ∈ { 1, …, n}. A set to which a rule has been applied is called the premise of the rule, and the sets obtained by an application of the rule are called its conclusions.

Let L be a relational logic. A finite set {φ₁, …, φ _n } of L-formulas is said to be an L-setwhenever for every L-model $\mathcal{M}$ and for every valuation v in $\mathcal{M}$ there exists i ∈ { 1, …, n} such that φ _i is satisfied by v in $\mathcal{M}$. It follows that the first-order disjunction of all the formulas from an L-set is valid in first-order logic. A rule of the form (rule) is L-correct whenever for every finite set X of L-formulas, $X \cup \Phi (\overline{x})$ is an L-set if and only if $X \cup {\Phi }_{j}({\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j})$ is an L-set, for every j ∈ { 1, …, n}, i.e., the rule preserves and reflects validity. If $\mathcal{K}$ is a class of L-structures, then we define the notion of a $\mathcal{K}$-set and the notion of $\mathcal{K}$-correctness in a similar way. A finite set of L-formulas {φ₁, …, φ _n } is said to be a $\mathcal{K}$ -set whenever for every $\mathcal{K}$-structure $\mathcal{M}$ and for every valuation v in $\mathcal{M}$ there exists i ∈ { 1, …, n} such that φ _i is satisfied by v in $\mathcal{M}$. A rule of the form (rule) is $\mathcal{K}$ -correctwhenever for every finite set X of L-formulas, $X \cup \Phi (\overline{x})$ is a $\mathcal{K}$-set if and only if $X \cup {\Phi }_{j}({\overline{x}}_{j},{\overline{u}}_{j},{\overline{w}}_{j})$ is a $\mathcal{K}$-set, for every j ∈ { 1, …, n}.

Let xRy be an L-formula. The notion of an L-proof treeis defined in a similar way as in logic F in Sect. 1.3, that is an L-proof tree for xRy is a tree with the following properties:

• The formula xRy is at the root of the tree;

• Each node except the root is obtained by an application of an L-rule to its predecessor node;

• A node does not have successors whenever its set of formulas is an L-axiomatic set or none of the rules is applicable to its set of formulas.

Similarly as in the dual tableau for logic F, a branchof an L-proof tree is said to be closedwhenever it contains a node with an L-axiomatic set of formulas. A tree is closed whenever all of its branches are closed. An L-formula xRy is L-provablewhenever there is a closed L-proof tree for it which is then refereed to as its L-proof.

5 A Basic Relational Logic

The logic RL presented in this section is a common core of all the logics of binary relations presented in this book. RL represents, in fact, a family of logics which possibly differ in the object constants admitted in their languages. We do not assume here any specific properties of these constants, so all the developments of this section are relevant for any such logic. Throughout the book, by RL-logic we shall mean any logic from this family. The language of RL-logic is defined as in Sect. 2.3 with:

• ${\mathbb{R}\mathbb{C}}_{\mathsf{RL}} = \varnothing$;

• The relational operations are −, ∪, ∩, ;, ^{− 1}.

RL-models coincide with the RL-structures defined in Sect. 2.3 adjusted to the RL-language.

An RL-dual tableau consists of decomposition rules and axiomatic sets. Decomposition rules have the following forms:

For any object symbols x and y and for any relational terms R and S,

$$\begin{array}{llllll}(\cup) &\frac{x(R \cup S)y}{xRy,xSy} \qquad (-\cup) \quad \frac{x-(R \cup S)y}{x-Ry\;\vert \;x-Sy} \\(\cap ) &\frac{x(R \cap S)y}{xRy\,\vert \,xSy}\qquad (-\cap )\,\quad \frac{x-(R \cap S)y}{x-Ry,x-Sy} \\ (-) \quad \frac{x\hbox{--}Ry}{xRy}\\ (^{-1})&\frac{x{R}^{-1}y}{yRx} \qquad ({-}^{-1}) \quad \frac{x-{R}^{-1}y}{y-Rx} \\ (;) & \frac{x(R\,;\,S)y} {xRz,x(R\,;\,S)y\,\vert \,zSy,x(R\,;\,S)y}\,\qquad \,z\,\mbox{is any object symbol}\\ (-;)& \frac{x-(R\,;\,S)y} {x-Rz,z-Sy}\, \qquad \,z\,\mbox{is a new object variable}\end{array}$$

A set of RL-formulas is said to be an RL-axiomatic set whenever it includes a subset of the following form:

(Ax) {xRy, x − Ry}, where x, y are object symbols and R is a relational term.

Most of relational logics of binary relations studied in the book are obtained from RL by postulating some constraints on their object and/or relational constants. Dual tableaux for these logics include the decomposition rules of RL-dual tableau, where in each particular logic L the terms and object symbols range over the corresponding entities of the language of L. Specific rules reflect the properties of constants assumed in the L-language in question. In all relational dual tableaux considered in the book the sets including a subset of the form (Ax) are assumed to be L-axiomatic sets.

Proposition 2.5.1.

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

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

Proof.

By way of example, we prove correctness of the rules (; ) and ( − ; ). Let X be a finite set of RL-formulas.

(; ) Clearly, if X ∪{ x(R ; S)y} is an RL-set, then so are X ∪{xRz, x(R ; S)y}, X ∪{zSy, x(R ; S)y}. Assume X ∪{xRz, x(R ; S)y} and X ∪{ zSy, x(R ; S)y} are RL-sets, and suppose X ∪{ x(R ; S)y} is not an RL-set. Then there exist an RL-model $\mathcal{M} = (U,m)$ and a valuation v in $\mathcal{M}$ such that for every φ ∈ X ∪{x(R ; S)y}, $\mathcal{M},v\nvDash \varphi$. It follows that for every a ∈ U, (v(x), a) ∉ m(R) or (a, v(y)) ∉ m(S). However, by the assumption, model $\mathcal{M}$ and valuation v satisfy (v(x), v(z)) ∈ m(R) and (v(z), v(y)) ∈ m(S), a contradiction.

( − ; ) Assume X ∪{x − (R ; S)y} is an RL-set. Suppose $X \cup \{ x-Rz,z-Sy\}$ is not an RL-set, where z does not occur in X and z≠x, y. Then there exist an RL-model $\mathcal{M} = (U,m)$ and a valuation v in $\mathcal{M}$ such that for every $\varphi \in X \cup \{ x-Rz,z-Sy\}$, $\mathcal{M},v\nvDash \varphi$. Thus, (v(x), v(z)) ∈ m(R) and (v(z), v(y)) ∈ m(S). However, by the assumption, for every a ∈ U, (v(x), a) ∉ m(R) or (a, v(y)) ∉ m(S), a contradiction. Now, assume $X \cup \{ x-Rz,z-Sy\}$ is an RL-set. Then, by the assumption on variable z, for every RL-model $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$, either there exists φ ∈ X such that $\mathcal{M},v\models \varphi$ or for every a ∈ U, either (v(x), a) ∉ m(R) or (a, v(y)) ∉ m(S). That is for every RL-model $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$ either there exists φ ∈ X such that $\mathcal{M},v\models \varphi$ or $\mathcal{M},v\models x-(R\,;\,S)y$. Hence, X ∪{x − (R ; S)y} is an RL-set. □

Due to the above proposition, we obtain:

Proposition 2.5.2.

Let φ be an RL-formula. If φ is RL-provable, then it is RL-valid.

A branch b of an RL-proof tree is said to be complete whenever it is closed or it satisfies the following RL-completion conditions: For all object symbols x and y and for all relational terms R and S, Cpl( ∪) (resp. Cpl( − ∩ )) If x(R ∪S)y ∈ b (resp. x − (R ∩ S)y ∈ b), then both xRy ∈ b (resp. x − Ry ∈ b) and xSy ∈ b (resp. x − Sy ∈ b), obtained by an application of the rule ( ∪) (resp. ( − ∩ ));Cpl( ∩ ) (resp. Cpl( − ∪)) If x(R ∩ S)y ∈ b (resp. x − (R ∪S)y ∈ b), then either xRy ∈ b (resp. x − Ry ∈ b) or xSy ∈ b (resp. x − Sy ∈ b), obtained by an application of the rule ( ∩ ) (resp. ( − ∪)); Cpl( − ) If $x(\hbox{--}R)y \in b$, then xRy ∈ b, obtained by an application of the rule ( − ); Cpl(^{− 1}) If xR ^{− 1} y ∈ b, then yRx ∈ b, obtained by an application of the rule (^{− 1}); Cpl(${-}^{-1})$ If $x-{R}^{-1}y \in b$, then y − Rx ∈ b, obtained by an application of the rule $({-}^{-1})$; Cpl(; ) If x(R ; S)y ∈ b, then for every object symbol z, either xRz ∈ b or zSy ∈ b, obtained by an application of the rule (; );Cpl( − ; ) If x − (R ; S)y ∈ b, then for some object variable z, both x − Rz ∈ b and z − Sy ∈ b, obtained by an application of the rule ( − ; ).An RL-proof tree is said to be complete if and only if all of its branches are complete. A complete non-closed branch of an RL-proof tree is said to be open.Note that every RL-proof tree can be extended to a complete RL-proof tree, i.e., for every RL-formula φ there exists a complete RL-proof tree for φ Due to the forms of RL-decomposition rules, Fact 1.3.1 and Proposition 1.3.3 transfer to logic RL.

Fact 2.5.1.

If a node of an RL-proof tree contains an RL-formula xRy or x−Ry, for an atomic R, then all of its successors contain this formula as well.

This property will be referred to as preservation of formulas built with atomic terms or their complements.

Proposition 2.5.3.

For every branch b of an RL-proof tree and for every atomic term R, if xRy ∈ b and x−Ry ∈ b, then b is closed.

We can prove a stronger form of Proposition 2.5.3:

Proposition 2.5.4.

Let b be a complete branch of an RL-proof tree. If there is a relational term R such that xRy ∈ b and x−Ry ∈ b, then b is closed.

Proof.

Clearly, if branch b is closed, then the proposition holds. Assume that branch b is open. The proof of the proposition is by induction on the complexity of relational terms. For atomic relational terms the statement holds due to Proposition 2.5.3. By way of example, we prove the statement for terms of the form R ; S. Suppose x(R ; S)y and x − (R ; S)y belong to b, for some relational terms R and S, and some object symbols x and y. Since x − (R ; S)y ∈ b, by the completion condition Cpl( − ; ), both x − Rz ∈ b and z − Sy ∈ b, for some object variable z. Furthermore, since x(R ; S)y ∈ b, by the completion condition Cpl(; ), for every object variable z, either xRz ∈ b or zSy ∈ b. Thus either both xRz and x − Rz belong to b or both zSy and z − Sy belong to b. Hence, by the induction hypothesis, b is closed. □

In order to prove completeness of RL-dual tableau, first, we construct a branch structure ${\mathcal{M}}^{b} = ({U}^{b},{m}^{b})$ determined by an open branch b of a complete RL-proof tree as follows:

• ${U}^{b} ={ \mathbb{O}\mathbb{S}}_{\mathsf{RL}}$;

• m ^b(c) = c, for every $c \in { \mathbb{O}\mathbb{C}}_{\mathsf{RL}}$;

• m ^b(R) = {(x, y) ∈ U ^b ×U ^b : xRy ∉ b}, for every relational variable R;

• m ^b extends to all the compound relational terms as in the RL-models.

Directly from this definition, we obtain:

Fact 2.5.2.

For every open branch b of an RL-proof tree, ${\mathcal{M}}^{b}$ is an RL-model.

Any structure ${\mathcal{M}}^{b}$ is referred to as an RL-branch model. Let ${v}^{b}:{ \mathbb{O}\mathbb{S}}_{\mathsf{RL}} \rightarrow {U}^{b}$ be a valuation in ${\mathcal{M}}^{b}$ such that v ^b(x) = x, for every $x \in { \mathbb{O}\mathbb{S}}_{\mathsf{RL}}$.

Proposition 2.5.5.

For every open branch b of an RL-proof tree and for every RL-formula φ, if ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ , then φ∉b.

Proof.

The proof is by induction on the complexity of formulas.

Let φ = xRy be an atomic RL-formula. Assume that ${\mathcal{M}}^{b},{v}^{b}\models xRy$, that is (x, y) ∈ m ^b(R). By the definition of the branch model xRy ∉ b. Let $R \in { \mathbb{R}\mathbb{V}}_{\mathsf{RL}}$ and ${\mathcal{M}}^{b},{v}^{b}\models x-Ry$, that is (x, y) ∉ m ^b(R). Therefore xRy ∈ b. Then, by Proposition 2.5.3, x − Ry ∉ b, for otherwise b would be closed.

Let ${\mathcal{M}}^{b},{v}^{b}\models x(S\,;\,T)y$. Then (x, y) ∈ m ^b(S ; T), that is there exists an object symbol z ∈ U ^b such that (x, z) ∈ m ^b(S) and (z, y) ∈ m ^b(T). By the induction hypothesis, xSz ∉ b and zTy ∉ b. Suppose x(S ; T)y ∈ b. By the completion condition Cpl(; ), for every object symbol z ∈ U ^b, either xSz ∈ b or zTy ∈ b, a contradiction.

Let ${\mathcal{M}}^{b},{v}^{b}\models x-(S\,;\,T)y$. Then (x, y) ∉ m ^b(S ; T), that is for every object symbol z ∈ U ^b, either (x, z) ∉ m ^b(S) or (z, y) ∉ m ^b(T). Suppose that x − (S ; T)y ∈ b. By the completion condition Cpl( − ; ), for some object variable z ∈ U ^b, both x − Sz ∈ b and z − Ty ∈ b. By the induction hypothesis, (x, z) ∈ m ^b(S) and (z, y) ∈ m ^b(T), a contradiction.

The proofs of the remaining cases are similar. □

Fact 2.5.2 and Proposition 2.5.5 enable us to prove:

Proposition 2.5.6.

Let φ be an RL-formula. If φ is RL-valid, then φ is RL-provable.

Proof.

Assume φ is RL-valid. Suppose there is no any closed RL-proof tree for φ. Then there exists a complete RL-proof tree for φ with an open branch, say b. Since φ ∈ b, by Proposition 2.5.5, φ is not satisfied by valuation v ^b in the branch model ${\mathcal{M}}^{b}$. Hence φ is not RL-valid, a contradiction. □

By Propositions 2.5.2 and 2.5.6, we have:

Theorem 2.5.1 (Soundness and Completeness of RL).

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

• 1. φ is RL-valid;

• 2. φ is RL-provable.

Example.

We show that (R ∩ S) ; T ⊆ (R ; T) ∩ (S ; T) by proving the formula:

$$x(-((R \cap S)\,;\,T) \cup ((R\,;\,T) \cap (S\,;\,T)))y.$$

Figure 2.2 presents its RL-proof.

Fig. 2.2

An RL-proof of (R ∩ S) ; T ⊆ (R ; T) ∩ (S ; T)

6 A Method of Proving Soundness and Completeness of Relational Dual Tableaux

The method applied to proving soundness and completeness of RL-dual tableau determines a paradigm for all the soundness and completeness proofs presented in this book.

Let L be a relational logic. In order to prove that an L-provable formula is L-valid it suffices to show that all the rules of an L-dual tableau are L-correct and all the axiomatic sets are L-sets. In some cases we also show correspondences between the semantic constraints posed on relational constants and/or relational operations and the rules and/or axiomatic sets reflecting those constraints. More precisely, we say that a rule (resp. an axiomatic set) of an L-dual tableau reflects a constraint assumed in L-models whenever for every class $\mathcal{K}$ of L-structures, $\mathcal{K}$-correctness of the rule (resp. $\mathcal{K}$-validity of the axiomatic set) implies that every structure from $\mathcal{K}$ satisfies the constraint.

In order to prove that an L-valid formula has an L-proof, we suppose that the formula does not have any L-proof. It follows that there exists a complete L-proof tree for this formula with an open branch b. Then we construct a branch structure ${\mathcal{M}}^{b} = ({U}^{b},{m}^{b})$ determined by b, where U ^b consists of all the object symbols of L-language and m ^b is the meaning function which assigns relations to atomic relational terms and extends homomorphically to all the terms as in RL-models. Most often the meaning function m ^b of ${\mathcal{M}}^{b}$ is defined by:

$m^{b}(R)\stackrel{\mathrm{df}}{=}\{(x,y)\in\,U^{b}\times U^{b}: xRy\in\,b\}.$

In that case we will say that ${\mathcal{M}}^{b}$ is defined in a standard way.We define the valuation v ^b in the model ${\mathcal{M}}^{b}$ as the identity function, i.e., v ^b(x) = x for every object symbol x.

Then the major steps of the proof are the propositions showing the following three properties:

• (1) Closed Branch Property: For any branch of an L-proof tree, if xRy and x − Ry, for an atomic term R, belong to the branch, then the branch can be closed.

• (2) Branch Model Property: Let ${\mathcal{M}}^{b}$ be a branch structure determined by an open branch b of an L-proof tree. Then ${\mathcal{M}}^{b}$ is an L-model.

• (3) Satisfaction in Branch Model Property: For every L-formula φ and for every open branch b of an L-proof tree for φ, the branch model ${\mathcal{M}}^{b}$ and valuation v ^b in ${\mathcal{M}}^{b}$ satisfy:

  $$\mbox{ If }{\mathcal{M}}^{b},{v}^{b}\models \varphi, \mbox{ then }\varphi \not\in b.$$

Then we reason as in the proof of Proposition 2.5.6.

Roughly speaking, the method can be successfully applied provided that the following conditions will be satisfied: a sufficient condition for (1) is the preservation of formulas built with atomic terms or their complements by the applications of the rules; for (2), the L-dual tableau must have enough rules in order to reflect all the semantic properties of relational constants and relational operations of the L-language; for (3), the branch structure must provide a model that falsifies the non-provable formulas.

7 Relational Logic with Relations 1 and 1′

The logic considered in this section is obtained from RL-logic by expanding its language with constants 1 and 1′. The vocabulary of the language of RL(1, 1′)-logic is defined as in Sect. 2.3 with:

• ${\mathbb{R}\mathbb{C}}_{\mathsf{RL}(1,1^{\prime})} =\{ 1,1^{\prime}\}$.

An RL(1, 1′)-structure is an RL-model $\mathcal{M} = (U,m)$ such that m(1) and m(1′) are binary relations on U. An RL(1, 1′)-model is an $\mathsf{RL}(1,1^{\prime})$-structure $\mathcal{M} = (U,m)$ such that the following conditions are satisfied:

• m(1) = U ×U;

• m(1′) is an equivalence relation on U;

• $m(1^{\prime})\,;\,m(R) = m(R)\,;\,m(1^{\prime}) = m(R)$, for every atomic relational term R (extensionality);

• m extends to all the compound relational terms as in RL-models.

Proposition 2.7.1.

Let $\mathcal{M} = (U,m)$ be an RL(1,1′)-model. Then, for every relational term R of RL(1,1′)-language, the extensionality property holds:

$$m(1^{\prime})\,;\,m(R) = m(R)\,;\,m(1^{\prime}) = m(R).$$

Proof.

The proof is by induction on the complexity of relational terms. By way of example, we show the extensionality property for $R = -S$. Since m(1′) is reflexive, $m(-S) \subseteq m(1^{\prime})\,;\,m(-S)$. For ⊇, assume that there exists z ∈ U such that (x, z) ∈ m(1′) and (z, y) ∉ m(S). By the induction hypothesis, for every u ∈ U, (z, u) ∉ m(1′) or (u, y) ∉ m(S). In particular, (z, x) ∉ m(1′) or (x, y) ∉ m(S). Since m(1′) is symmetric, (x, y) ∈ m( − S).

The equality $m(-S) = m(-S)\,;\,m(1^{\prime})$ can be proved in a similar way. The extensionality condition for the terms built with ∪, ∩, ;, and ^{− 1} follows easily from the definition of the meaning function, properties of relational operations, and the induction hypothesis. □

Proposition 2.7.2.

Let $\mathcal{M} = (U,m)$ be an RL(1,1′)-structure satisfying the following conditions:

• 1. m(1) = U × U;

• 2. m(1′) is reflexive;

• 3. $m(1^{\prime})\,;\,m(R) = m(R)\,;\,m(1^{\prime}) = m(R)$ , for every relational term R.

Then $\mathcal{M}$ is an RL(1,1′)-model.

Proof.

Since m(1′) is reflexive, so is m(1′ ^{− 1}). Thus m(1′) ⊆ m(1′ ^{− 1}) ; m(1′). By 3., $m({1^{\prime}}^{-1})\ ;\ m(1^{\prime})\,=\,m({1^{\prime}}^{-1})$. Therefore m(1′) is symmetric. Transitivity follows directly from 3. □

It follows that an equivalent set of conditions characterizing the RL(1, 1′)-models could be reflexivity of m(1′) and the extensionality property for all the relational terms.

An RL(1, 1′)-model $\mathcal{M} = (U,m)$ is said to be standard whenever m(1′) is the identity on U, that is m(1′) = { (x, x) : x ∈ U}.

Fact 2.7.1.

If a formula is RL(1,1′)-valid, then it is true in all standard RL(1,1′)-models.

RL(1, 1′)-dual tableau includes the decomposition rules of RL-dual tableau (see Section 2.5) adjusted to RL(1, 1′)-language and the specific rules of the following forms:

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

$$\begin{array}{lll} (1^{\prime}1)\,&\, \frac{xRy} {xRz,xRy\,\vert \,y1^{\prime}z,xRy}\,&\,\mbox{ z is any object symbol } \\ (1^{\prime}2)\,&\, \frac{xRy} {x1^{\prime}z,xRy\,\vert \,zRy,xRy}\,&\,\mbox{ z is any object symbol } \\ \end{array}$$

The rule (1′1) reflects symmetry, transitivity, and the part m(R) ; m(1′) ⊆ m(R) of the extensionality property of 1′. The rule (1′2) reflects the part m(1′) ; m(R) ⊆ m(R) of extensionality property of 1′. The formal presentation of these facts is given in Theorem 2.7.1.

A finite set of formulas is said to be RL(1, 1′)-axiomatic whenever it is an RL-axiomatic set adjusted to R(1, 1′)-language or it includes either of the sets of the following forms:

For all object symbols x and y,

• (Ax1) {x1′x};

• (Ax2) {x1y}.

The axiomatic set {x1′x} reflects reflexivity of 1′.

Theorem 2.7.1 (Correspondence).

Let $\mathcal{K}$ be a class of RL(1,1′)-structures. Then the following conditions are equivalent:

• 1. $\mathcal{K}$ is a class of RL(1,1′)-models;

• 2. The RL(1,1′)-axiomatic sets (Ax1) and (Ax2) are $\mathcal{K}$ -sets and the rules (1′1) and (1′2) are $\mathcal{K}$ -correct.

Proof.

(1. → 2. ) Let $\mathcal{K}$ be a class of RL(1, 1′)-models. Since m(1) = U ×U, every superset of {x1y} is an RL(1, 1′)-set. Furthermore, since m(1′) is reflexive, X ∪{x1′x} is a $\mathcal{K}$-set, for every finite set X of RL(1, 1′)-formulas.

Now, we prove that the rule (1′1) is $\mathcal{K}$-correct. Let X be a finite set of RL(1, 1′)-formulas. It is easy to see that if X ∪{xRy} is a $\mathcal{K}$-set, then so are X ∪{xRz, xRy} and X ∪{ y1′z, xRy}. Now, assume X ∪{xRz, xRy} and X ∪{ y1′z, xRy} are $\mathcal{K}$-sets. Suppose X ∪{xRy} is not a $\mathcal{K}$-set, that is there exist an RL(1, 1′)-model $\mathcal{M}$ in $\mathcal{K}$ and a valuation v in $\mathcal{M}$ such that for every formula φ ∈ X ∪{ xRy}, $\mathcal{M},v\nvDash \varphi$, in particular $\mathcal{M},v\nvDash xRy$. Then, by the assumption and since m(1′) is symmetric, $\mathcal{M},v\models xRz$ and $\mathcal{M},v\models z1^{\prime}y$, that is (v(x), v(z)) ∈ m(R) and (v(z), v(y)) ∈ m(1′). Since m(R) ; m(1′) ⊆ m(R), (v(x), v(y)) ∈ m(R). Hence, $\mathcal{M},v\models xRy$, a contradiction. The proof for the rule (1′2) is similar.

(2. → 1. ) Let $\mathcal{K}$ be a class of RL(1, 1′)-structures. We need to show that every $\mathcal{K}$-structure $\mathcal{M} = (U,m)$ is an RL(1, 1′)-model, i.e., m(1) = U ×U, m(1′) is an equivalence relation on U, and the extensionality property is satisfied. Since every finite superset of {x1y} is a $\mathcal{K}$-set, the formula x1y is valid in every structure from $\mathcal{K}$. Hence, the first condition holds.

For reflexivity, observe that {x1′x} is a $\mathcal{K}$-set. Thus, in every $\mathcal{K}$-structure $\mathcal{M}$, $\mathcal{M}\models x1^{\prime}x$.

For symmetry, let $X\stackrel{\mathrm{df}}{=}\{y-1\prime x\}$. Since the rule (1′1) is $\mathcal{K}$-correct and the sets X ∪{x1′x, x1′y} and X ∪{y1′x, x1′y} are $\mathcal{K}$-sets, X ∪{x1′y} is also a $\mathcal{K}$-set. Therefore, for every $\mathcal{K}$-structure $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$, if (v(y), v(x)) ∈ m(1′), then (v(x), v(y)) ∈ m(1′).

For transitivity, let $X\stackrel{\mathrm{df}}{=}\{x-1^{\prime}z,z-1^{\prime}y\}$. Then, X ∪{ x1′z, x1′y} and X ∪{ z1′y, x1′y} are $\mathcal{K}$-sets. Thus, by $\mathcal{K}$-correctness of the rule (1′2), X ∪{x1′y} is also a $\mathcal{K}$-set. Therefore, for every $\mathcal{K}$-structure $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$, if (v(x), v(z)) ∈ m(1′) and (v(z), v(y)) ∈ m(1′), then (v(x), v(y)) ∈ m(1′).

Now, we prove the extensionality property, i.e., we show that for every atomic relational term R, $m(1^{\prime})\,;\,m(R) = m(R)\,;\,m(1^{\prime}) = m(R)$.

Since m(1′) is reflexive, m(R) ⊆ m(1′) ; m(R) and m(R) ⊆ m(R) ; m(1′).

To show m(1′) ; m(R) ⊆ m(R), consider $X\stackrel{\mathrm{df}}{=}\{x-1^{\prime}z,z-Ry\}$. By $\mathcal{K}$-correctness of the rule (1′2), X ∪{xRy} is a $\mathcal{K}$-set. Therefore, for every $\mathcal{K}$-structure $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$, if (v(x), v(z)) ∈ m(1′) and (v(z), v(y)) ∈ m(R), then (v(x), v(y)) ∈ m(R), which implies that if (v(x), v(y)) ∈ m(1′) ; m(R), then (v(x), v(y)) ∈ m(R).

For m(R) ; m(1′) ⊆ m(R), let $X\stackrel{\mathrm{df}}{=}\{x-Rz,y-1^{\prime}z\}$. Then, by $\mathcal{K}$-correctness of the rule (1′1), X ∪{xRy} is a $\mathcal{K}$-set. Therefore, for every $\mathcal{K}$-structure $\mathcal{M} = (U,m)$ and for every valuation v in $\mathcal{M}$, if (v(x), v(z)) ∈ m(R) and (v(y), v(z)) ∈ m(1′), then (v(x), v(y)) ∈ m(R). $\mathcal{K}$-correctness of the rule (1′1) implies symmetry of m(1′), so if (v(x), v(y)) ∈ m(R) ; m(1′), then (v(x), v(y)) ∈ m(R).

Hence, the extensionality property follows. □

RL(1, 1′)-correctness of the decomposition rules can be proved as in Proposition 2.5.1. Thus, by Theorem 2.7.1, we have:

Proposition 2.7.3.

• 1. The RL(1,1′)-rules are RL(1,1′)-correct;

• 2. The RL(1,1′)-axiomatic sets are RL(1,1′)-sets.

Following the general method of proving soundness described in Sect. 2.6, the above proposition implies:

Proposition 2.7.4.

Let φ be an RL(1,1′)-formula. If φ is RL(1,1′)-provable, then it is RL(1,1′)-valid.

Corollary 2.7.1.

Let φ be an RL(1,1′)-formula. If φ is RL(1,1′)-provable, then it is true in all standard RL(1,1′)-models.

The notions of an RL(1, 1′)-proof tree, a closed branch, a closed RL(1, 1′)-proof tree, and an RL(1, 1′)-proof of an RL(1, 1′)-formula are defined as in Sect. 2.4. Observe that any application of the rules of RL(1, 1′)-dual tableau, in particular an application of the specific rules (1′1) and (1′2), preserves the formulas built with atomic terms or their complements (see Fact 2.5.1). Therefore, whenever an atomic formula xRy and the formula x − Ry appear in a branch, then the branch is closed. Thus, the closed branch property holds.

A branch b of an RL(1, 1′)-proof tree is said to be RL(1, 1′)-complete whenever it is closed or it satisfies RL(1′)-completion conditions which consist of the completion conditions of RL-dual tableau adjusted to RL(1, 1′)-language and the following completion conditions determined by the specific rules of RL(1, 1′)-dual tableau:

For all object symbols x and y and for every atomic relational term R, Cpl(1′1) If xRy ∈ b, then for every object symbol z, either xRz ∈ b or y1′z ∈ b, obtained by an application of the rule (1′1);Cpl(1′2) If xRy ∈ b, then for every object symbol z, either x1′z ∈ b or zRy ∈ b, obtained by an application of the rule (1′1).

Let b be an open branch of an RL(1, 1′)-proof tree. We define a branch structure ${\mathcal{M}}^{b} = ({U}^{b},{m}^{b})$ as in RL-logic adapting it to the RL(1, 1′)-language. In particular, $m^{b}(R)\stackrel{\mathrm{df}}{=}\{(x,y)\in\,U^{b}\times U^{b}: xRy\in\,b\}$, for R ∈ { 1, 1′}.

Proposition 2.7.5 (Branch Model Property).

For every open branch b of an RL(1,1′)-proof tree, a branch structure ${\mathcal{M}}^{b}$ is an RL(1,1′)-model.

Proof.

We need to prove: (1) m ^b(1) = U ^b ×U ^b, (2) m ^b(1′) is an equivalence relation on U ^b, and (3) ${m}^{b}(1^{\prime})\,;\,{m}^{b}(R) = {m}^{b}(R)\,;\,{m}^{b}(1^{\prime}) = {m}^{b}(R)$, for every atomic relational term R.

Proof of (1). Clearly, for all object symbols x and y it must be x1y ∉ b, for otherwise b would be closed. Thus m ^b(1) = U ^b ×U ^b.

Proof of (2). For every x ∈ U ^b, x1′x ∉ b, for otherwise b would be closed. Therefore (x, x) ∈ m ^b(1′), hence m ^b(1′) is reflexive. Assume (x, y) ∈ m ^b(1′), that is x1′y ∉ b. Suppose (y, x) ∉ m ^b(1′). Then y1′x ∈ b. By the completion condition Cpl(1′1), either y1′y ∈ b or x1′y ∈ b, a contradiction. Therefore m ^b(1′) is symmetric. To prove transitivity, assume that (x, y) ∈ m ^b(1′) and (y, z) ∈ m ^b(1′), that is x1′y ∉ b and y1′z ∉ b. Suppose (x, z) ∉ m ^b(1′). Then x1′z ∈ b. By the completion condition Cpl(1′1), either x1′y ∈ b or z1′y ∈ b. In the first case we get a contradiction, so z1′y ∈ b. By the completion condition Cpl(1′1) applied to z1′y, either z1′z ∈ b or y1′z ∈ b. In both cases we get a contradiction.

Proof of (3). Since m ^b(1′) is reflexive, we have m ^b(R) ⊆ m ^b(1′) ; m ^b(R) and m ^b(R) ⊆ m ^b(R) ; m ^b(1′).

Now, assume (x, y) ∈ m ^b(1′) ; m ^b(R), that is there exists z ∈ U ^b such that x1′z ∉ b and zRy ∉ b. Suppose (x, y) ∉ m ^b(R). Then xRy ∈ b. By the completion condition Cpl(1′2), for every z ∈ U ^b, either x1′z ∈ b or zRy ∈ b, a contradiction.

Assume (x, y) ∈ m ^b(R) ; m ^b(1′), that is, by symmetry of m ^b(1′), there exists z ∈ U ^b such that xRz ∉ b and y1′z ∉ b. Suppose (x, y) ∉ m ^b(R). Then xRy ∈ b. By the completion condition Cpl(1′1), for every z ∈ U ^b, either xRz ∈ b or y1′z ∈ b, a contradiction. □

Any structure ${\mathcal{M}}^{b}$ defined as above is referred to as an RL(1, 1′)-branch model. Let ${v}^{b}:{ \mathbb{O}\mathbb{S}}_{\mathsf{RL}(1,1^{\prime})} \rightarrow {U}^{b}$ be a valuation in ${\mathcal{M}}^{b}$ such that v ^b(x) = x, for every object symbol x.

Proposition 2.7.6 (Satisfaction in Branch Model Property).

For every open branch b of an RL(1,1′)-proof tree and for every RL(1,1′)-formula φ, if ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ , then φ∉b.

The proof of the above proposition is similar to the proof of Proposition 2.5.5.

Given an RL(1, 1′)-branch model ${\mathcal{M}}^{b}$, since m ^b(1′) is an equivalence relation on U ^b, we may define the quotient model ${\mathcal{M}}_{q}^{b} = ({U}_{q}^{b},{m}_{q}^{b})$ as follows:

• ${U}_{q}^{b} =\{\| x\| : x \in {U}^{b}\}$, where $\|x\|$ is the equivalence class of m ^b(1′) generated by x;

• ${m}_{b}^{q}(c) =\| c\|$, for every object constant c;

• ${m}_{q}^{b}(R) =\{ (\|x\|,\|y\|)) \in {U}_{q}^{b} \times {U}_{q}^{b} : (x,y) \in {m}^{b}(R)\}$, for every atomic relational term R;

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

Since a branch model satisfies the extensionality property, the definition of m _q ^b(R) is correct, that is:

$$\mbox{ If $(x,y) \in {m}^{b}(R)$ and $(x,z),(y,t) \in {m}^{b}(1^{\prime})$, then $(z,t) \in {m}^{b}(R)$. }$$

Let v _q ^b be a valuation in ${\mathcal{M}}_{q}^{b}$ such that ${v}_{q}^{b}(x) =\| x\|$, for every object symbol x.

Proposition 2.7.7.

• 1. The model ${\mathcal{M}}_{q}^{b}$ is a standard RL(1,1′)-model;

• 2. For every RL(1,1′)-formula φ, ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ iff ${\mathcal{M}}_{q}^{b},{v}_{q}^{b}\models \varphi$ .

Proof.

• 1. We have to show that m _q ^b(1′) is the identity on U _q ^b. Indeed, we have:

  $$(\|x\|,\|y\|) \in {m}_{q}^{b}(1^{\prime})\mbox{ iff }(x,y) \in {m}^{b}(1^{\prime})\mbox{ iff }\|x\| =\| y\|.$$

• 2. The proof is by an easy induction on the complexity of relational terms. □

Proposition 2.7.8.

Let φ be an RL(1,1′)-formula. If φ is true in all standard RL(1,1′)-models, then φ is RL(1,1′)-provable.

Proof.

Assume φ is true in all standard RL(1, 1′)-models. Suppose there is no any closed RL(1, 1′)-proof tree for φ. Then there exists a complete RL(1, 1′)-proof tree for φ with an open branch, say b. Since φ ∈ b, by Proposition 2.7.6, φ is not satisfied by v ^b in the branch model ${\mathcal{M}}^{b}$. By Proposition 2.7.7(2.), φ is not satisfied by v _q ^b in the quotient model ${\mathcal{M}}_{q}^{b}$. Since ${\mathcal{M}}_{q}^{b}$ is a standard RL(1, 1′)-model, φ is not true in all standard RL(1, 1′)-models, a contradiction. □

From Fact 2.7.1, Propositions 2.7.4 and 2.7.8 we get:

Theorem 2.7.2 (Soundness and Completeness of RL(1, 1′)).

Let φ be an RL(1,1′)-formula. Then the following conditions are equivalent:

• 1. φ is RL(1,1′)-valid;

• 2. φ is true in all standard RL(1,1′)-models;

• 3. φ is RL(1,1′)-provable.

The class of RL(1, 1′)-models corresponds to the class FRA of full relation algebras, as it will be proved in Sect. 2.9.

8 Discussion of Various Rules for Relation 1′

As in the case of F-proof system, in RL(1, 1′)-dual tableau we can admit some other rules for relation 1′. There are at least three possibilities of choosing rules for 1′. In this section, rules (1′1) and (1′2) (see p. 43) will be called classical.

In many relational proof systems in the style of Rasiowa–Sikorski the following specific rules are used:

8.1 Standard

8.1.1 Standard

$$\begin{array}{llll} {(1^{\prime}1)}^{1} & \frac{xRy} {xRz,xRy\;\vert \;z1^{\prime}y,xRy} &\qquad {(1^{\prime}2)}^{1} & \frac{xRy} {x1^{\prime}z,xRy\;\vert \;zRy,xRy} \\ {(sym)}^{1} & \frac{x1^{\prime}y} {y1^{\prime}x}\\ \end{array}$$

where R is any relational variable or relational constant, x, y, z are any object symbols.

Then, the axiomatic sets are those of RL(1, 1′)-dual tableau, i.e., (Ax) from Sect. 2.5 and (Ax1) and (Ax2) from Sect. 2.7.

Completion conditions for rules (1′1)¹ and (1′2)² are analogous to those for the classical rules, and for the rule (sym)¹ we have:

Cpl(sym)¹ If x1′y ∈ b, then y1′x ∈ b.

Note that these standard specific rules differ from the classical ones in the rules (1′2)¹ and (sym)¹. The rule (1′2)¹ seems to be more natural than the rule (1′2). On the metalogical level the rule (1′2)¹ says: xRy is valid iff the conjunction of x1′z ∨ xRy and zRy ∨ xRy is valid. In the rule (1′2) positions of variables x and z in a formula x1′z are interchanged and this, in some sense, expresses symmetry of 1′. From a logical point of view it is immaterial which of these sets of specific rules is used. The standard rules are correct and give the complete proof system. The proof of completeness is similar to the proof for the system with the classical rules. The only difference is that symmetry of m ^b(1′) follows from the completion condition corresponding to the rule (sym)¹.

The following rules are essentially different from the classical ones.

8.1.2 Negative standard

$$\begin{array}{llll} {(1^{\prime}1)}^{2} & \frac{x-1^{\prime}y,y-Rz} {x-Rz,x-1^{\prime}y,y-Rz} &\qquad {(1^{\prime}2)}^{2} & \frac{x-1^{\prime}y,z-Rx} {z-Ry,x-1^{\prime}y,z-Rx} \\ {(sym)}^{2} & \frac{x-1^{\prime}y} {y-1^{\prime}x} &\qquad {(ref)}^{2} & \frac{} {x-1^{\prime}x} \\ {(1)}^{2} & \frac{} {x-1y} \\ \end{array}$$

where R is any relational variable or relational constant, and x, y, z are any object symbols.

The axiomatic sets are those of RL-dual tableau, i.e., (Ax) from Sect. 2.5.

The negative forms of specific rules are dual to the rules of a tableau system for the relational logic. Note that the rules (1′1)² and (1′2)² can be applied only to negated atomic formulas. Moreover, contrary to the classical rules, they do not branch a proof tree and do not involve introduction of a variable which makes them more suitable for implementation. Our conclusions from the discussion of different forms of the specific rule for the first-order logic in Sect. 1.8 are also relevant to this case.

Below we prove completeness of the proof system with the negative form of the rules for 1′. Moreover, we show that all these rules are needed to prove it.

The completion conditions corresponding to the negative rules are:

For all object symbols x, y, and z and for every atomic relational term R,Cpl(1′1)² If x − 1′y ∈ b and y − Rz ∈ b, then x − Rz ∈ b, obtained by an application of the rule (1′1)²;Cpl(1′2)² If x − 1′y ∈ b and z − Rx ∈ b, then z − Ry ∈ b, obtained by an application of the rule (1′2)²;Cpl(sym)² If x − 1′y ∈ b, then y − 1′x ∈ b, obtained by an application of the rule (sym)²;Cpl(ref)² For every object symbol x, x − 1′x ∈ b, obtained by an application of the rule (ref)²;Cpl(1)² For all object symbols x and y, x − 1y ∈ b, obtained by an application of the rule (1)².

Proposition 2.8.1 (Closed Branch Property).

For every branch of a proof tree in the relational dual tableau with negative standard rules, if xRy and x−Ry, for an atomic R, belong to the branch, then the branch can be closed.

Proof.

Although the rule (sym)² does not preserve the formula x − 1′y, if x − 1′y appears in a node of a branch, say b, then all the successors of this node in b include either x − 1′y, if the rule (sym)² has not been applied yet, or y − 1′x if the rule (sym)² has been applied. If x1′y is in a node, say n, of branch b, then either x − 1′y ∈ n and x1′y ∈ n or y − 1′x ∈ n and x1′y ∈ n. In the former case, the branch is closed. In the latter, we can apply rule (sym)² to y − 1′x in node n. Then we obtain a node which includes x − 1′y and x1′y and we close the branch. All the remaining rules preserve the formulas built with atomic terms or their complements. Thus, the closed branch property holds. □

Since the rules are applied to formulas built with complements of atomic terms, we need to change the definition of a branch structure. Let b be an open branch of a proof tree. We define a branch structure ${\mathcal{M}}^{b} = ({U}^{b},{m}^{b})$ as follows:

• ${U}^{b} ={ \mathbb{O}\mathbb{S}}_{\mathsf{RL}(1,1^{\prime})}$;

• ${m}^{b}(R) =\{ (x,y) \in {U}^{b} \times {U}^{b} : x-Ry \in b\}$, for every atomic relational term R;

• m ^b extends to all the compound terms as in RL-models.

Let ${v}^{b}:{ \mathbb{O}\mathbb{S}}_{\mathsf{RL}(1,1^{\prime})} \rightarrow {U}^{b}$ be a valuation in ${\mathcal{M}}^{b}$ such that v ^b(x) = x, for every object symbol x. First, we prove that m ^b(1′) is an equivalence relation.

Proposition 2.8.2.

m ^b (1′) is an equivalence relation.

Proof.

By the completion condition Cpl(ref)², for every x ∈ U ^b, x − 1′x ∈ b, which means that (x, x) ∈ m ^b(1′). Hence, m ^b(1′) is reflexive. Assume (x, y) ∈ m ^b(1′), that is x − 1′y ∈ b. By the completion condition Cpl(sym)², y − 1′x ∈ b, hence (y, x) ∈ m ^b(1′). Thus, m ^b(1′) is symmetric. Assume (x, y) ∈ m ^b(1′), (y, z) ∈ m ^b(1′), that is x − 1′y ∈ b and y − 1′z ∈ b. By the completion condition Cpl(1′1)², x − 1′z ∈ b, hence (x, z) ∈ m ^b(1′), which proves transitivity of m ^b(1′). □

Note that the rules (ref)² and (sym)² are needed to prove reflexivity and symmetry of m ^b(1′), respectively. The rule (1′1)² is needed to prove transitivity of m ^b(1′).

Proposition 2.8.3.

For every atomic relational term R:

• 1. m ^b (1′) ; m ^b (R) ⊆ m ^b (R);

• 2. m ^b (R) ; m ^b (1′) ⊆ m ^b (R).

Proof.

For 1., assume (x, y) ∈ m ^b(1′) ; m ^b(R). Then there exists z ∈ U ^b such that (x, z) ∈ m ^b(1′) and (z, y) ∈ m ^b(R), that is x − 1′z ∈ b and z − Ry ∈ b. By the completion condition Cpl(1′1)², x − Ry ∈ b, hence (x, y) ∈ m ^b(R).

The proof of 2. is similar. □

By the above proposition, the branch structure satisfies the extensionality property assumed in RL(1, 1′)-models. Moreover, due to the completion condition Cpl(1)², it satisfies the constraint m ^b(1) = U ^b ×U ^b. We conclude that the branch structure ${\mathcal{M}}^{b}$ is an RL(1, 1′)-model. Therefore, the quotient model can be defined in a similar way as in the proof of the completeness of RL(1, 1′) (see p. 52). The satisfaction in branch model property can be proved by induction on the complexity of relational terms, that is we have:

Proposition 2.8.4 (Satisfaction in Branch Model Property).

For every open branch b and for every RL(1,1′)-formula φ, if ${\mathcal{M}}^{b},{v}^{b}\models \varphi$, then φ∉b.

Moreover, the following can be proved in a similar way as in RL(1, 1′)-dual tableau:

Proposition 2.8.5.

• 1. ${\mathcal{M}}_{q}^{b}$ is a standard RL(1,1′)-model;

• 2. ${\mathcal{M}}^{b},{v}^{b}\models \varphi \mbox{ iff }{\mathcal{M}}_{q}^{b},{v}_{q}^{b}\models \varphi$.

Then completeness of RL(1, 1′)-dual tableau with negative specific rules follows from the above propositions.

We may refine the set of negative rules in analogy with the classical set of specific rules by deleting the symmetry rule and interchanging the positions of x and y in the rule (1′2)². Then we have less specific rules than in the negative standard set.

$$\begin{array}{llll} {(1^{\prime}1)}^{3} & \frac{x-1^{\prime}y,y-Rz} {x-Rz,x-1^{\prime}y,y-Rz} &\qquad {(1^{\prime}2)}^{3} & \frac{y-1^{\prime}x,z-Rx} {z-Ry,y-1^{\prime}x,z-Rx} \\ {(ref)}^{3} & \frac{} {x-1^{\prime}x} &\qquad {(1)}^{3} & \frac{} {x-1y}\\ \end{array}$$

where R is any relational variable or relational constant, and x, y, z are any object symbols.

Then, the axiomatic sets are those of RL-dual tableau, i.e., (Ax) from Sect. 2.5.

This set of specific rules together with the decomposition rules provides a complete proof system for RL(1, 1′). The proof of completeness is similar to the previous one except for the parts where rules (1′2)² and (sym)² are used.

9 Full Relation Algebras and Relational Logics

We recall that the class of full relation algebras, FRA, is the class of algebras of the form $(\mathcal{P}(U \times U),\cup, \cap, -,\varnothing, U \times U,;{,}^{-1},1^{\prime})$, where U is a non-empty set, 1′ is the identity on U, operations −, ∪, and ∩ are Boolean operations, ^{− 1} and ; are converse and composition of binary relations, respectively.

Let $\mathfrak{C}$ be a class of relation algebras. An equation R ₁ = R ₂, where R ₁ and R ₂ are relation algebra terms, is said to be $\mathfrak{C}$-valid whenever it is true in all algebras of $\mathfrak{C}$. The following theorem follows directly from the definition of validity in relational logics.

Theorem 2.9.1.

Let R be any relational term and let x and y be any two different object variables. Then xRy is true in all standard RL(1,1′)-models iff R = 1 is FRA-valid.

Proof.

( → ) Assume xRy is true in all standard RL(1, 1′)-models and suppose that R = 1 is not FRA-valid. Then there exists a FRA-algebra $\mathfrak{A}$ of binary relations on a set U such that ${R}^{\mathfrak{A}}\neq {1}^{\mathfrak{A}}$, where ${1}^{\mathfrak{A}}$ is the universal relation on U. Hence, for some u, u′ ∈ U, $(u,u^{\prime})\not\in {R}^{\mathfrak{A}}$. Consider an RL(1, 1′)-model ${\mathcal{M}}_{\mathfrak{A}} = (U,{m}_{\mathfrak{A}})$ such that:

• ${m}_{\mathfrak{A}}(P) = {P}^{\mathfrak{A}}$, for every relational variable P and for P ∈ { 1, 1′};

• ${m}_{\mathfrak{A}}$ extends to all the compound relational terms as in RL(1, 1′)-models (see Sect. 2.3).

It follows that for every relational term Q, ${m}_{\mathfrak{A}}(Q) = {Q}^{\mathfrak{A}}$. Consider a valuation v in model ${\mathcal{M}}_{\mathfrak{A}}$ such that v(x) = u and v(y) = u′. Such a valuation v exists, since variables x and y are different. Then $(v(x),v(y))\not\in {m}_{\mathfrak{A}}(R)$, a contradiction.

( ← ) Assume R = 1 is FRA-valid and suppose xRy is not true in a standard RL(1, 1′)-model $\mathcal{M} = (U,m)$. Then there exists a valuation v in $\mathcal{M}$ such that (v(x), v(y)) ∉ m(R). Consider a FRA-algebra ${\mathfrak{A}}_{\mathcal{M}} = (\mathcal{P}(U \times U),\cup, \cap, -,\varnothing, U \times U,;{,}^{-1},m(1^{\prime}))$ such that ${P}^{{\mathfrak{A}}_{\mathcal{M}}} = m(P)$, for every relational variable P. It follows that for every relational term Q, ${Q}^{{\mathfrak{A}}_{\mathcal{M}}} = m(Q)$. Since R = 1 is FRA-valid, it must be true in ${\mathfrak{A}}_{\mathcal{M}}$. Hence, ${R}^{{\mathfrak{A}}_{\mathcal{M}}} = {1}^{{\mathfrak{A}}_{\mathcal{M}}} = U \times U$. This yields m(R) = U ×U, a contradiction. □

Due to the above theorem and Theorem 2.7.2, we obtain:

Theorem 2.9.2.

Let xRy be an RL(1,1′)-formula. Then xRy is RL(1,1′)-provable iff R = 1 is FRA-valid.

An example of RL(1, 1′)-provable formula which represents a FRA-valid equation which is not RA-valid is presented in Sect. 2.10.

As a consequence of Proposition 2.2.1(1.), we have:

Proposition 2.9.1.

Let R and S be RL(1,1′)-terms. Then R ⊆ S holds in every FRA-algebra iff x(−R ∪ S)y is RL(1,1′)-valid.

Since the class RRA is a variety generated by FRA, it is know that:

Theorem 2.9.3.

The set of equations valid in RRA coincides with the set of equations valid in FRA.

Hence, RL(1, 1′)-logic is a tool for verification of validity of equations in the class RRA of representable relation algebras.

10 An Example of a Relational Dual Tableau Proof

As an example of an RL(1, 1′)-provable equation let us consider the equation $\tau=1,$ for $\tau\stackrel{\mathrm{df}}{=}(1;\rho;1)$ and $\rho\stackrel{\mathrm{df}}{=}(A\,\cup\,B\cup\,D\,\cup\,E)$, where A, B, C, D, and E are defined as follows, for relational variables R and N:

• $A = -(1\,;\,R\,;\,1)$,

• $B = [R \cap -[(N\,;\,N) \cap (R\,;\,N)]]$,

• C = (N ; N ∪R ; R) ∩ N,

• $D = [(R \cup {R}^{-1} \cup 1^{\prime}) \cap N]$,

• $E = -(R \cup {R}^{-1} \cup 1^{\prime} \cup N)$.

This equation is RRA-valid, while it is not RA-valid.

Proposition 2.10.1.

The equation τ is true in all representable relation algebras.

Proof.

Suppose τ is not true in some $\mathfrak{A} \in$ FRA, that is τ≠1. Then, by Proposition 2.2.1(3.), ρ = ∅ in $\mathfrak{A}$. It means that the following are true in $\mathfrak{A}$:

• (1) $-(1\,;\,R\,;\,1) = \varnothing$,

• (2) $(R \cap -[(N\,;\,N) \cap (R\,;\,N)]) = \varnothing$,

• (3) [(R ; R ∪N ; N) ∩ N] = ∅,

• (4) $[(R \cup {R}^{-1} \cup 1^{\prime}) \cap N] = \varnothing$,

• (5) $-(R \cup {R}^{-1} \cup 1^{\prime} \cup N) = \varnothing$.

The first condition implies that R≠∅, since the following holds:

$$-(1\,;\,R\,;\,1) = \varnothing \mbox{ iff }(1\,;\,R\,;\,1) = 1\mbox{ iff }R\neq \varnothing.$$

The condition (2) is equivalent to R ⊆ (N ; N) ∩ (R ; N), which means that R ⊆ N ; N and R ⊆ R ; N. From condition (3) it follows that (R ; R) ∩ N = ∅ and (N ; N) ∩ N = ∅. Condition (4) implies that relations R ∩ N, R ^{− 1} ∩ N, 1′ ∩ N are empty. The condition (5) means that R ∪R ^{− 1} ∪1′ ∪N is the universal relation 1.

Summarizing, if τ is not true in $\mathfrak{A}$, then the following must hold:

• (a) R≠∅,

• (b1) R ⊆ N ; N,

• (b2) R ⊆ R ; N,

• (c1) (R ; R) ∩ N = ∅,

• (c2) (N ; N) ∩ N = ∅,

• (d1) R ∩ N = ∅,

• (d2) ${R}^{-1} \cap N = \varnothing$,

• (d3) 1′ ∩ N = ∅,

• (e) $(R \cup {R}^{-1} \cup 1^{\prime} \cup N) = 1$.

By (a), (b2), and (d1) there are different x, y in the universe of $\mathfrak{A}$ such that (x, y) ∈ R. By (b1) an element z must exist such that (x, z), (z, y) ∈ N. Since R ∩ N = ∅, we have z≠x, y. Figure 2.3 presents this part of $\mathfrak{A}$. Thick lines and thin lines correspond to relations R and N, respectively.

Fig. 2.3

Algbra $\mathfrak{A}$, step 1

By (b2) there is v such that (x, v) ∈ R and (v, y) ∈ N. Since by (d3) 1′ ∩ N = ∅, v≠y. If v = x or v = z, then R ∩ N≠∅. Hence v≠x, y, z, (x, v) ∈ R, and (v, y) ∈ N as presented in Fig. 2.4a. By condition (e), (z, v) ∈ R or (v, z) ∈ R or (z, v) ∈ N. Suppose (v, z) ∈ R. Then (x, v), (v, z) ∈ R and (x, z) ∈ N which implies that (R ; R) ∩ N is not empty, a contradiction with condition (c1). Suppose (z, v) ∈ N. Then (z, v), (v, y), (z, y) ∈ N, which contradicts condition (c2). So (z, v) ∈ R, and hence the algebra $\mathfrak{A}$ must look as shown in Fig. 2.4b. Since (x, v) ∈ R and by (b1) R ⊆ (N ; N), there must exist an element s such that (x, s), (s, v) ∈ N. By condition (d1), s≠y, v, for otherwise R ∩ N≠∅. By condition (d3), s≠x, for otherwise 1′ ∩ N≠∅. Suppose s = z. Then (z, y), (v, y), (z, v) ∈ N, which means that (N ; N) ∩ N≠∅, a contradiction with condition (c2). Therefore, s is distinct from x, y, z, and v (see Fig. 2.5a). Hence, (x, y), (x, v) ∈ R and (z, y), (x, z), (v, y), (x, s), (s, v) ∈ N.

Fig. 2.4

Algebra $\mathfrak{A}$, step 2

Again by condition (e), (y, s) ∈ R or (s, y) ∈ R or (s, y) ∈ N. Assumptions (s, y) ∈ N and (y, s) ∈ R lead to a contradiction with conditions (c2) and (c1), respectively. Therefore (s, y) ∈ R as shown in Fig. 2.5b. By condition (e), s and z must be in one of the relations R, R ^{− 1} or N. If (s, z) ∈ R, then we have (s, z), (z, v) ∈ R and (s, v) ∈ N, a contradiction with condition (c1). Similarly, we can prove that (z, s) ∉ R. Therefore (s, z) ∈ N, but then (N ; N) ∩ N is non-empty, a contradiction. □

Fig. 2.5

Algebra $\mathfrak{A}$, step 3

Proposition 2.10.2.

There exists a relation algebra $\mathfrak{A}$ in which the equation τ is not true.

Proof.

Let $\mathfrak{A} = (W,+,\cdot, -,0,1,;,\breve{\;},1^{\prime})$ be a relation algebra such that $(W,+,\cdot, -,0,1)$ is a Boolean algebra generated by the four atoms a, b, c, and d and the operations ; and $\breve{\;}$ are defined as follows:

	$\smile$
a	a
b	c
c	b
d	d

$\breve{\;}$	a	b	c	d
a	a	b	c	d
b	b	b	1	b + d
c	c	1	c	c + d
d	d	b + d	c + d	$a + b + c$

Let v be a valuation such that $v(1^{\prime}) = a,v(R) = b,v(N) = d$. We show that the equation τ is not satisfied in $\mathfrak{A}$ by v.

From Proposition 2.10.1 it is known that unsatisfiability of τ in a relation algebra implies that all the equations (1)–(5) are true in such an algebra. Therefore it suffices to show that these equations are true in $\mathfrak{A}$.

Since $(W,+,\cdot, -,0,1)$ is a Boolean algebra generated by the atoms a, b, c, d and $1 = a + b + c + d$, the following hold:

• (1) $-(1\,;\,b\,;\,1) = -[(a + b + c + d)\,;\,b\,;\,(a + b + c + d)] = -(1\,;\,1) = 0$, since ; is an associative operation that distributes over +,

• (2) $(b \cdot -[(d\,;\,d) \cdot (b\,;\,d)]) = b \cdot -[(a + b + c) \cdot (b + d)] = b \cdot -b = 0$,

• (3) $[(b\,;\,b + d\,;\,d) \cdot d] = [b + (a + b + c)] \cdot d = 0$,

• (4) $[(b + {b}^{\smile } + 1^{\prime}) \cdot d] = (a + b + c) \cdot d = 0$,

• (5) $-(b \cdot {b}^{\smile } + 1^{\prime} + d) = -(a + b + c + d) = -1 = 0$.

Therefore we may conclude that τ is not true in $\mathfrak{A}$. □

Below we present a construction of an RL(1, 1′)-proof of the formula uτw which provides a proof of RRA-validity of the equation τ = 1.

It is easy to show that in a proof tree of uτw, if a formula uτw occurs in a node of this tree, then it is possible to build a subtree of this proof tree with this formula at the root such that it ends with exactly one non-axiomatic node containing at least one of the following formulas: zAv, zBv, zCv, zDv, and zEv, for some variables z and v. Therefore, in such cases instead of building long subtrees we will use the following derived rules:

For all object symbols u, w, z, and v,

$$\begin{array}{llllll} (Azv)\quad & \frac{u\tau w} {zAv,u\tau w} &\qquad (Bzv)\quad & \frac{u\tau w} {zBv,u\tau w} &\qquad (Czv)\quad & \frac{u\tau w} {zCv,u\tau w} \\ (Dzv)\quad & \frac{u\tau w} {zDv,u\tau w} &\qquad (Ezv)\quad & \frac{u\tau w} {zEv,u\tau w}\\ \end{array}$$

By way of example, in Fig. 2.6 we present a derivation of rule (Azv).

Fig. 2.6

A derivation of rule (Azv)

Similarly, we can admit the following derived rules:

$$\begin{array}{llll} ({1^{\prime}}^{{_\ast}}) &\,\frac{x1^{\prime}y} {y1^{\prime}x} &\qquad (Rxyz) &\, \frac{x-Ry,u\tau w} {x-Nz,z-Ny,x-(R\,;\,N)y,x-Ry,u\tau w} \\ & & &\qquad \mbox{ z is a new variable} \\ {(RN1^{\prime}xyz)}_{1} & \, \frac{z-Rx,z-Ny,u\tau w} {x1^{\prime}y,z-Rx,z-Ny,u\tau w} & \frac{z-Rx,z-Ny,u\tau w} {y1^{\prime}x,z-Rx,z-Ny,u\tau w} \\ {(RN1^{\prime}xyz)}_{2} & \, \frac{x-Rz,y-Nz,u\tau w} {x1^{\prime}y,x-Rz,y-Nz,u\tau w} & \frac{x-Rz,y-Nz,u\tau w} {y1^{\prime}x,x-Rz,y-Nz,u\tau w} \\ (RRNxyz) &\,\frac{x-Ry,y-Rz,x-Nz,u\tau w} {\mathit{closed}} \\ (NNNxyz)&\,\frac{x-Ny,y-Nz,x-Nz,u\tau w} {\mathit{closed}}\\ \end{array}$$

By way of example, in Figs. 2.10 and 2.11 we show how to obtain the derived rules (Rxyz) and (RN1′xyz)₁, respectively. The remaining derived rules are obtained in a similar way. It is easy to check that the derived rule (Cxy) is needed to get (RRNxyz) and (NNNxyz), while (Dxy) is needed in the proofs of (RN1′xyz)₁ and (RN1′xyz)₂. Figure 2.7 presents an RL(1, 1′)-proof of uτw.

Fig. 2.7

An RL(1, 1′)-proof of uτw

Fig. 2.8

The subtree Π

Fig. 2.9

The subtree Γ

Fig. 2.10

A derivation of the rule (Rxyz)

Fig. 2.11

A derivation of the rule (RN1′xyz)₁

11 Relational Entailment

The logic RL(1, 1′) can be used to verify entailment of formulas from a finite set of formulas. The method is based on the following fact. Let n ≥ 1 and let R ₁, …, R _n , R be binary relations on a set U and let 1 = U ×U. It is known ([Tar41], see also Proposition 2.2.1(7.)), that ${R}_{1}\,=\,1,\ldots, {R}_{n}\,=\,1$ imply R = 1 iff $(1\,;\,-({R}_{1} \cap \ldots \cap {R}_{n})\,;\,1) \cup R = 1$. It follows that for every RL(1, 1′)-model $\mathcal{M}$, $\mathcal{M}\models x{R}_{1}y$, …, $\mathcal{M}\models x{R}_{n}y$ imply $\mathcal{M}\models xRy$ iff $\mathcal{M}\models x(1\,;\,-({R}_{1} \cap \ldots \cap {R}_{n})\,;\,1) \cup R)y$ which means that entailment in RL(1, 1′) can be expressed in its language.

Example.

We prove that $x-(R\,;\,-P)y$ and $x-(R\,;\,-(-P \cup Q))y$ entail $x-(R\,;\,-Q)y$, by showing that the formula:

$$x[(1\,;\,-(-(R\,;\,-P) \cap -(R\,;\,-(-P \cup Q)))\,;\,1) \cup -(R\,;\,-Q)]y$$

is RL(1, 1′)-provable. Figure 2.12 presents an RL(1, 1′)-proof of this formula.

Fig. 2.12

An RL(1, 1′)-proof showing that $x-(R\,;\,-P)y$ and $x-(R\,;\,-(-P \cup Q))y$ entail $x-(R\,;\,-Q)y$

Now, we show that for every relation R, R ; 1 = 1 or $1\,;\,-R = 1$. Applying Proposition 2.2.1(6.), we need to show that the formula

$$x1\,;\,(-(1\,;\,(-(R\,;\,1)\,;\,1))\,;\,1) \cup (1\,;\,-R)y$$

is RL(1, 1′)-provable. Figure 2.13 presents an RL(1, 1′)-proof of this formula.

12 Decision Procedures for Some Relational Logics

In this section we present some decidable subclasses of formulas of the basic relational logic RL chosen from those presented in [BO97, Dob96a, Dob96b]. The classes are described in the syntactic terms. Usually, a distinguishing feature of a class is formulated in terms of a condition on the occurrences of the composition symbol in the formulas of the class. For the sake of simplicity, we will often say composition when referring to its occurrences.

Fig. 2.13

An RL(1, 1′)-proof showing that R ; 1 = 1 or $1\,;\,-R = 1$

An occurrence of the symbol of composition (; ) is said to be positive (resp. negative) in a formula iff it is in the scope of an even (resp. odd) number of the complement symbols in the formula. Similarly, an occurrence of the symbol of composition is negative-positive (resp. positive-negative) iff it is positive (resp. negative) and it falls into the scope of a negative (resp. positive) composition. An occurrence c of the composition is between the compositions c ₁ and c ₂ iff c falls into the scope of c ₁ and c ₂ falls into the scope of c.

A formula φ of the logic RL is said to be:

• Positive (resp. negative) iff all the compositions in φ are positive (resp. negative);

• Negative-positive if there is no any positive-negative composition in φ;

• 1-positive iff there is exactly one positive composition in φ (and possibly some negative ones);

• 2-positive iff there are exactly two positive compositions in φ and there is no any negative composition in φ between the positive compositions.

The classes of formulas considered above will be referred to as:

• RL _POS – the class of all positive formulas;

• RL _NEG – the class of all negative formulas;

• RL _NP – the class of all negative-positive formulas;

• RL _POS(1) – the class of all 1-positive formulas;

• RL _POS(2) – the class of all 2-positive formulas.

Example.

Let P, Q be relational variables. Consider the following RL-terms:

• ${T}_{1} = -(-(P\,;\,(Q \cap P)) \cup -(Q\,;\,P))$,

• ${T}_{2} = (-(P\,;\,Q) \cap -(Q \cup (Q\,;\,P)))$,

• ${T}_{3} = -((-(P\,;\,Q)\,;\,-(Q\,;\,P))\,;\,(-(Q\,;\,-P)\,;\,-(P\,;\,-Q)))$,

• ${T}_{4} = -((P \cup Q)\,;\,-(-(Q\,;\,P)\,;\,Q))$,

• ${T}_{5} = -(-P\,;\,-((Q\,;\,-(Q\,;\,P))\,;\,Q))$.

The formula xT ₁ y is positive, since all of its compositions are in the scope of an even number of complements, and similarly, xT ₂ y is negative, since all of its compositions are negative. The formula xT ₃ y is negative–positive, and its positive compositions occur in the following terms that do not contain any negative occurrence of composition: (P ; Q), (Q ; P), (Q ; − P), and (P ; − Q). The formula xT ₄ y is 1-positive, since the only positive composition of this formula is the principal composition of ( − (Q ; P) ; Q) and all the other compositions are negative. The formula xT ₅ y is 2-positive. In order to see this, observe that xT ₅ y contains only two positive compositions, namely those in the term ((Q ; − (Q ; P)) ; Q), and there is no any negative composition between these two positive compositions.

Decidability of these classes of formulas is proved by showing that the first-order translations of their members form decidable subclasses of the classical first-order predicate logic F. A natural translation τ of relational formulas into first-order formulas is defined as follows. Let a one-to-one assignment τ′ be given of object variables and relational variables of RL to individual variables and predicate symbols from the language of F, respectively. Then we define:

• τ(xPy) = τ′(P)(τ′(x), τ′(y)), for every atomic relational variable P;

For all relational terms R and S:

• $\tau (x-Ry) = \neg \tau (xRy)$;

• τ(x(R ∪S)y) = τ(xRy) ∨ τ(xSy);

• τ(x(R ∩ S)y) = τ(xRy) ∧ τ(xSy);

• $\tau (x{R}^{-1}y) = \tau (yRx)$;

• τ(x(R ; S)y) = ∃τ′(z)(τ(xRz) ∧ τ(zSy)).

The translations of relational formulas from the classes defined above belong to the following decidable classes of first-order formulas. Let $(\forall )$ and ( ∃) denote finite strings of universal and existential quantifiers, respectively. The classes are denoted by indicating a form of the string of quantifiers in the prenex normal form of the formulas in the class:

• ( ∃) – the class of existential formulas;

• $(\forall )$ – the class of universal formulas;

• $(\forall )(\exists )$ – the class of formulas with universal quantifiers followed by existential quantifiers;

• $(\forall )\exists (\forall )$ – the class of formulas with exactly one existential quantifier between the universal quantifiers;

• $(\forall ){\exists }_{1}{\exists }_{2}(\forall )$ – the class of formulas with exactly two existential quantifiers between the universal quantifiers.

The following is well known (see [Ack54]):

Proposition 2.12.1.

The classes (∃), $(\forall),$ $(\forall )(\exists ),$ $(\forall )\exists (\forall )$ , and $(\forall ){\exists }_{1}{\exists }_{2}(\forall )$ have a decidable validity problem.

The translations of relational formulas from the classes listed above fall into the following classes of first-order logic:

Proposition 2.12.2.

For every relational formula φ, the prenex form of τ(φ), pf(τ(φ)), satisfies:

• 1. If φ is positive, then $pf(\tau (\varphi )) \in {\forall }_{1}{\forall }_{2}(\exists )$

• 2. If φ is negative, then $pf(\tau (\varphi )) \in (\forall )$;

• 3. If φ is negative-positive, then $pf(\tau (\varphi )) \in (\forall )(\exists )$

• 4. If φ is 1-positive, then $pf(\tau (\varphi )) \in (\forall )\exists (\forall )$;

• 5. If φ is 2-positive, then $pf(\tau (\varphi )) \in (\forall ){\exists }_{1}{\exists }_{2}(\forall ).$

By Propositions 2.12.1 and 2.12.2, we get:

Theorem 2.12.1 (Decidable Classes of Relational Formulas).

The classes RL _POS , RL _NEG , RL _NP , RL _POS(1) , and RL _POS(2) of relational formulas have a decidable validity problem.

Below we present sound and complete dual tableaux that are decision procedures for the classes RL _POS , RL _NEG , RL _NP . Note that RL-dual tableau is not a decision procedure for these classes, since if the rule (; ) is applicable, then it can be applied infinitely many times. Observe that the rule (; ) is the only rule of RL-dual tableau with that property. Therefore, in order to obtain decision procedures for the classes defined in terms of positive formulas we need to modify the rule for the composition or to restrict its applicability. According to the definition of the classes ${\mathsf{RL}}_{\mathcal{K}}$, for $\mathcal{K}\in \{\mathsf{POS},\mathsf{NEG},\mathsf{NP}\}$ given above, we observe that:

• If φ is positive, then none of its proof trees involves any application of the rule ( − ; ),

• If φ is negative, then none of its proof trees involves any application of the rule (; ),

• If φ is negative-positive, then in each of its proof trees the applications of the rule ( − ; ) precede the applications of the rule (; ).

These observations suggest that dual tableaux for these classes should be constructed from RL-dual tableau as follows:

• RL _POS -dual tableau consists of the axiomatic sets and decomposition rules of RL-dual tableau except the rule ( − ; ),

• RL _NEG -dual tableau consists of the axiomatic sets and decomposition rules of RL-dual tableau except the rule (; ),

• RL _NP -dual tableau consists of the axiomatic sets and decomposition rules of RL-dual tableau.

In order to obtain decision procedures for the classes listed above we modify the applicability of the rule (; ) as follows. The rule (; ) of the form:

$$\frac{x(R\,;\,S)y} {xRz,x(R\,;\,S)y\,\vert \,zSy,x(R\,;\,S)y}$$

may be applied to a finite set X of relational formulas if and only if the following conditions are satisfied:

• x(R ; S)y ∈ X;

• z occurs in X;

• The rule (; ) introduces a new formula, i.e., xRz ∉ X or zSy ∉ X;

• No other rule is applicable to X.

The second condition implies that there are finitely many possibilities of choosing a variable z. Hence, together with the third condition, they prevent needless expansion of sets of formulas ad infinitum by repeated applications of the rule. The last condition guarantees that the rule (; ) can be applied only after the applications of the rule ( − ; ), since all the classes in question do not contain positive–negative formulas.

As in RL-logic, the rules of all dual tableaux considered above guarantee that whenever xRy and x − Ry, for an atomic R, belong to a branch of a proof tree, then the branch is closed. Thus the closed branch property holds. Since all the rules are RL-correct, we have:

Proposition 2.12.3.

For every $\mathcal{K}\in \{\mathsf{POS},\mathsf{NEG},\mathsf{NP}\}$ , all ${\mathsf{RL}}_{\mathcal{K}}$ -rules are ${\mathsf{RL}}_{\mathcal{K}}$ -correct.

Moreover, since formulas of the class RL _NEG do not contain positive compositions, the completeness of the reduct of RL-dual tableau for RL _NEG can be proved as for the appropriate part of RL-dual tableau.

Theorem 2.12.2 (Soundness and Completeness of RL _NEG ).

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

• 1. φ is RL _NEG -valid;

• 2. φ is RL _NEG -provable.

By the above theorem and due to the forms of RL _NEG -rules, RL _NEG -dual tableau is a decision procedure for the class RL _NEG .

Now, we aim at proving completeness of RL _POS -dual tableau. Let b be a branch of an RL _POS -proof tree. Let $\mathbb{O}\mathbb{V}(b)$ be the set of all variables that occur in formulas appearing in the nodes of b. The branch b is said to be complete if it is closed or it satisfies all the completion conditions of RL-dual tableau except Cpl(; ) and, in addition, the following completion condition:

Cpl’(; ) If x(R ; S)y ∈ b, then for every $z \in \mathbb{O}\mathbb{V}(b)$, either xRz ∈ b or zSy ∈ b.

We define the branch structure ${\mathcal{M}}^{b} = ({U}^{b},{m}^{b})$ as follows:

• ${U}^{b} = \mathbb{O}\mathbb{V}(b)$;

• m ^b(P) = {(x, y) ∈ U ^b ×U ^b : xPy ∉ b}, for every atomic term P;

• m ^b extends to all the compound relational terms as in RL-models.

Clearly, ${\mathcal{M}}^{b}$ is an RL-model. Hence, the branch model property holds. Let v ^b be a valuation in ${\mathcal{M}}^{b}$ such that v ^b(x) = x for every object variable x.

Proposition 2.12.4 (Satisfaction in Branch Model Property).

Let b be an open branch of an RL _POS -proof tree. Then, for every RL _POS -formula φ, if φ ∈ b, then ${\mathcal{M}}^{b},{v}^{b}\nvDash \varphi$ .

Proof.

The proof is by induction on the complexity of terms. If P is a relational variable and xPy ∈ b, then the proposition holds by the definition of ${\mathcal{M}}^{b}$. If x − Py ∈ b, then xPy ∉ b, since otherwise, due to the closed branch property, b would be closed. Thus, (x, y) ∈ m ^b(P). Suppose ${\mathcal{M}}^{b},{v}^{b}\models x-Py$. Then (x, y) ∉ m ^b(P), a contradiction.

Now, assume x(R ; S)y ∈ b. Then, by the completion condition Cpl’(; ), for every z ∈ U ^b, either xRz ∈ b or zSy ∈ b. By the induction hypothesis, for every z ∈ U ^b, either (x, z) ∉ m ^b(R) or (z, y) ∉ m ^b(S). Suppose ${\mathcal{M}}^{b},{v}^{b}\models x(R\,;\,S)y$. Then there exists z ∈ U ^b such that (x, z) ∈ m ^b(R) and (z, y) ∈ m ^b(S), a contradiction.

The proofs for terms of the form R ∪S, R ∩ S, and their complements are similar as in the completeness proof of RL-dual tableau. □

We conclude:

Theorem 2.12.3 (Soundness and Completeness of RL _POS ).

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

• 1. φ is RL _POS -valid;

• 2. φ is RL _POS -provable.

Note that none of the RL _POS -rules introduces a new variable. Therefore, the rule (; ) can be applied to a given set of formulas only finitely many times. Hence, RL _POS -dual tableau is a decision procedure for the class RL _POS .

Completeness of RL _NP -dual tableau can be proved in a similar way as completeness of RL _POS -dual tableau. Namely, RL _NP -completion conditions are RL _POS -completion condition and the following:

Cpl’( − ; ) If x − (R ; S)y ∈ b, then for some $z \in \mathbb{O}\mathbb{V}(b)$, both xRz ∈ b and zSy ∈ b.

We have:

Theorem 2.12.4 (Soundness and Completeness of RL _NP ).

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

• 1. φ is RL _NP -valid;

• 2. φ is RL _NP -provable.

Recall that RL _NP -formulas do not contain positive-negative compositions, which means that each positive composition is in the scope of a negative composition. Although, the rule ( − ; ) introduces a new variable, it is never applied after the application of the rule (; ). Consequently, there are finitely many possibilities of choosing a variable in the application of the rule (; ), and hence the rule (; ) can be applied to a given set of formulas only finitely many times. Therefore, we conclude that RL _NP -dual tableau is a decision procedure for the class RL _NP .