Dual Tableaux for Temporal Logics

Abstract

The first attempts to create a tense logic are the investigations of A. N. Prior published in [Pri57, Pri67]. Temporal logics are modal logics whose modal operations are determined by two relations on a set of time points expressing earlier-later or past-future relationships between instants of time. The relations are ordering relations possibly satisfying various axioms such as strict ordering, linear ordering, branching time, ordering with or without endpoints, discrete, etc. If P is a relation such that holding of tPt′ is interpreted as t precedes t′, then the modal operator ⟨P⟩ means ‘it will at some time be the case that’ and [P] is interpreted as ‘it will always be the case that’. Similarly, if F is a relation such that tFt′ means t follows t′, then ⟨F⟩ says ‘it has at some time been the case that’ and [F] is intuitively interpreted as ‘it has always been the case that’.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The first attempts to create a tense logic are the investigations of A. N. Prior published in [Pri57, Pri67]. Temporal logics are modal logics whose modal operations are determined by two relations on a set of time points expressing earlier-later or past-future relationships between instants of time. The relations are ordering relations possibly satisfying various axioms such as strict ordering, linear ordering, branching time, ordering with or without endpoints, discrete, etc. If P is a relation such that holding of tPt′ is interpreted as t precedes t′, then the modal operator ⟨P⟩ means ‘it will at some time be the case that’ and [P] is interpreted as ‘it will always be the case that’. Similarly, if F is a relation such that tFt′ means t follows t′, then ⟨F⟩ says ‘it has at some time been the case that’ and [F] is intuitively interpreted as ‘it has always been the case that’. Often some other temporal operations are included in languages of temporal logics. The binary operations Since and Until introduced in [Kam68] and the unary operation Next, introduced in [vW65], are among the most popular. If φ and ψ are formulas, then the formula ‘φ Since ψ’ says that ψ has been true since a time point when φ was true. The formula ‘φ Until ψ’ means that there is a future time point at which ψ is true, with φ true at all time points between now and then. The formula ‘Next φ’ is meaningful whenever the ordering of time points is discrete. Then it says that φ is true at the immediate successor of a present time moment.

The problem of representing time-varying information and reasoning with such information arises in a wide range of disciplines including logic, computer science, psychology, linguistics, and philosophy. Applications of temporal logic in computer science have been initiated by J. Bubenko in [Bub77] for applications in the theory of databases and by A. Pnueli in [Pnu77] for applications in the theory of programs. Since then temporal logics have become an important issue in artificial intelligence, in the specification and verification of programs, and in reasoning about actions and events. In Chap. 19 we discuss, among others, a temporal logic for the specification and verification of concurrent programs. Surveys of temporal logics and their applications can be found in [Bur79, vB83, vB95, Gol87, AHK02, HR06]. There are many results on decidability of temporal logics. It was proved that the temporal theories of arbitrary linear orders, of every elementary class of linear orders, of well orders, and of complete orders are decidable. A comprehensive survey of decidability of temporal logics can be found in [BG85].

In this chapter we present relational dual tableaux for a number of point-based temporal structures.

2 Basic Temporal Logic

Temporal logics belong to the family of modal logics. In their models the elements of the universes are interpreted as moments of time and the accessibility relation reflects earlier-later relationship. To get access to both past and future moments, in temporal frames we usually include the accessibility relation and its converse, denoted by P and F, respectively. Modal operations determined by these relational constants refer to past and future moments of time, respectively. The logics with these operations as the only modal operations are referred to as the standard temporal logics. We obtain various classes of standard temporal logics by assuming specific properties of the accessibility relations.

The common language of standard temporal logics is a modal language as defined in Sect. 7.3 with relational constants F and P. In this chapter we consider the basic temporal logic TL whose models are structures of the form $\mathcal{M} = (U,F,P,m)$ as defined in Sect. 7.3 (see p. 157) such that F and P are transitive relations on U satisfying F = P ^{− 1}. Relations F and P may satisfy some additional conditions, for example linearity or density, as presented in the next section.

The language of temporal logics with operations determined by relations F and P is more expressive than the ordinary modal language with operations determined by one of these relations, for example, continuity of a strict linear ordering is expressible only in the presence of both past and future operations.

In order to obtain a relational representation of the logic TL, we follow the method presented in Sect. 7.4. We define logic RL _TL whose language is appropriate for expressing formulas of TL as relations. It is an RL(1, 1′)-language such that ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{TL}}}\,=\,\{1,1\prime,F,P\}$ and ${\mathbb{O}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{TL}}}\,=\,\varnothing$. An RL _TL -model is a structure $\mathcal{M}\,=\,(U,F,P,m)$ such that (U, m) is an RL(1, 1′)-model, F and P are binary relations on U that provide the interpretation of relational constants F and P, respectively, and satisfy all the properties of relations F and P that are assumed in TL-models. The translation of TL-formulas into relational terms is defined as in Sect. 7.4 (see p. 158). Due to Theorem 7.4.1, we have:

Theorem 16.2.1.

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

• 1. φ is TL-valid;

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

RL _TL -dual tableau is an extension of RL(1, 1′)-dual tableau with the specific rules that reflect properties of the relations F and P. The rule reflecting transitivity is presented in Sect. 6.6 (see also Sect. 7.4). We recall that this rule has the following form:

For all object variables x and y and for every R ∈ {F, P},

$$(\mbox{ tran }R)\quad \frac{xRy} {xRz,xRy\,\vert \,zRy,xRy}\quad z\ \mbox{ is any object variable}$$

The rules that reflect the conditions P ^{− 1} ⊆ F and F ⊆ P ^{− 1} have the following forms, respectively:

For all object variables x and y,

$$(F)\quad \frac{xFy} {yPx,xFy}\qquad (P)\quad \frac{xPy} {yFx,xPy}$$

Alternative forms of rules (F) and (P) are discussed in Sect. 25.9.

The notions of an RL _TL -set and correctness of a rule are defined as in Sect. 2.4. Following the proof of correspondence for the RL _FCL -rules (S) and (R) in Theorem 13.3.2, it can be shown that the rules (F) and (P) are correct if and only if the conditions P ^{− 1} ⊆ F and F ⊆ P ^{− 1}, respectively, hold in all RL _TL -structures. Thus, based on correctness of RL(1, 1′)-rules and on correctness of the rule (tran R) proved in Sect. 6.6, we get:

Proposition 16.2.1.

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

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

The notions of an RL _TL -proof tree, a closed branch of such a tree, a closed RL _TL -proof tree, and RL _TL -provability are defined as in Sect. 2.4.

A branch b of an RL _TL -proof tree is complete whenever it is closed or it satisfies the completion conditions of RL(1, 1′)-dual tableau adjusted to RL _TL -language and the following conditions specific for the RL _TL -dual tableau:

For all object variables x and y and for every R ∈ {F, P},

Cpl(tran R) If xRy ∈ b, then for every object variable z, either xRz ∈ b or zRy ∈ b, obtained by an application of the rule (tran R);Cpl(F) If xFy ∈ b, then yPx ∈ b, obtained by an application of the rule (F);Cpl(P) If xPy ∈ b, then yFx ∈ b, obtained by an application of the rule (P).

The rules of RL _TL -dual tableau, in particular the specific rules listed above, guarantee that for every branch b of an RL _TL -proof tree, if xTy ∈ b and x − Ty ∈ b, for some atomic relational term T, then there is a node in the branch which contains both of these formulas, which implies that branch b is closed. Therefore, the closed branch property holds.

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

Let b be an open branch of an RL _TL -proof tree. The branch structure ${\mathcal{M}}^{b} = ({U}^{b},{F}^{b},{P}^{b},{m}^{b})$ is defined in a standard way (see Sect. 2.6), i.e., (U ^b, m ^b) is an RL(1, 1′)-branch model and m ^b(R) = { (x, y) ∈ U ^b ×U ^b : xRy ∉ b}, for every R ∈ {F, P}. Following the proof of the branch model property in the completeness proof of RL _EQ -dual tableau and RL _FCL -dual tableau (see Sects. 6.6 and 13.3, respectively), the branch model property for RL _TL -dual tableau can be proved. Since the branch model ${\mathcal{M}}^{b}$ is defined in a standard way and the closed branch property holds, the satisfaction in branch model property can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7). Hence, completeness of RL _TL -dual tableau follows.

Theorem 16.2.2 (Soundness and Completeness of RL _TL ).

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

• 1. φ is RL _TL -valid;

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

• 3. φ is RL _TL -provable.

The above theorem and Theorem 16.2.1 imply:

Theorem 16.2.3 (Relational Soundness and Completeness of TL).

Let φ be a TL-formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. φ is TL-valid;

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

3 Semantic Restrictions on Basic Temporal Logic

Various temporal logics are obtained from TL by assuming some properties of the time ordering F and P. Let R ∈ {F, P}. The following conditions on R are among the most typical:

For all x, y, and z,

• R is irreflexive: (x, x) ∉ R;

• R is serial: there exists y such that (x, y) ∈ R;

• R is unbound from below: R ^{− 1} is serial;

• R is discrete: (x, y) ∈ R implies (1) there exists z such that (x, z) ∈ R and for all t if (x, t) ∈ R, then (z, t) ∈ R, and (2) there exists z such that (z, y) ∈ R and for all t if (t, y) ∈ R, then (t, z) ∈ R;

• R is weakly connected: (x, y) ∈ R and (x, z) ∈ R imply (y, z) ∈ R or (z, y) ∈ R or y = z;

• R is connected: either (x, y) ∈ R or (y, x) ∈ R or x = y;

• R is dense: (x, y) ∈ R implies there exists z such that (x, z) ∈ R and (z, y) ∈ R;

• R is weakly directed: (x, y) ∈ R and (x, z) ∈ R imply there exists t such that (y, t) ∈ R and (z, t) ∈ R;

• R is Euclidean: (x, y) ∈ R and (x, z) ∈ R imply (y, z) ∈ R;

• R is partially functional: (x, y) ∈ R and (x, z) ∈ R imply y = z;

• R is functional: there exists exactly one y such that (x, y) ∈ R.

These properties of temporal ordering are of great importance in temporal reasoning. The adequate modelling of time scale should guarantee that any time moment does not precede itself. It seems that the most appropriate model for linear time scales is a strict total order which is irreflexive and connected. In several applications we need to distinguish between discrete and dense time scales, for example to model execution of computer programs, a discrete time is appropriate.

In what follows, any logic whose models are TL-models such that the relation R possibly satisfies some constraints from the above list is referred to as a standard temporal logic and is denoted by L _TL .It is always specified semantically in terms of a class of models.

The relational logic for an L _TL -logic is defined as in the previous section with the minor change of notation. We will write R and R ^{− 1} instead of F and P (or P and F), respectively, both in the language, in the structures, and in the models. An ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}}}$-structure is an RL _TL -model $\mathcal{M} = (U,R,{R}^{-1},m)$. An ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}}}$-model is an ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}}}$-structure such that the relation R satisfies all the conditions assumed in the L _TL -models.

As usual, we can prove the following:

Theorem 16.3.1.

Let L _TL be a standard temporal logic. Then for every L _TL -formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is L _TL -valid;

• 2. xτ(φ)y is $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -valid.

$\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$-dual tableaux are extensions of RL _TL -dual tableau with the specific rules and/or axiomatic sets that reflect properties of the relation R. Below we present the rules and axiomatic sets that reflect the properties of relations from the above list.

Connectivity of R leads to the following axiomatic set:

(Ax) {xRy, yRx, x1′y}.

Alternatively, connectivity can be expressed with a rule (see Sect. 25.9).

The rule that reflects irreflexivity can be found in Sect. 12.6. We recall that this rule has the following form:

$(\mbox{ irref }R)\quad \frac{} {xRx}\quad x\mbox{ is any object variable}$

The rules for the remaining properties have the following forms:

$$\begin{array}{ll} (\mathrm{ser}\ R) & \frac{} {x-(R\,;\,1)x}\quad x\ \text{ is any object variable} \\ (\mathrm{un}\ R) & \frac{} {x-({R}^{-1}\,;\,1)x}\quad x\ \text{ is any object variable} \\ ({\mathrm{dis}}_{1}\ R)& \frac{} {xRy\,\vert \,x-(-(R\,;\,-{R}^{-1})\,;\,{R}^{-1})x}\quad x,y\ \text{ are any object variables} \end{array}$$

$$\begin{array}{ll} ({\text{ dis}}_{2}\ R) & \frac{} {xRy\,\vert \,y-(-({R}^{-1}\,;\,-R)\,;\,R)y}\quad x,y\ \text{ are any object variables} \\ (\text{ wcon}\ R)& \frac{yRz,zRy,y1\prime z} {xRy,yRz,zRy,y1\prime z\,\vert \,xRz,yRz,zRy,y1\prime z} \\ &x\ \text{ is any object variable} \\ (\text{ den}\ R) & \frac{} {xRy\,\vert \,x-(R\,;\,R)y}\quad x,y\ \text{ are any object variables} \\ (\text{ wdir}\ R) & \frac{} {xRy\,\vert \,xRz\,\vert \,y-(R\,;\,{R}^{-1})z}\quad x,y,z\ \text{ are any object variables} \end{array}$$

$$\begin{array}{ll} (\mathrm{Euc}\ R) & \frac{yRz} {xRy,yRz\,\vert \,xRz,yRz}\quad x\ \text{ is any object variable} \\ (\mathrm{pfun}\ R)& \frac{y1\prime z} {xRy,y1\prime z\,\vert \,xRz,y1\prime z}\quad x\ \text{ is any object variable} \\ (\mathrm{fun}\ R) & \frac{} {xRy,x-(R\,;\,1)x\,\vert \,xRz,x-(R\,;\,1)x\,\vert \,y-1\prime z,x-(R\,;\,1)x} \\ &x,y,z\ \text{ are any object variables} \end{array}$$

Many of these rules have the form of a specialized cut rule. Some of them could be replaced by rules with a non-empty premise, and then an ordinary cut rule must be introduced to the dual tableau in question. This issue is discussed in detail in Sect. 25.9.

The rules (ser R), (dis₁ R), (dis₂ R), (wcon R), (den R), (wdir R), (Euc R), (pfun R), (fun R), and (un R) reflect that the relation R is serial, discrete, weakly connected, dense, weakly directed, Euclidean, partially functional, functional, and unbound from below, respectively. Introduction of any of these rules to the ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-dual tableau does not violate the closed branch property which can be proved as in Proposition 2.5.3.

Let L _TL be a standard temporal logic and let $\mathcal{K}$ be a class of L _TL -structures. The notion of a $\mathcal{K}$-set and the notion of $\mathcal{K}$-correctness are defined as in Sect. 2.4.

Theorem 16.3.2 (Correspondence).

Let L _TL be a standard temporal logic and let $\mathcal{K}$ be a class of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$ -structures. A condition (c) is true in the class $\mathcal{K}$ iff its corresponding rule(s) is(are) $\mathcal{K}$ -correct.

Proof.

By way of example, we prove the statement for a logic where relation R is dense and for a logic where R is discrete.

(den R) Let L _TL be a logic where relation R is dense. Assume that R is dense in every $\mathcal{K}$-structure. Let X be a finite set of $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$-formulas. Preservation of validity from the upper set to the lower sets is obvious. Now, assume that X ∪{ xRy} and X ∪{ x − (R ; R)y} are $\mathcal{K}$-sets and suppose X is not a $\mathcal{K}$-set. Then, by the assumption, there exist a $\mathcal{K}$-structure $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that (v(x), v(y)) ∈ R and for every z ∈ U either (v(x), z) ∉ R or (z, v(y)) ∉ R, a contradiction with density of R. Hence, the rule (den R) is $\mathcal{K}$-correct. Now, assume the rule (den R) is $\mathcal{K}$-correct. Let $X{ \mathrm{df} \atop =} \{x-Ry,x(R\,;\,R)y\}$. Then X ∪{ xRy} and X ∪{ x − (R ; R)y} are $\mathcal{K}$-sets. Thus, by the assumption, {x − Ry, x(R ; R)y} is a $\mathcal{K}$-set, which means that for every $\mathcal{K}$-structure $\mathcal{M}$ and for all x, y ∈ U if (x, y) ∈ R, then there exists z ∈ U such that (x, z) ∈ R and (z, y) ∈ R. Hence, R is dense.

(dis R) Let L _TL be a logic where relation R is discrete. Assume that R is discrete in every $\mathcal{K}$-structure. Let X be a finite set of $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$-formulas. Assume that X ∪{ xRy} and X ∪{ x − ( − (R ; − R ^{− 1}) ; R ^{− 1})x} are $\mathcal{K}$-sets and suppose X is not a $\mathcal{K}$-set. Then, by the assumption, there exist a $\mathcal{K}$-structure $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that (v(x), v(y)) ∈ R and for all z ∈ U either (v(x), z) ∉ R or there exists t ∈ U such that (v(x), t) ∈ R and (z, t) ∉ R, which contradicts discreteness of R. Preservation of validity from the upper set to the lower sets is obvious. Therefore, the rule (dis₁ R) is $\mathcal{K}$-correct. Correctness of the rule (dis₂ R) can be proved in a similar way. Now, assume that the rules (dis₁ R) and (dis₂ R) are $\mathcal{K}$-correct. We show that R is discrete in every $\mathcal{K}$-structure. Let $X{ \mathrm{df} \atop =} \{x-Ry,x(-(R\,;\,-{R}^{-1})\,;\,{R}^{-1})x\}$. Then, in every $\mathcal{K}$-structure the sets X ∪{ xRy} and X ∪{ x − ( − (R ; − R ^{− 1}) ; R ^{− 1})x} are $\mathcal{K}$-sets. Thus, by $\mathcal{K}$-correctness of the rule (dis₁ R), X is a $\mathcal{K}$-set, that is for all x, y ∈ U, if (x, y) ∈ R, then there exists z ∈ U such that (x, z) ∈ R and for all t ∈ U, if (x, t) ∈ R, then (z, t) ∈ R. Therefore, the part (1) of discreteness holds. In a similar way, correctness of the rule (dis₂ R) implies part (2) of discreteness.

The above theorem leads to the following:

Proposition 16.3.1.

Let L _TL be a standard temporal logic. Then:

• 1. The $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -rules are $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -correct;

• 2. The $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -axiomatic sets are $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -sets.

A branch b of an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-proof tree is complete whenever it is closed or it satisfies the completion conditions of ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}}}$-dual tableau and the following conditions specific for the ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}}}$-dual tableau:

For all object variables x, y, z,

Cpl(irref R) xRx ∈ b, obtained by an application of the rule (irref R);Cpl(ser R) x − (R ; 1)x ∈ b, obtained by an application of the rule (ser R);Cpl(un R) x − (R ^{− 1} ; 1)x ∈ b, obtained by an application of the rule (un R);Cpl(dis₁ R) Either xRy ∈ b or x − ( − (R ; − R ^{− 1}) ; R ^{− 1})x ∈ b, obtained by an application of the rule (dis₁ R);Cpl(dis₂ R) Either xRy ∈ b or y − ( − (R ^{− 1} ; − R) ; R)y ∈ b, obtained by an application of the rule (dis₂ R);Cpl(wcon R) If yRz ∈ b, zRy ∈ b, and y1′z ∈ b, then either xRy ∈ b or xRz ∈ b, obtained by an application of the rule (wcon R);Cpl(den R) Either xRy ∈ b or x − (R ; R)y ∈ b, obtained by an application of the rule (den R);Cpl(wdir R) Either xRy ∈ b or xRz ∈ b or y − (R ; R ^{− 1})z ∈ b, obtained by an application of the rule (wdir R);Cpl(Euc R) If yRz ∈ b, then either xRy ∈ b or xRz ∈ b, obtained by an application of the rule (Euc R);Cpl(pfun R) If y1′z ∈ b, then for every object variable x, either xRy ∈ b or xRz ∈ b, obtained by an application of the rule (pfun R);Cpl(fun R) x − (R ; 1)x ∈ b and either xRy ∈ b or xRz ∈ b or y − 1′z ∈ b, obtained by an application of the rule (fun R).

The notions of a complete ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-proof tree and an open branch of an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-proof tree are defined as in RL-logic (see Sect. 2.5).

Let b be an open branch of an $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$-proof tree. The branch structure ${\mathcal{M}}^{b} = ({U}^{b},{R}^{b},{({R}^{-1})}^{b},{m}^{b})$ is defined as in the completeness proof of RL _TL -dual tableau, in particular ${R}^{b} = {m}^{b}(R){ \mathrm{df} \atop =} \{(x,y)\,\in \,{U}^{b} \times {U}^{b} : xRy\not\in b\}$ and ${({R}^{-1})}^{b}{ \mathrm{df} \atop =} {({R}^{b})}^{-1}$.

Proposition 16.3.2 (Branch Model Property).

Let L _TL be a standard temporal logic. For every open branch b of an $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -proof tree, the branch structure ${\mathcal{M}}^{b} = ({U}^{b},{R}^{b},{({R}^{-1})}^{b},{m}^{b})$ is an $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -model.

Proof.

It suffices to show that if a condition is true in all models of a logic $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$, then it is true in ${\mathcal{M}}^{b}$.

By way of example, we show that this holds for a logic L _TL whose models have a discrete relation R. Then, the dual tableau for $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ contains rules (dis₁ R) and (dis₂ R). By the completion condition Cpl(dis₁ R), for all x, y ∈ U ^b, either xRy ∈ b or x − ( − (R ; − R ^{− 1}) ; R ^{− 1})x ∈ b. Thus, by the completion conditions Cpl( − ; ), Cpl( − ), and Cpl( − ^{− 1}), for all x, y ∈ U ^b, either xRy ∈ b or for some z ∈ U ^b, x(R ; − R ^{− 1})z ∈ b and x − Rz ∈ b. Thus, by the completion conditions Cpl(; ) and Cpl( − ^{− 1}), if (x, y) ∈ R ^b, then there exists z ∈ U ^b such that (x, z) ∈ R ^b and if (x, t) ∈ R ^b, then (z, t) ∈ R ^b. On the other hand, by the completion condition Cpl(dis₂ R), it can be proved that if (x, y) ∈ R ^b, then there exists z ∈ U ^b such that (z, y) ∈ R ^b and if (t, y) ∈ R ^b, then (t, z) ∈ R ^b. Therefore, R ^b is discrete.

The satisfaction in branch model property can be proved as in RL _TL -logic. Therefore, we get:

Theorem 16.3.3 (Soundness and Completeness of $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$).

Let L _TL be a standard temporal logic and let φ be an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$ -formula. Then the following conditions are equivalent:

• 1. φ is $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -valid;

• 2. φ is true in all standard $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -models;

• 3. φ is $\mathsf{R{L}_{{\mathsf{L}}_{\mathsf{TL}}}}$ -provable.

The above theorem and Theorem 16.3.1 imply:

Theorem 16.3.4 (Relational Soundness and Completeness of L _TL ).

Let L _TL be a standard temporal logic and let φ be an L _TL -formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. φ is L _TL -valid;

• 2. xτ(φ)y is ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$ -provable.

Example.

Let ${\mathsf{L}}_{\mathsf{TL}}^{1}$ be a standard temporal logic whose models have an Euclidean relation R. Figure 16.1 presents an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}^{1}}$-proof of the formula:

$$\varphi =\langle R\rangle p \rightarrow [R]\langle R\rangle p,$$

which reflects this property.

Fig. 16.1

An ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}^{1}}$-proof of the formula ⟨R⟩p → [R]⟨R⟩p

Let ${\mathsf{L}}_{\mathsf{TL}}^{2}$ be a standard temporal logic whose models have a dense relation R. Figure 16.2 presents an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}^{2}}$-proof of the formula

$$\psi = [R][R]p \rightarrow [R]p.$$

Fig. 16.2

An ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}^{2}}$-proof of the formula [R][R]p → [R]p

For simplicity, we write P instead of τ(p). The relational translation of φ and ψ are:

$$\tau (\varphi ) = -(R\,;\,P) \cup -(R\,;\,-(R\,;\,P)),$$

$$\tau (\psi ) = --(R\,;\,--(R\,;\,-P)) \cup -(R\,;\,-P).$$

In the following sections we present some signature extensions of the basic temporal logic.

4 Temporal Logics with Since and Until

In languages of temporal logics we often admit binary operations Since and Untilwith the following semantics. Let R be a temporal ordering, then:

• $\mathcal{M},s\models \varphi \,\mathit{Since}\,\psi$ iff there exists s′ ∈ U such that (s′, s) ∈ R and $\mathcal{M},s\prime\ \models \ \psi$ and for all u ∈ U, if (s′, u) ∈ R and (u, s) ∈ R, then $\mathcal{M},u\models \varphi$;

• $\mathcal{M},s\models \varphi \,\mathit{Until}\,\psi$ iff there exists s′ ∈ U such that (s, s′) ∈ R and $\mathcal{M},s\prime\models \psi$ and for all u ∈ U, if (s, u) ∈ R and (u, s′) ∈ R, then $\mathcal{M},u\models \varphi$.

A formula φ Since ψ means that there is a past moment s′ at which ψ is satisfied and at all moments between s′ and now φ is satisfied. Similarly, φ Until ψ says that there is a future moment s′ at which ψ is satisfied and φ is satisfied at all moments between now and s′. In the presence of Until the next-state operation, Next, is definable in the modal language:

• $\mathcal{M},s\models \mathit{Next}\,\varphi$ iff $\mathcal{M},s\models (\varphi \wedge \neg \varphi )\mathit{Until}\,\varphi$.

Let TL _SU denote a temporal logic with a time ordering R and operations Since, Until, and Next. To define a relational representation of TL _SU -formulas, we extend the set of relational terms of TL by admitting relational counterparts of logical operations Since, Until, and Next among the relational operations. For the sake of simplicity, they are denoted in the same way as the respective propositional operations. Namely, the vocabulary of the language of logic ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ is the RL(1, 1′)-language such that:

• ${\mathbb{O}\mathbb{C}}_{{\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}} = \varnothing$;

• ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}} =\{ 1,1\prime ,R\}$, where R is the relational constant representing the time ordering;

• {Since,Until,Next} is included in the set of relational operations.

The set of relational terms is obtained from ${\mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{{ \mathsf{TL}}_{ \mathsf{SU}}}} \cup \{ 1,1\prime ,R\}$ by making its closure with respect to the standard relational operations and the operations Since, Until, and Next.

${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-structures are of the form $\mathcal{M} = (U,R,{R}^{-1},m)$, where (U, m) is an RL(1, 1′)-model, R = m(R) is a binary relation on U satisfying all the conditions assumed in TL _SU -logic, and the relational operations Since, Until, and Next are interpreted as operations on binary relations on U. ${\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}$-models are ${\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}$-structures $\mathcal{M} = (U,R,{R}^{-1},m)$ such that the relational operations Since, Until, and Next are interpreted as follows. Let T, Q be relational terms, then:

• $m(T\,\mathit{Since}\,Q){ \mathrm{df} \atop =} \{(x,y) : \exists t[(t,x)\,\in \,R \wedge (t,y)\,\in \,m(Q) \wedge \forall u\,((t,u)\,\in \,R \wedge (u,x)\,\in \,R \rightarrow (u,u)\,\in \,m(T)]\}$;

• $m(T\,\mathit{Until}\,Q){ \mathrm{df} \atop =} \{(x,y) : \exists t[(x,t)\,\in \,R \wedge (t,y)\,\in \,m(Q) \wedge \forall u\,((x,u)\,\in \,R \wedge (u,t)\,\in \,R \rightarrow (u,u)\,\in \,m(T)]\}$;

• $m(\mathit{Next}\,T){ \mathrm{df} \atop =} \{(x,y) : \exists t[(x,t)\,\in \,R \wedge (t,y)\,\in \,m(T) \wedge \neg \exists u\,((x,u)\,\in \,R \wedge (u,t)\,\in \,R)]\}$.

This interpretation of the operations Since, Until, and Next is motivated with the role that they play in the representation of TL _SU -formulas which are interpreted as right ideal relations (see translation function defined on p. 35 and Theorem 16.4.1).

The next proposition shows that operations Since, Until, and Next are definable in the logic RL(1, 1′). It is due to the fact that their relational definitions involve implicitly the information that the relations to which they apply are meant to be right ideal relations. For the reasons of readability, we will identify symbols of the language with the corresponding entities in the models, if it does not lead to a confusion. In particular, we will omit the symbol of a meaning function.

Proposition 16.4.1.

For every ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -model $\mathcal{M} = (U,R,{R}^{-1},m)$ and for all relations T and Q on U the following hold:

• 1. T Since Q = (R ∩−(R ; (−T ∩ 1′) ; R))⁻¹ ; Q;

• 2. T Until Q = (R ∩−(R ⁻¹ ; (−T ∩ 1′) ; R ⁻¹ ) ⁻¹ ) ; Q;

• 3. Next T = (R ∩−(R ; R)) ; T.

Proof.

Let $\mathcal{M} = (U,R,{R}^{-1},m)$ be an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-model, let T and Q be relations on U, and let x, y ∈ U. First, note that the following holds: ( ∗ ) (t, x) ∈ R ; ( − T ∩ 1′) ; R iff there exists u ∈ U such that (t, u) ∈ R and (u, x) ∈ R and (u, u) ∉ T. Indeed, (t, x) ∈ R ; ( − T ∩ 1′) ; R iff there exist u, v ∈ U such that (t, v) ∈ R, (v, u) ∉ T, (v, u) ∈ 1′, and (u, x) ∈ R. Therefore, if the left side of ( ∗ ) holds, then it can be easily proved, by the extensionality property of RL(1, 1′)-models (see Sect. 2.7), that the right side of ( ∗ ) also holds. Conversely, if the right side of ( ∗ ) holds, then taking v : = u the left side also holds.

To prove 1., note that (x, y) ∈ (R ∩ − (R ; ( − T ∩ 1′) ; R))^{− 1} ; Q) iff there exists t ∈ U such that (t, x) ∈ R and (t, y) ∈ Q and (t, x) ∉ R ; ( − T ∩ 1′) ; R. By ( ∗ ), the latter is equivalent to: there exists t ∈ U such that (t, x) ∈ R and (t, y) ∈ Q and for all u ∈ U if (t, u) ∈ R and (u, x) ∈ R, then (u, u) ∈ T, which is equivalent to (x, y) ∈ T Since Q.

2. and 3. can be proved in a similar way.

The translation of TL _SU -formulas into relational terms is defined by an extension of the function τ defined in Sect. 7.4 with the following clauses:

• τ(φ Since ψ) = τ(φ) Since τ(ψ);

• τ(φ Until ψ) = τ(φ) Until τ(ψ);

• τ(Next φ) = Next τ(φ).

In view of Proposition 7.4.1, it is easy to check that the relational terms, obtained from temporal formulas built with operations Since, Until, and Next, represent right ideal relations. Therefore, the following can be proved in a similar way as Theorem 7.4.1:

Theorem 16.4.1.

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

• 1. φ is TL _SU -valid;

• 2. xτ(φ)y is $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$ -valid.

Proof.

It suffices to show that Propositions 7.4.2 and 7.4.3 are true for all TL _SU -formulas. For that purpose, we need to show:

• (1) For every TL _SU -model $\mathcal{M} = (U,R,{R}^{-1},m)$ there exists an $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$-model $\mathcal{M}\prime = (U,R,{R}^{-1},m\prime)$ with the same universe and the same relation R as those in $\mathcal{M}$, and such that for all s, s′ ∈ U and for every TL _SU -formula φ of the form ψ Since $\vartheta$, ψ Until $\vartheta$, and Next ψ, the following holds:

  $$({_\ast})\;\mathcal{M},s\models \varphi \mbox{ iff }(s,s\prime)\,\in \,m\prime(\tau (\varphi ));$$

• (2) For every standard ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-model $\mathcal{M}\prime = (U,R,{R}^{-1},m\prime)$ there exists a TL _SU -model $\mathcal{M} = (U,R,{R}^{-1},m)$ with the same universe and the same relation R as those in $\mathcal{M}\prime$, and such that for all s, s′ ∈ U and for every TL _SU -formula φ of the form ψ Since $\vartheta$, ψ Until $\vartheta$, and Next ψ, ( ∗ ) holds.

Then, the rest of the proof is similar to the proof of Theorem 7.4.1.

By way of example, we prove (1). Let $\mathcal{M} = (U,R,{R}^{-1},m)$ be a TL _SU -model. Then we define $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$-model $\mathcal{M}\prime = (U,R,{R}^{-1},m\prime)$ as in the proof of Proposition 7.4.2, namely:

• m′(1) = U ×U;

• m′(1′) is the identity on U;

• m′(τ(p)) = { (x, y) ∈ U ×U : x ∈ m(p)}, for every propositional variable p;

• m′(R) = R;

• m′ extends to all the compound terms as in ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models.

Let $\varphi = \psi \,\mathit{Since}\,{\vartheta}$ and let s, s′ ∈ U. Assume that $\mathcal{M},s\models \varphi$, that is there exists t ∈ U such that (t, s) ∈ R, $\mathcal{M},t\models {\vartheta}$, and for all u ∈ U, if (t, u) ∈ R and (u, s) ∈ R, then $\mathcal{M},u\models \psi$. Then, by the induction hypothesis, this is equivalent to: there exists t ∈ U such that (t, s) ∈ R and $(t,s\prime)\,\in \,m\prime(\tau ({\vartheta}))$ and for all u ∈ U, if (t, u) ∈ R and (u, s) ∈ R, then (u, s′) ∈ m′(τ(ψ)). Since τ(ψ) is a right ideal relation, by Proposition 7.4.1, (u, s′) ∈ m′(τ(ψ)) iff (u, u) ∈ m′(τ(ψ)). Hence, $(s,s\prime)\,\in \,m\prime(\tau (\psi )\mathit{Since}\,\tau ({\vartheta}))$.

In a similar way we can prove that ( ∗ ) holds for the formulas of the form $\psi \,\mathit{Until}\,{\vartheta}$ and Next ψ.

${\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}$-dual tableau is an extension of RL(1, 1′)-dual tableau with the rules and the axiomatic sets reflecting properties of the relation R and with the rules corresponding to the new relational operations Since, Until, and Next. These rules have the following forms:

For all object variables x, y and for all relational terms T and Q,

$$\begin{array}{ll} (\mathit{Since})& \frac{x(T\,\mathit{Since}\,Q)y} {tRx,K\,\vert \,tQy,K\,\vert \,t-(R\,;\,(-T \cap 1\prime)\,;\,R)x,K} \\ &K = x(T\,\mathit{Since}\,Q)y,\,t\ \text{ is any object variable}\\ \end{array}$$

$$\begin{array}{ll} (-\mathit{Since})& \frac{x-(T\,\mathit{Since}\,Q)y} {t-Rx,t-Qy,t(R\,;\,(-T \cap 1\prime)\,;\,R)x} \\ &t\ \text{ is a new object variable} \end{array}$$

$$\begin{array}{ll} (\mathit{Until})& \frac{x(T\,\mathit{Until}\,Q)y} {xRt,K\,\vert \,tQy,K\,\vert \,t-({R}^{-1}\,;\,(-T \cap 1\prime)\,;\,{R}^{-1})x,K} \\ &K = x(T\,\mathit{Until}\,Q)y,\,t\ \text{ is any object variable}\\ \end{array}$$

$$\begin{array}{ll} (-\mathit{Until})& \frac{x-(T\,\mathit{Until}\,Q)y} {x-Rt,t-Qy,t({R}^{-1}\,;\,(-T \cap 1\prime)\,;\,{R}^{-1})x} \\ &t\ \text{ is a new object variable}\\ \end{array}$$

$$\begin{array}{ll} (\mathit{Next})& \frac{x(\mathit{Next}\,T)y} {xRt,x(\mathit{Next}\,T)y\,\vert \,tTy,x(\mathit{Next}\,T)y\,\vert \,x-(R\,;\,R)t,x(\mathit{Next}\,T)y} \\ &\,t\ \text{ is any object variable} \end{array}$$

$$\begin{array}{ll} (-\mathit{Next})& \frac{x-(\mathit{Next}\,T)y} {x-Rt,t-Ty,x(R\,;\,R)t} \\ &t\ \text{ is a new object variable} \end{array}$$

Theorem 16.4.2 (Correspondence).

Let $\mathcal{K}$ be a class of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -structures. Then $\mathcal{K}$ is a class of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -models iff the rules (#) and (−#) are $\mathcal{K}$ -correct for every # ∈ { Since,Until,Next}.

Proof.

( → ) Assume that $\mathcal{K}$ is a class of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models. We need to show that for every # ∈ {Since,Until,Next}, the rules (#) and ( − #) are $\mathcal{K}$-correct. By way of example, we show it for the operation Since.

Let X be a finite set of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-formulas. Clearly, if the upper set of formulas in the rule (Since) is a $\mathcal{K}$-set, then all the lower sets of formulas in the rule are also $\mathcal{K}$-sets. Now, assume that X ∪{ tRx, x(T Since Q)y}, X ∪{ tQy, x(T Since Q)y}, and X ∪{ t − (R ; ( − T ∩ 1′) ; R)x, x(T Since Q)y} are $\mathcal{K}$-sets and suppose that X ∪{ x(T Since Q)y} is not a $\mathcal{K}$-set. Then there exist an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-model $\mathcal{M} = (U,R,{R}^{-1},m)$ in $\mathcal{K}$ and a valuation v in $\mathcal{M}$ such that (v(x), v(y)) ∉ m(T Since Q). By the assumption, there exists t ∈ U such that (v(t), v(x)) ∈ R and (v(t), v(y)) ∈ m(Q) and (v(t), v(x)) ∉ m(R ; ( − T ∩ 1′) ; R). By Proposition 16.4.1, (v(x), v(y)) ∈ m(T Since Q), a contradiction.

Now, we prove that the rule ( − Since) is $\mathcal{K}$-correct. Let X be a finite set of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-formulas. Let t be a variable that does not occur in X and let x, y≠t. Assume that X ∪{ t − Rx, t − Qy, t(R ; ( − T ∩ 1′) ; R)x} is a $\mathcal{K}$-set and suppose that X ∪{ x − (T Since Q)y} is not a $\mathcal{K}$-set. Then there exist an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-model $\mathcal{M} = (U,R,{R}^{-1},m)$ in $\mathcal{K}$ and a valuation v in $\mathcal{M}$ such that (v(x), v(y)) ∈ m(T Since Q). By the assumption and since t does not occur in X ∪{ x − (T Since Q)y}, for all t ∈ U either (t, v(x)) ∉ R or (t, v(y)) ∉ m(Q) or (t, v(x)) ∈ m(R ; ( − T ∩ 1′) ; R). By Proposition 16.4.1, (v(x), v(y)) ∉ m(T Since Q), a contradiction.

( ← ) Let $\mathcal{K}$ be a class of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-structures. Assume that for every # ∈ {Since, Until,Next} the rules (#) and ( − #) are $\mathcal{K}$-correct. We show that $\mathcal{K}$ is a class of ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models, that is that the meaning of the operations Since, Until, and Next is as in ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models defined on p. 33. By way of example, we show it for Until. By Proposition 16.4.1, we need to show that $\mathcal{K}$-correctness of the rules (Until) and ( − Until) implies m(T Until Q) = m((R ∩ − (R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1}))^{− 1} ; Q).

( ⊇ ) Let $X{ \mathrm{df} \atop =} \{x-Rt,t-Qy,t({R}^{-1}\,;\,(-T \cap 1\prime)\,;\,{R}^{-1})x\}$. Then, clearly all the sets X ∪{ xRt, x(T Until Q)y}, X ∪{ tQy, x(T Until Q)y}, and X ∪{ t − (R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1})x, x(T Until Q)y} are $\mathcal{K}$-sets. By $\mathcal{K}$-correctness of the rule (Until), X ∪{ x(T Until Q)y} is a $\mathcal{K}$-set, which means that if (x, y) ∈ m((R ∩ − (R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1}))^{− 1} ; Q), then (x, y) ∈ m(T Until Q).

( ⊆ ) Let $X{ \mathrm{df} \atop =} \{x{(R \cap -({R}^{-1}\,;\,(-T \cap 1\prime)\,;\,{R}^{-1}))}^{-1}\,;\,Qy\}$ and let x, y≠t. Then, X ∪{ x − Rt, t − Qy, t(R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1})x} is a $\mathcal{K}$-set. Thus, by $\mathcal{K}$-correctness of the rule ( − Until), X ∪{ x − (T Until Q)y} is a $\mathcal{K}$-set, which means that if (x, y) ∈ m(T Until Q), then (x, y) ∈ m((R ∩ − (R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1}))^{− 1} ; Q).

By the above theorem and since correctness of the remaining rules can be proved as in ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-logics (see Proposition 16.2.1 and Theorem 16.3.2), we have:

Proposition 16.4.2.

• 1. The $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$ -rules are $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$ -correct;

• 2. The $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$ -axiomatic sets are $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$ -sets.

The completion conditions determined by the rules for operations Since, Until, and Next are:

For all object variables x, y and for all relational terms T and Q,

Cpl(Since) If x(T Since Q)y ∈ b, then for every object variable t, either tRx ∈ b or tQy ∈ b or t − (R ; ( − T ∩ 1′) ; R)x ∈ b, obtained by an application of the rule (Since);Cpl( − Since) If x − (T Since Q)y ∈ b, then for some object variable t, t − Rx ∈ b and t − Qy ∈ b and t(R ; ( − T ∩ 1′) ; R)x ∈ b, obtained by an application of the rule ( − Since);Cpl(Until) If x(T Until Q)y ∈ b, then for every object variable t, either xRt ∈ b or tQy ∈ b or t − (R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1})x ∈ b, obtained by an application of the rule (Until);Cpl( − Until) If x − (T Until Q)y ∈ b, then for some object variable t, x − Rt ∈ b and t − Qy ∈ b and t(R ^{− 1} ; ( − T ∩ 1′) ; R ^{− 1})x ∈ b, obtained by an application of the rule ( − Until);Cpl(Next) If x(Next T)y ∈ b, then for every object variable t, either xRt ∈ b or tTy ∈ b or x − (R ; R)t ∈ b, obtained by an application of the rule (Next);Cpl( − Next) If x − (Next T)y ∈ b, then for some variable t, x − Rt ∈ b and t − Ty ∈ b and x(R ; R)t ∈ b, obtained by an application of the rule ( − Next).

As in ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-logics, every branch that contains formulas xTy and x − Ty, for some atomic relational term T, is closed. Thus, the closed branch property holds.

Let b be an open branch of an $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$-proof tree. The branch structure ${\mathcal{M}}^{b} = ({U}^{b},{R}^{b},{({R}^{-1})}^{b},{m}^{b})$ is defined in a standard way, namely:

• ${U}^{b} ={ \mathbb{O}\mathbb{V}}_{{\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}}$;

• R ^b = m ^b(R) and (R ^{− 1})^b = (R ^b)^{− 1};

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

• m ^b extends to all the compound relational terms as in ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models.

It follows from this definition that ${\mathcal{M}}^{b}$ is an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-model, so the branch model property is satisfied. Actually, we only need to prove that the time ordering R ^b satisfies all the conditions assumed in ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-models. This can be done as in the completeness proof of ${\mathsf{RL}}_{\mathsf{T{L}_{L}}}$-dual tableaux presented in the previous section.

Proposition 16.4.3 (Satisfaction in Branch Model Property).

Let b be an open branch of an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -proof tree. Then for every ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -formula φ, ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ implies φ∉b.

Proof.

Let b be an open branch of an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-proof tree. The proof is by induction on the complexity of formulas. If φ is of the form xTy or x − Ty for some atomic relational term T, we prove the above condition as in RL-logic (see the proof of Proposition 2.5.5). Then, we show that the condition holds for the compound relational terms. By way of example, we show it for Next.

Assume ${\mathcal{M}}^{b},{v}^{b}\models x(\mathit{Next}\,T)y$, Then, by Proposition 16.4.1, (x, y) ∈ m ^b((R ∩ − (R ; R)) ; T). Suppose x(Next T)y ∈ b. Then, by the completion condition Cpl(Next), for every t ∈ U ^b, either xRt ∈ b or tTy ∈ b or x − (R ; R)t ∈ b. By the completion condition Cpl( − ; ), for every t ∈ U ^b, either xRt ∈ b or tTy ∈ b or for some u ∈ U ^b both x − Ru ∈ b and u − Rt ∈ b. By the induction hypothesis, for every t ∈ U ^b, either (x, t) ∉ R ^b or (t, y) ∉ m ^b(T) or for some u ∈ U ^b both (x, u) ∈ R ^b and (u, t) ∈ R ^b. Therefore, (x, y) ∉ m ^b((R ∩ − (R ; R)) ; T), a contradiction.

Assume ${\mathcal{M}}^{b},{v}^{b}\models x-(\mathit{Next}\,T)y$, Then, (x, y) ∉ m ^b((R ∩ − (R ; R)) ; T). Suppose x − (Next T)y ∈ b. Then, by the completion condition Cpl( − Next), for some t ∈ U ^b the following hold: xRt ∉ b, tTy ∉ b, and x(R ; R)t ∈ b. By the completion condition Cpl(; ), there exists t ∈ U ^b such that xRt ∉ b and tTy ∉ b and for all u ∈ U ^b, either xRu ∈ b or uRt ∈ b. Thus, by the induction hypothesis, there exists t ∈ U ^b such that (x, t) ∈ R ^b and (t, y) ∈ m ^b(T) and for all u ∈ U ^b, either (x, u) ∉ R ^b or (u, t) ∉ R ^b. Therefore, (x, y) ∈ m ^b((R ∩ − (R ; R)) ; T), a contradiction.

Therefore, we have:

Theorem 16.4.3 (Soundness and Completeness of $\mathsf{R{L}_{{\mathsf{TL}}_{\mathsf{SU}}}}$).

For every ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -formula φ, the following conditions are equivalent:

• 1. φ is ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -valid;

• 2. φ is true in all standard ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -models;

• 3. φ is ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -provable.

The theorem above and Theorem 16.4.1 imply:

Theorem 16.4.4 (Relational Soundness and Completeness of TL _SU ).

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

• 1. φ is TL _SU -valid;

• 2. xτ(φ)y is ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$ -provable.

Example. Let φ be the following formula:

$$\varphi = (p \wedge \langle R\rangle (p \wedge [{R}^{-1})\neg q)] \rightarrow \neg q\,\mathit{Until}\,p.$$

Its relational translation is:

$$\tau (\varphi ) = -((P\,;\,1) \cap (R\,;\,((P\,;\,1) \cap -({R}^{-1}\,;\,--(Q\,;\,1))))) \cup (-(Q\,;\,1)\mathit{Until}(P\,;\,1)),$$

where τ(p) = P ; 1 and τ(q) = Q ; 1. TL _SU -validity of φ is equivalent to ${\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{SU}}}$-provability of the formula xτ(φ)y. Figure 16.3 presents an ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-proof of φ.

Fig. 16.3

An ${\mathsf{RL}}_{{\mathsf{TL}}_{\mathsf{SU}}}$-proof of [p ∧ ⟨R⟩(p ∧ [R ^{− 1}] ¬q)] → ¬q Until p

5 Standard Temporal Logics with Nominals

Temporal logics with nominals were considered by Arthur Prior [Pri67] and Robert Bull [Bul70] in the late 1960s. Nominals are propositional constants interpreted as singleton sets. In computer science nominals were introduced to the dynamic logic in [Pas84] and then studied in [PT85]. In temporal languages both nominals and propositional variables are considered as atomic formulas.

Given a model $\mathcal{M} = (U,R,{R}^{-1},m)$, we define the satisfaction of nominals:

• $\mathcal{M},s\models c$ iff m(c) = { s}.

An extensive study of nominals can be found in [Bla90].

Nominals increase drastically expressiveness of modal languages. Below we list examples of classes of relations which are not definable in a modal language with a single accessibility relation, unless the language contains the nominals (see e.g., [Bla90]).

• R is irreflexive: c → ¬⟨R⟩c;

• R is antisymmetric: c → [R](⟨R⟩c → c);

• R is directed: ⟨R⟩⟨R ^{− 1}⟩c;

• R is connected: ⟨R ^{− 1}⟩c ∨ c ∨ ⟨R⟩c;

• R is discrete: c → (⟨R⟩(φ ∨ ¬φ) → ⟨R⟩[R ^{− 1}][R ^{− 1}] ¬c).

Let a logic $\mathsf{TL}(\mathbb{C})$ be obtained from the temporal logic TL by extending its language with a set $\mathbb{C}$ of nominals. Its models are TL-models $\mathcal{M} = (U,F,P,m)$ such that m(c) ∈ U, for every $c\,\in \,\mathbb{C}$ (see Sect. 7.3). In analogy to logics considered in Sect. 16.3, we consider standard temporal logics with nominals, ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$, based on $\mathsf{TL}(\mathbb{C})$. The corresponding relational logics are based on the relational logic with point relations introduced with axioms. The logic is defined in Sect. 3.2.

Let ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ be a standard temporal logic with the set $\mathbb{C}$ of nominals. With every nominal $c\,\in \,\mathbb{C}$, we associate a relational constant C _c . Then, a relational logic appropriate for expressing ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-formulas, ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}(\mathbb{C})}}$, is based on logic ${\mathsf{RL}}_{\mathit{a}x}(\{{C}_{c} : c\,\in \,\mathbb{C}\})$ which is an instance of the logics considered in Sect. 3.2. The set of relational constants of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ is $\{1,1\prime,R\} \cup \{ {C}_{c} : c\,\in \,\mathbb{C}\}$, where R represents the time ordering and $\{{C}_{c} : c\,\in \,\mathbb{C}\}$ is the set of relational constants representing nominals from $\mathbb{C}$.

${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-models are structures $\mathcal{M} = (U,R,{R}^{-1},m)$ such that (U, m) is an ${\mathsf{RL}}_{\mathit{a}x}(\{{C}_{c} : c\,\in \,\mathbb{C}\})$-model, as defined in Sect. 3.2, and R = m(R) is the relation on U that satisfies all the conditions assumed in ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-models.

The translation of ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-formulas into relational terms is defined as in Sect. 7.4 (p. 158), that is τ(c) = C _c ; 1. As usual, the translation is defined so that it preserves the validity of formulas. Due to Theorem 7.4.1, we have:

Theorem 16.5.1.

Let ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ be a standard temporal logic with nominals. For every ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ -formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ -valid;

• 2. xτ(φ)y is ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -valid.

${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}(\mathbb{C})}}$-dual tableau is an extension of ${\mathsf{RL}}_{\mathit{a}x}(\{{C}_{c}\,:\,c\,\in \,\mathbb{C}\})$-dual tableau with the rules reflecting the properties of the time ordering R. We recall that the specific rules of ${\mathsf{RL}}_{\mathit{a}x}(\{{C}_{c} : c\,\in \,\mathbb{C}\})$-dual tableau are (see Sect. 3.2):

For all object symbols x and y and for every $c\,\in \,\mathbb{C}$,

$$\begin{array}{lll} (C1)\,&\, \frac{} {z-{C}_{c}t}\, &\,z,t\ \text{ are new object variables and}\ z\neq t \\ (C2)\,&\, \frac{x{C}_{c}y} {x{C}_{c}z,x{C}_{c}y}\, &\,z\ \text{ is any object symbol} \\ (C3)\,&\, \frac{x1\prime y} {x{C}_{c}z,x1\prime y\,\vert \,y{C}_{c}z,x1\prime y}\,&\,z\ \text{ is any object symbol} \end{array}$$

Soundness and completeness of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-dual tableau follow from soundness and completeness of ${\mathsf{RL}}_{\mathit{a}x}(\{{C}_{c} : c\,\in \,\mathbb{C}\})$-dual tableau (see Theorem 3.2.1) and ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}}}$-dual tableaux for standard temporal logics (see Theorem 16.3.3). Hence, we have:

Theorem 16.5.2 (Soundness and Completeness of ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$).

Let ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ be a standard temporal logic with nominals. Then, for every ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -formula φ, the following conditions are equivalent:

• 1. φ is ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -valid;

• 2. φ is true in all standard ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -models;

• 3. φ is ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -provable.

By the above and Theorem 16.5.1, we obtain:

Theorem 16.5.3 (Relational Soundness and Completeness of ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$).

Let ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ be a temporal logic with nominals. Then, for every ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ -formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$ -valid;

• 2. x(τ(φ))y is ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$ -provable.

Example.

The formula:

$$\varphi = c \rightarrow \neg \langle R\rangle c$$

defines irreflexivity of relation R, hence it is true in all ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures in which R is irreflexive. The translation of φ is:

$$\tau (\varphi ) = -({C}_{c}\,;\,1) \cup -(R\,;\,({C}_{c}\,;\,1)),$$

where τ(c) = C _c ; 1. Then, φ is valid in all irreflexive ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures iff xτ(φ)y is provable in ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-dual tableau with the rule (irref R) presented in Sect. 16.3. Figure 16.4 presents an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-proof of xτ(φ)y which shows that φ is true in all irreflexive ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures.

Fig. 16.4

An ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-proof showing that c → ¬⟨R⟩c is true in all irreflexive ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures

The formula:

$$\psi =\langle {R}^{-1}\rangle c \vee c \vee \langle R\rangle c$$

defines connectivity of relation R, thus ψ is true in all ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures in which R is connected. The translation of ψ is:

$$\tau (\psi ) = ({R}^{-1}\,;\,({C}_{ c}\,;\,1)) \cup ({C}_{c}\,;\,1) \cup (R\,;\,({C}_{c}\,;\,1)),$$

where τ(c) = C _c ; 1. Then, validity of ψ in all connected ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures is equivalent to ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-provability of xτ(ψ)y. ${\mathsf{RL}}_{{\mathsf{L}}_{ \mathsf{TL}(\mathbb{C})}}$-dual tableau includes axiomatic sets (Ax), presented in Sect. 16.3 (p. 14), that reflect connectivity of R. Figure 16.5 presents an ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-proof of xτ(ψ)y.

6 Temporal Information Logics

Temporal information logic TIL considered in the present section was developed to provide a means of reasoning in temporal databases where properties of objects change with the lapse of time. In logic TIL we intend to represent data that have the form of a description of time varying properties of objects. For example, we are interested in such attributes as Height, Temperature, Blood Pressure, usually at given moments of time. Further, their change in a given time interval may be of essential importance too. For that purpose, we include in information systems a parameter which represents the moment to which an information about values of attributes applies.

Fig. 16.5

An ${\mathsf{RL}}_{{\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}}$-proof showing that ⟨R ^{− 1}⟩c ∨ c ∨ ⟨R⟩c is true in all connected ${\mathsf{L}}_{\mathsf{TL}(\mathbb{C})}$-structures

By a dynamic information system (see [Orł82]) we mean a system of the form $\mathcal{S} = (\mathbb{O}\mathbb{B}, \mathbb{T},R, \mathbb{A}\mathbb{T},\{{ \mathbb{V}\mathbb{A}\mathbb{L}}_{a} : a\,\in \,\mathbb{A}\mathbb{T}\},f)$, where $\mathbb{O}\mathbb{B}$ is a non-empty set of objects, $\mathbb{T}$ is a non-empty set of moments of time, R is an ordering on a set $\mathbb{T}$, $\mathbb{A}\mathbb{T}$ is a non-empty set of attributes, ${\mathbb{V}\mathbb{A}\mathbb{L}}_{a}$, for $a\,\in \,\mathbb{A}\mathbb{T}$, is a non-empty set of values of attribute a, f is a function $f : \mathbb{O}\mathbb{B} \times \mathbb{T} \times \mathbb{A}\mathbb{T} \rightarrow \bigcup \nolimits \{{ \mathbb{V}\mathbb{A}\mathbb{L}}_{a} : a\,\in \,\mathbb{A}\mathbb{T}\}$, such that $f(x,t,a)\,\in \,{\mathbb{V}\mathbb{A}\mathbb{L}}_{a}$, for all $x\,\in \,\mathbb{O}\mathbb{B}$, $t\,\in \,\mathbb{T}$, and $a\,\in \,\mathbb{A}\mathbb{T}$.

As an example, consider Table 16.1 containing partial results of photoelectric observations of stars, presented in the Astrophysical Journal.

Table 16.1 A dynamic information system

The table can be treated as a dynamic information system such that the set $\mathbb{O}\mathbb{B}$ of objects consists of the stars, that is $\mathbb{O}\mathbb{B}\,=\,$ S Canis Minoris, R Caneri, R Leonis, T Centauri}, the set $\mathbb{T}$ of moments of time consists of non-negative real numbers representing Julian Days given in the second column of the table, relation R is the natural order in the set of real numbers restricted to the set $\mathbb{T}$, the set $\mathbb{A}\mathbb{T}$ of attributes consists of two wavelength regions of spectrum, $\mathbb{A}\mathbb{T} =\{ visual(V ),blue-visual(B-V )\}$, the set $\mathbb{V}\mathbb{A}\mathbb{L}$ of values of attributes consists of the magnitudes of a star in the given wavelength regions.

The language of logic TIL is a language of basic temporal logic with specific atomic formulas. An atomic piece of information in an information system is a statement of the form: an object x assumes a value v of an attribute a. Hence, instead of propositional variables, we admit structured atomic formulas built with syntactic components of three types. Let $\mathbb{O}\mathbb{V}$, $\mathbb{A}\mathbb{V}$, and $\mathbb{A}\mathbb{V}\mathbb{V}$ be sets of object variables, attribute variables, and attribute value variables, respectively. They are arbitrary, pairwise disjoint, countable sets. Then, the atomic formulas** of the language are of the form (o, a, v), for $o\,\in \,\mathbb{O}\mathbb{V}$, $a\,\in \,\mathbb{A}\mathbb{V}$, and $v\,\in \,\mathbb{A}\mathbb{V}\mathbb{V}$. The compound formulas are built from atomic formulas with the usual propositional operations of temporal logics.

We define semantics of the logic TIL by means of notion of a model determined by a dynamic information system. By a TIL-model we mean any pair $\mathcal{M} = (\mathcal{S},m)$, where $\mathcal{S} = (\mathbb{O}\mathbb{B}, \mathbb{T},R, \mathbb{A}\mathbb{T},$ $\{{\mathbb{V}\mathbb{A}\mathbb{L}}_{a} : a\,\in \,\mathbb{A}\mathbb{T}\},f)$ is a dynamic information system, and m is a meaning function which assigns objects to object variables, attributes to attribute variables, and values of attributes to attribute value variables: $m(o)\,\in \,\mathbb{O}\mathbb{B}$, $m(a)\,\in \,\mathbb{A}\mathbb{T}$, $m(v)\,\in \,\bigcup \nolimits \{{ \mathbb{V}\mathbb{A}\mathbb{L}}_{a} : a\,\in \,\mathbb{A}\mathbb{T}\}$. We define satisfaction of formulas in a moment of time in the usual way (see Sect. 7.3), with the exception that for atomic formulas we have:

• $\mathcal{M},t\models (o,a,v)$ iff f(m(o), t, m(a)) = m(v).

The relational logic RL _TIL corresponding to the logic TIL is similar to the relational logic for the basic temporal logic. The minor difference is that the relational variables are indexed with triples of the form (o, a, v). Models of the relational logic for TIL are determined by dynamic information systems in the same way as the respective TIL-models. As usual, the translation starts with a one-to-one assignment of relational variables P _{(o, a, v)} to the atomic TIL-formulas (o, a, v). Let τ′ be such an assignment. Then the translation τ of TIL-formulas into RL _TIL -terms is defined as in Sect. 7.4 with the following clause for atomic formulas: $\tau (o,a,v){ \mathrm{df} \atop =} {P}_{(o,a,v)}\,;\,1$.

In view of Proposition 7.4.1, it is easy to check that the relational terms obtained from TIL-formulas represent right ideal relations. Therefore, the following can be proved in a similar way as Theorem 7.4.1:

Theorem 16.6.1.

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

• 1. φ is TIL-valid;

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

Proof.

It suffices to show that Propositions 7.4.2 and 7.4.3 are true for all TIL-formulas. Thus, we need to show that for every TIL-model $\mathcal{M}$ there exists a standard RL _TIL -model $\mathcal{M}\prime$ that satisfies the same TIL-formulas as model $\mathcal{M}$, and that for every RL _TIL -model $\mathcal{M}\prime$ there exists a TIL-model $\mathcal{M}$ that satisfies the same TIL-formulas as $\mathcal{M}\prime$. If a TIL-model $\mathcal{M}$ is given, then the model $\mathcal{M}\prime$ is defined as a standard RL _TIL -model such that the interpretation of a relational variable P _{(o, a, v)} is a right ideal relation whose domain is the set of the form {x : f(m(o), x, m(a)) = m(v)}. If an RL _TIL -model $\mathcal{M}\prime$ is given, then the model $\mathcal{M}$ is defined as a TIL-model such that the interpretation of an atomic formula (o, a, v) is the domain of the relation P _{(o, a, v)}. The rest of the proof is similar to the proof of Theorem 7.4.1.

RL _TIL -dual tableau is an ${\mathsf{RL}}_{{\mathsf{TL}}_{ \mathsf{L}}}$-dual tableau adjusted to the RL _TIL -language and extended with the rule of the following form:

For all object variables x and y,

$$\begin{array}{ll} (\mathsf{TIL})& \frac{x{P}_{(o,a,v)}y} {x{P}_{(o\prime,a\prime,v\prime)}y,x{P}_{(o,a,v)}y\,\vert \,x{P}_{(o\prime,a\prime,v)}y,x{P}_{(o,a,v)}y\,\vert \,x{P}_{(o,a,v\prime)}y,x{P}_{(o,a,v)}y} \\ &\text{ for any}\ o\prime\,\in \,\mathbb{O}\mathbb{V},\ a\prime\,\in \,\mathbb{A}\mathbb{V},\ \mathrm{and}\ v\prime\,\in \,\mathbb{A}\mathbb{V}\mathbb{V} \end{array}$$

The rule (TIL) reflects the following property of relations P _{(o, a, v)}: in an underlying information system, given an object, a moment of time, and an attribute, the function f assigns a unique value of the attribute to this triple.

The completion condition determined by this rule is:

For all object variables x and y, Cpl(TIL) If xP _{(o, a, v)} y ∈ b, then for all $o\prime\,\in \,\mathbb{O}\mathbb{V}$, $a\prime\,\in \,\mathbb{A}\mathbb{V}$, and $v\prime\,\in \,\mathbb{A}\mathbb{V}\mathbb{V}$, either xP _{(o′, a′, v′)} y ∈ b or xP _{(o′, a′, v)} y ∈ b or xP _{(o, a, v′)} y ∈ b.

Proofs of all the propositions needed for proving soundness and completeness of RL _TIL follow the analogous proofs in the logics RL _TL and ${\mathsf{RL}}_{\mathsf{{L}_{TL}}}$ presented in the previous sections of this chapter. Thus, we have:

Theorem 16.6.2 (Soundness and Completeness of RL _TIL ).

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

• 1. φ is RL _TIL -valid;

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

• 3. φ is RL _TIL -provable.

By the above and Theorem 16.6.1, we get:

Theorem 16.6.3 (Relational Soundness and Completeness of TIL).

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

• 1. φ is TIL-valid;

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