1 Introduction

Order of magnitude reasoning is a reasoning in terms of qualitative ranges of variables instead of their precise values. More precisely, the order of magnitude approach enables us the reasoning in terms of relative magnitudes of variables obtained by comparisons of the sizes of quantities. In a sense, order of magnitude methods of reasoning are situated midway between numerical methods and qualitative formalisms.

The logical approaches to order of magnitude reasoning can be found in [BOO04, BOA05, BMVOA06]. These approaches are based on a system with two landmarks and with relations of comparability and negligibility. The intuitive representation of the underlying models can be illustrated with the linearly ordered set of real numbers, where two landmarks − α and + α are considered.

In the picture, − α and + α represent the greatest negative observable and the least positive observable, respectively, partitioning the real line into classes of positive observable numbers, Obs +, negative observable numbers, Obs −, and non-observable (also called infinitesimal) numbers, Inf. This choice makes sense, in particular, when considering physical metric spaces in which we always have a smallest unit which can be measured; however, it is not possible to identify a least or a greatest non-observable number.

figure 1

Consider the following example which illustrates a concept of comparability. Assume one aims at specifying the behavior of a device for automatic control of the speed of a car; assume the system has to maintain the speed close to some speed limit v. For practical purposes, any value in an interval [v − ε, v + ε] for small ε is admissible. The extreme points of this interval can then be considered as the landmarks − α and + α; furthermore, the sets { Obs} −, { Inf}, and { Obs} + can be interpreted as Slow, Adequate, and High speed.

Regarding negligibility, the representation capabilities of a pocket calculator provide an illustrative example of a relation of that kind. In such a device, it is not possible to present any number whose absolute value is less than 10− 99. Therefore, it makes sense to consider − α = − 10− 99 and + α = + 10− 99 since any number between − 10− 99 and 10− 99 cannot be observed or presented. On the other hand, a number x can be said to be negligible with respect to y provided that the difference y − x cannot be distinguished from y. Numerically, and assuming 8 + 2 (digits and mantissa) display, this amounts to stating that x is negligible with respect to y if and only if y − x > 108. Furthermore, this example suggests a real-life model in which, for instance, − 1000 is negligible with respect to − 1. This is even more suggestive if we interpret the numbers as exponents, since 10− 1000 certainly can be considered negligible with respect to 10− 1.

In this chapter we consider a logic OMR of order of magnitude reasoning introduced in [BOO04] and we present a relational dual tableau for this logic based on the developments in [BMVOA06]. In the logic we deal with the comparability and negligibility relations. They determine modal operators which enable us to specify statements about properties of physical systems within the ranges of values of variables. The deduction tool of dual tableau for OMR provides a means for verifying these statements. Decidability of the logic OMR is an open problem.

2 A Multimodal Logic of Order of Magnitude Reasoning

The language of the logic OMR of order of magnitude reasoning is a multimodal propositional language with three types of modal operations, each of which is associated with a certain relation: [ < ] and [ < − 1] to deal with an ordering of the elements of a system, the operations [⊏] and [⊏ − 1] to deal with a comparability relation ⊏, and the operations [ ≺ ] and [ ≺ − 1] to deal with a negligibility relation ≺.

The intuitive meaning of the modal operations is as follows:

[ < ]φ – φ is true for all numbers which are greater than the current one;[ < − 1]φ – φ is true for all numbers which are less than the current one;[⊏]φ – φ is true for all numbers which are greater than and comparable with the current one;[⊏ − 1]φ – φ is true for all numbers which are less than and comparable with the current one;[ ≺ ]φ – φ is true for all numbers with respect to which the current one is negligible;[ ≺ − 1]φ – φ is true for all numbers which are negligible with respect to the current one.

Formulas of the language are constructed with symbols from the following pairwise disjoint sets:

  • \(\mathbb{V}\) – a set of propositional variables;

  • {c −, c +} – the set of object constants representing the landmarks;

  • { <, ⊏, ≺ } – the set of relational constants representing ordering, comparability, and negligibility, respectively;

  • ¬, ∨, ∧ } – the set of classical propositional operations;

  • \(\{[<],[{< }^{-1}],[\sqsubset ],[{\sqsubset }^{-1}],[\prec ],[{\prec }^{-1}]\}\) – the set of unary modal operations.

OMR-formulas are generated from the elements of \(\mathbb{V} \cup \{ {c}^{-},{c}^{+}\}\) with the propositional operations.

An OMR-model is a structure \(\mathcal{M} = (U,<,\sqsubset,\prec,{c}^{-},{c}^{+},m)\), where U is a non-empty set, c − and c + are designated elements of U which, for the sake of simplicity, are denoted with the same symbols as the constants of the language, and m is a meaning function satisfying the following conditions:

  • m(p) ⊆ U, for every \(p \in \mathbb{V}\);

  • < is a strict linear ordering on U, that is for all x, y, z ∈ U, the following conditions are satisfied:

    (irref < )  (x, x) ∉ <,(tran < ) If (x, y) ∈ < and (y, z) ∈ <, then (x, z) ∈ <,(con < )   (x, y) ∈ < or (y, x) ∈ < or x = y;

  • m(c −) = c −, m(c +) = c + and (c −, c +) ∈ < ; then the sets { Obs} +, { Inf}, and { Obs} − are defined by: Obs \({}^{-}{ \mathrm{df} \atop =} \{x \in U : (x,{c}^{-}) \in <\mbox{ or }x = {c}^{-}\}\), Inf \({ \mathrm{df} \atop =} \{x \in U : ({c}^{-},x) \in <\mbox{ and }(x,{c}^{+}) \in <\}\), Obs \({}^{+}{ \mathrm{df} \atop =} \{x \in U : ({c}^{+},x) \in <\mbox{ or }{c}^{+} = x\}\);

  • ⊏ is a binary relation on U called the comparability relation:

    \(\sqsubset { \mathrm{df} \atop =} < \cap \big{(}({<Emphasis Type="SmallCaps">\text{ Obs}</Emphasis>}^{-}\times {<Emphasis Type="SmallCaps">\text{ Obs}</Emphasis>}^{-}) \cup (<Emphasis Type="SmallCaps">\text{ Inf}</Emphasis> \times <Emphasis Type="SmallCaps">\text{ Inf}</Emphasis>) \cup ({<Emphasis Type="SmallCaps">\text{ Obs}</Emphasis>}^{+} \times {<Emphasis Type="SmallCaps">\text{ Obs}</Emphasis>}^{+})\big{)}\), that is for any x, y ∈ U, (x, y) ∈ ⊏ iff either of the following conditions is satisfied:

    (i ⊏)   (x, y) ∈ <, ((x, c −) ∈ < or x = c −), and ((y, c −) ∈ < or y = c −),(ii ⊏)   (x, y) ∈ <, (c −, x) ∈ <, (x, c +) ∈ <, (c −, y) ∈ <, and (y, c +) ∈ <,(iii ⊏)   (x, y) ∈ <, (c +, x) ∈ < or c + = x), and (c +, y) ∈ < or c + = y);

  • ≺ is a binary relation on U called the negligibility relation and satisfying the following conditions:(i ≺ )   ≺ ⊆ <,(ii ≺ )   If (x, y) ∈ ≺ and (y, z) ∈ <, then (x, z) ∈ ≺,(iii ≺ )   If (x, y) ∈ < and (y, z) ∈ ≺, then (x, z) ∈ ≺,(iv ≺ )   If (x, y) ∈ ≺, then either x∉{ Inf} or y∉{ Inf}.

Note that as a consequence of items (ii ≺ ) and (iii ≺ ), the relation ≺ is transitive; item (iv ≺ ) states that two non-observable elements cannot be compared by the negligibility relation.

Let φ be an OMR-formula and let \(\mathcal{M} = (U,<,\sqsubset,\prec,m)\) be an OMR-model. The satisfaction of φ in \(\mathcal{M}\) by a state s ∈ U, \(\mathcal{M},s\models \varphi \) for short, is defined as follows:

  • \(\mathcal{M},s\models p\) iff s ∈ m(p), for every \(p \in \mathbb{V}\);

  • \(\mathcal{M},s\models {c}^{\#}\) iff s = c #, for # ∈ {−, +};

  • \(\mathcal{M},s\models \neg \varphi \) iff not \(\mathcal{M},s\models \varphi \);

  • \(\mathcal{M},s\models (\varphi \vee \psi )\) iff \(\mathcal{M},s\models \varphi \) or \(\mathcal{M},s\models \psi \);

  • \(\mathcal{M},s\models (\varphi \wedge \psi )\) iff \(\mathcal{M},s\models \varphi \) and \(\mathcal{M},s\models \psi \);

    For T ∈ { <, ⊏, ≺ },

  • \(\mathcal{M},s\models [T]\varphi \) iff for all s′ ∈ U, (s, s′) ∈ T implies \(\mathcal{M},s\prime\models \varphi \);

  • \(\mathcal{M},s\models [{T}^{-1}]\varphi \) iff for all s′ ∈ U, (s, s′) ∈ T − 1 implies \(\mathcal{M},s\prime\models \varphi \).

3 Dual Tableau for the Logic of Order of Magnitude Reasoning

A relational logic for representation of OMR-formulas, RL OMR , is an instance of the relational logic \({\mathsf{RL}}_{\mathit{df }}(\mathbb{C})\) presented in Sect. 3.3. The vocabulary of its language consists of symbols from the following pairwise disjoint sets:

  • \({\mathbb{O}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{OMR}}}\) – a set of object variables;

  • \({\mathbb{O}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{OMR}}} =\{ {c}^{-},{c}^{+}\}\) – the set of object constants corresponding to the distinguished elements from the OMR-models;

  • \({\mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{OMR}}}\) – a set of binary relational variables;

  • \({\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{OMR}}} =\{ 1,1\prime,<,\sqsubset,\prec,{C}^{-},{C}^{+}\}\) – the set of relational constants where C − and C + are intended to be point relations representing the landmarks;

  • { −, ∪, ∩ ;, − 1} – the set of relational operations.

The set of RL OMR -relational terms and the set of RL OMR -formulas are defined in a standard way (see Sect. 3.3).

An RL OMR -model is a structure \(\mathcal{M} = (U,<,\sqsubset,\prec,{c}^{-},{c}^{+},m)\), where U is a non-empty set, c − and c + are designated elements of U, and m is a meaning function satisfying the following conditions:

  • m(c −) = c −, m(c +) = c +;

  • m(R) ⊆ U ×U, for every \(R \in { \mathbb{R}\mathbb{A}}_{{\mathsf{RL}}_{\mathsf{OMR}}}\);

  • m(1′) and m(1) are defined as in RL(1, 1′)-models;

  • m( < ) = < is irreflexive, transitive, and it satisfies the following condition for all x, y ∈ U:

    $$\rm(con\prime) \, \rm Either (x,y) \in <\mbox{ or }(y,x) \in <\rm{ or }(x,y) \in m(1\prime);$$

  • (c −, c +) ∈ < ; as in OMR-models, the linearity of < enables us to partition U into the classes { Obs} −, { Obs} +, and Inf which are defined as in OMR-models with a difference that equality is replaced by m(1′) that may not be the identity (for a discussion of that issue see Sect. 2.7);

  • \(m(\sqsubset ) = \sqsubset = < \cap \big{(}({<Emphasis Type="SmallCaps">\text{ OBS}</Emphasis>}^{-}\times {<Emphasis Type="SmallCaps">\text{ OBS}</Emphasis>}^{-}) \cup (<Emphasis Type="SmallCaps">\text{ INF}</Emphasis> \times <Emphasis Type="SmallCaps">\text{ INF}</Emphasis>) \cup ({<Emphasis Type="SmallCaps">\text{ OBS}</Emphasis>}^{+} \times { <Emphasis Type="SmallCaps">\text{ OBS}</Emphasis>}^{+})\big{)}\), that is for any x, y ∈ U, (x, y) ∈ ⊏ iff either of the following conditions is satisfied:

    • (x, y) ∈ <, ((x, c −) ∈ < or (x, c −) ∈ m(1′)), and ((y, c −) ∈ < or (y, c −) ∈ m(1′)),

    • (x, y) ∈ <, (c −, x) ∈ <, (x, c +) ∈ <, (c −, y) ∈ <, and (y, c +) ∈ <,

    • (x, y) ∈ <, ((c +, x) ∈ < or (c +, x) ∈ m(1′)), and (c +, y) ∈ < or (c +, y) ∈ m(1′));

  • m( ≺ ) = ≺ satisfies all the constraints posed on the relation ≺ in OMR-models;

  • m(C #) = { x ∈ U : (x, c #) ∈ m(1′)} ×U, for # ∈ {−, +};

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

As in RL(1, 1′)-logic, an RL OMR -model in which m(1′) is interpreted as the identity is called a standard RL OMR -model. Note that if m(1′) is the identity on U, then m(C #) = { c #} ×U, # ∈ {−, +}, that is it is a point relation whose domain represents a landmark.

The validity preserving translation assigning relational terms to modal formulas is defined as in the classical modal logic (see Sect. 7.4) with the following additional clauses:

For # ∈ {−, +},

  • τ(c #) = C # ; 1.

For T ∈ { <, ⊏, ≺ },

  • τ([T]φ) = − (T ; − τ(φ));

  • τ([T − 1]φ) = − (T − 1 ; − τ(φ)).

By Theorem 7.4.1, in a similar way as in the classical modal logics, we obtain:

Theorem 15.3.1.

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

  • φ is OMR-valid;

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

A relational dual tableau for RL OMR consists of axiomatic sets and decomposition and specific rules of RL(1, 1′)-dual tableau adjusted to the language of RL OMR and the rules specific for RL OMR listed below.

The rule that reflects irreflexivity of < is an instance of the rule (irref R) presented in Sect. 12.6. The rule reflecting transitivity of < is presented in Sect. 6.6 (see also Sect. 7.4). Recall that these rules have the following forms:

For all object symbols x and y,

$$\begin{array}{llll} (\mathrm{irref}\ <)& \frac{} {x < x} &\qquad (\mathrm{tran}\ <)& \frac{x < y} {x < z,x < y\;\vert \;z < y,x < y} \\ & & &\text{ for every object symbol}\ z \end{array}$$

The rules for the comparability relation ⊏ that express its properties have the following forms:

For all object symbols x and y,

(r(i’ ⊏)) \(\frac{x \sqsubset y} {x < y,x \sqsubset y\,\vert \,x < {c}^{-},x1\prime{c}^{-},x \sqsubset y\,\vert \,y < {c}^{-},y1\prime{c}^{-},x \sqsubset y}\)

(r(ii’ ⊏)) \(\frac{x \sqsubset y} {x < y,x \sqsubset y\,\vert \,{c}^{-}<\,x,x \sqsubset y\,\vert \,x < {c}^{+},x \sqsubset y\,\vert \,{c}^{-}<\,y,x \sqsubset y\,\vert \,y < {c}^{+},x \sqsubset y}\)

(r(iii’ ⊏)) \(\frac{x \sqsubset y} {x < y,x \sqsubset y\,\vert \,{c}^{+}<\,x,{c}^{+}1\prime x,x \sqsubset y\,\vert \,{c}^{+}<\,y,{c}^{+}1\prime y,x \sqsubset y}\)

( − ⊏)   \(\frac{x-\sqsubset \,y} {{H}_{1}\,\vert \,{H}_{2}\,\vert \,{H}_{3}}\), where:

H 0 = { y < x, x1′y};

H 1 = H 0 ∪{ c − < x, c − < y, x − ⊏ y};

H 2 = H 0 ∪{ x < c −, x1′c −, c + < x, c +1′x, y < c −, y1′c −, c + < y, c +1′y, x − ⊏ y};

H 3 = H 0 ∪{ x < c +, y < c +, x − ⊏ y}.

The rules for the negligibility relation ≺ reflecting its properties have the following forms:

For all object symbols x and y,

(r(i ≺ )) \(\frac{x < y} {x \prec y,x < y}\)

(r(ii ≺ )) \(\frac{x \prec y} {x \prec z,x \prec y\;\vert \;z < y,x \prec y}\) for every object symbol z

(r(iii ≺ )) \(\frac{x \prec y} {x < z,x \prec y\;\vert \;z \prec y,x \prec y}\) for every object symbol z

(r(iv ≺ )) \(\frac{x < {c}^{-},x1\prime{c}^{-},{c}^{+}<\,x,{c}^{+}1\prime x,y < {c}^{-},y1\prime{c}^{-},{c}^{+}<\,y,{c}^{+}1\prime y} {x \prec y,x < {c}^{-},x1\prime{c}^{-},{c}^{+}<\,x,{c}^{+}1\prime x,y < {c}^{-},y1\prime{c}^{-},{c}^{+}<\,y,{c}^{+}1\prime y}\)

The rules for the relational constants C #, # ∈ {−, +} are:

For all object symbols x and y,

$$\begin{array}{llll} ({C}^{\#})&\ \, \frac{x{C}^{\#}y} {x1\prime{c}^{\#},x{C}^{\#}y} &\qquad (-{C}^{\#})&\ \, \frac{x-{C}^{\#}y} {x-1\prime{c}^{\#},x-{C}^{\#}y} \end{array}$$

Note that applications of the rules of RL OMR -dual tableau, in particular applications of the specific rules listed above, preserve the formulas built with atomic terms or their complements. Thus, the closed branch property holds.

The specific RL OMR -axiomatic sets are those including either of the following sets:

(Ax1) {c − < c +};

(Ax2) {x < y, y < x, x1′y}, for any object symbols x and y.

An alternative representation of the connectivity condition from the OMR-models can be provided by a rule in the RL OMR -dual tableau. This issue is discussed in Sect. 25.9, see also Sect. 25.6.

The notions of an RL OMR -set and RL OMR -correctness of a rule are defined as in Sect. 2.4.

Proposition 15.3.1.

  1. 1.

    The RL OMR -decomposition rules are RL OMR -correct;

  2. 2.

    The RL OMR -specific rules are RL OMR -correct;

  3. 3.

    The RL OMR -axiomatic sets are RL OMR -sets.

Proof.

The proof of 1. follows the proof of RL-correctness of the decomposition rules (see Proposition 2.5.1).

For 2., by way of example, we prove RL OMR -correctness of the rule (r(iv ≺ )). Let X be a finite set of RL OMR -formulas.

(r(iv ≺ ))  Assume that X ∪{x ≺ y, x < c −, x1′c −, c + < x, c +1′x, y < c −, y1′c −, c + < y, c +1′y} is an RL OMR -set. Suppose X ∪{ x < c −, x1′c −, c + < x, c +1′x, y < c −, y1′c −, c + < y, c +1′y} is not an RL OMR -set. Then there exist an RL OMR -model \(\mathcal{M}\) and valuation v in \(\mathcal{M}\) such that for every φ ∈ X, \(\mathcal{M},v\nvDash \varphi \). Hence, by linearity of <, all the following conditions are satisfied: (c −, v(x)) ∈ <, (v(x), c +) ∈ <, (c −, v(y)) ∈ <, and (v(y), c +) ∈ <. These conditions imply that v(x), v(y) ∈ { Inf}, thus by the condition (iv ≺ ), (v(x), v(y)) ∉ ≺. However, by the assumption, (v(x), v(y)) ∈ ≺, a contradiction. Preservation of validity from the upper set to the lower set is obvious.

Correctness of the remaining specific rules follows from the corresponding assumption in the RL OMR -models.

For 3., note that for every RL OMR -model \(\mathcal{M}\), (c −, c +) ∈ <, thus the sets including {c − < c +} are RL OMR -sets. Similarly, by connectivity of <, sets of the form X ∪ {x < y, x − < y, x1′y} are RL OMR -sets.

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

The completion conditions determined by the rules (irref < ) and (tran < ) are the instances of the completion conditions presented in Sects. 12.6 and 6.6, respectively. The completion conditions determined by the rules that are specific for RL OMR -dual tableau have the following forms:

For all object symbols x and y,

Cpl(r(i’ ⊏))  If x⊏y ∈ b, then either x < y ∈ b or (x < c − ∈ b and x1′c − ∈ b) or (y < c − ∈ b and y1′c − ∈ b), obtained by an application of the rule (r(i’ ⊏));Cpl(r(ii’ ⊏))  If x⊏y ∈ b, then either x < y ∈ b or c − < x ∈ b or x < c + ∈ b or c − < y ∈ b or y < c + ∈ b, obtained by an application of the rule (r(ii’ ⊏));Cpl(r(iii’ ⊏))  If x⊏y ∈ b, then either x < y ∈ b or (c + < x ∈ b and c +1′x ∈ b) or (c + < y ∈ b and c +1′y ∈ b), obtained by an application of the rule (r(iii’ ⊏));Cpl( − ⊏)  If x − ⊏ y ∈ b, then either of the following conditions is satisfied:

  • y < x ∈ b, x1′y ∈ b, c − < x ∈ b, and c − < y ∈ b,

  • y < x ∈ b, x1′y ∈ b, x < c − ∈ b, x1′c − ∈ b, c + < x ∈ b, c +1′x ∈ b, y < c − ∈ b, y1′c − ∈ b, c + < y ∈ b, and c +1′y ∈ b,

  • y < x ∈ b, x1′y ∈ b, x < c + ∈ b, and y < c + ∈ b,

obtained by an application of the rule ( − ⊏);Cpl(r(i ≺ ))  If x < y ∈ b, then x ≺ y ∈ b, obtained by an application of the rule (r(i ≺ ));Cpl(r(ii ≺ ))  If x ≺ y ∈ b, then for every object symbol z, either x ≺ z ∈ b or z < y ∈ b, obtained by an application of the rule (r(ii ≺ ));Cpl(r(iii ≺ ))  If x ≺ y ∈ b, then for every object symbol z, either x < z ∈ b or z ≺ y ∈ b, obtained by an application of the rule (r(iii ≺ ));Cpl(r(iv ≺ ))  If x < c − ∈ b, x1′c − ∈ b, c + < x ∈ b, c +1′x ∈ b, y < c − ∈ b, y1′c − ∈ b, c + < y ∈ b, and c +1′y ∈ b, then x ≺ y ∈ b, obtained by an application of the rule (r(iv ≺ ));Cpl(C #)  If xC # y ∈ b, then x1′c # ∈ b, obtained by an application of the rule (C #);Cpl( − C #)  If x − C # y ∈ b, then x − 1′c # ∈ b, obtained by an application of the rule ( − C #).

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

Let b be an open branch of an RL OMR -proof tree. A branch structure \({\mathcal{M}}^{b} = ({U}^{b},{< }^{b},{\sqsubset }^{b},{\prec }^{b},{({c}^{-})}^{b},{({c}^{+})}^{b},{m}^{b})\) is defined as follows:

  • \({U}^{b} ={ \mathbb{O}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{OMR}}} \cup \{ {c}^{-},{c}^{+}\}\);

  • (c #)b = m b(c #) = c #, for # ∈ {−, +};

  • m b(R) = { (x, y) ∈ U b ×U b : xRy ∉ b}, for \(R \in { \mathbb{R}\mathbb{A}}_{{\mathsf{RL}}_{\mathsf{OMR}}}\setminus \{\sqsubset,{C}^{-},{C}^{+}\}\);

  • < b = m b( < ) and ≺ b = m b( ≺ );

  • ⊏ b = m b(⊏), m b(C −), and m b(C +) are defined as in RL OMR -models;

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

Proposition 15.3.2 (Branch Model Property).

Let b be an open branch of an RL OMR -proof tree. The branch structure \({\mathcal{M}}^{b} = ({U}^{b},{< }^{b},{\sqsubset }^{b},{\prec }^{b},{({c}^{-})}^{b},{({c}^{+})}^{b},{m}^{b})\) is an RL OMR -model.

Proof.

Obviously, c # ∈ U b, for # ∈ {−, +}. Moreover, since {c − < c +} is an axiomatic set, c − < c + ∉ b, hence ((c −)b, (c +)b) ∈ < b.

Now, it suffices to show that ≺ b satisfies all the conditions assumed in RL OMR -models.

By Cpl(irref < ), for every x ∈ U b, x < x ∈ b, that is (x, x) ∉ < b. Hence, < b is irreflexive. Assume that for some x, y, z ∈ U b, (x, y) ∈ < b, (y, z) ∈ < b, but (x, z) ∉ < b. Then x < y ∉ b, y < z ∉ b, and x < z ∈ b. By Cpl(tran < ) and since x < z ∈ b, either x < y ∈ b or y < z ∈ b, a contradiction. Therefore, < b is transitive. Since {x < y, y < x, x1′y} is an axiomatic set, for all x, y ∈ U b, either x < y ∉ b or y < x ∉ b or x1′y ∉ b. Thus, for all x, y ∈ U b, either (x, y) ∈ < b or (y, x) ∈ < b or (x, y) ∈ m b(1′). Hence, < b is linear.

The linearity of < b enables us to partition U b into classes ({ OBS} −)b, ({ OBS} +)b, and { INF} b as defined on p. 10. Then, conditions (i ≺ ), (ii ≺ ), and (iii ≺ ) follow directly from the completion conditions Cpl(r(i ≺ )), Cpl(r(ii ≺ )), and Cpl(r(iii ≺ )), respectively.

Now, we prove that ≺ b satisfies the condition (iv ≺ ). Assume that for some x, y ∈ U b, (x, y) ∈ ≺ b, but x ∈ { Inf} b and y ∈ { Inf} b. Due to irreflexivity and transitivity of < b and extensionality property of m b(1′) (see the proof of Proposition 2.7.5) it is easy to prove that for all x, y ∈ U b, if (x, y) ∈ < b, then (y, x) ∉ < b ∪m b(1′). Thus, since x ∈ { Inf} b and y ∈ { Inf} b, we obtain (x, c −) ∉ < b ∪m b(1′), (c +, x) ∉ < b ∪m b(1′), (y, c −) ∉ < b ∪m b(1′), and (c +, y) ∉ < b ∪m b(1′). Thus all the following formulas belong to b: x < c −, x1′c −, c + < x, c +1′x, y < c −, y1′c −, c + < y, and c +1′y. Then, by the completion condition Cpl(r(iv ≺ )), x ≺ y ∈ b, so (x, y) ∉ ≺ b, a contradiction. Therefore, the condition (iv ≺ ) is satisfied.

A valuation v b in \({\mathcal{M}}^{b}\) is defined in a standard way, that is v b(x) = x, for every x ∈ U b.

Proposition 15.3.3 (Satisfaction in Branch Model Property).

Let b be an open branch of an RL OMR -proof tree. Then for every RL OMR -formula φ, if \({\mathcal{M}}^{b},{v}^{b}\models \varphi \) , then φ∉b.

Proof.

Let b be an open branch of an RL OMR -proof tree. The proof is by induction on the complexity of formulas. For a formula φ of the form xRy or x − Ry, where \(R \in { \mathbb{R}\mathbb{A}}_{{\mathsf{RL}}_{\mathsf{OMR}}}\setminus \{\sqsubset,{C}^{-},{C}^{+}\}\), the proof is as in RL-logic and it uses the closed branch property (see the proof of Proposition 2.5.5). Now, it suffices to show that the proposition holds for formulas of the form xRy and formulas of the form x − Ry, for R ∈ {⊏, C −, C +}. By way of example, we prove it for R = − ⊏.

Assume \({\mathcal{M}}^{b},{v}^{b}\models x-\sqsubset \,y\), i.e., (x, y) ∉ ⊏ b. Suppose x − ⊏ y ∈ b. Then by the completion condition Cpl( − ⊏) and symmetry of m b(1′), either of the following conditions is satisfied:

  • (y, x) ∉ < b ∪m b(1′), (c −, x) ∉ < b, and (c −, y) ∉ < b;

  • (y, x) ∉ < b ∪m b(1′), (x, c −) ∉ < b ∪m b(1′), (c +, x) ∉ < b ∪m b(1′), (y, c −) ∉ < b ∪m b(1′), and (c +, y) ∉ < b ∪m b(1′);

  • (y, x) ∉ < b ∪m b(1′), (x, c +) ∉ < b, and (y, c +) ∉ < b.

Thus, by the linearity of < b, either of the following conditions is satisfied:

  • (x, y) ∈ < b, (x, c −) ∈ < b ∪m b(1′), and (y, c −) ∈ < b ∪m b(1′);

  • (x, y) ∈ < b, (c −, x) ∈ < b, (x, c +) ∈ < b, (c −, y) ∈ < b, and (y, c +) ∈ < b;

  • (x, y) ∈ < b, (c +, x) ∈ < b ∪m b(1′), and (c +, y) ∈ < b ∪m b(1′).

Therefore, (x, y) ∈ ⊏ b, a contradiction. For the compound relational terms the proofs are similar to those in RL-logic.

Fig. 15.1
figure 2

An RL OMR -proof of the formula ¬c − ∨ [⊏]p

Full size image

Finally, we obtain:

Theorem 15.3.2 (Soundness and Completeness of RL OMR ).

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

  1. 1.

    φ is RL OMR -valid;

  2. 2.

    φ is true in all standard RL OMR -models;

  3. 3.

    φ is RL OMR -provable.

By the above theorem and Theorem 15.3.1, we have:

Theorem 15.3.3 (Relational Soundness and Completeness of OMR).

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

  1. 1.

    φ is OMR-valid;

  2. 2.

    xτ(φ)y is RL OMR -provable.

Example.

Consider an OMR-formula:

$$\varphi = \neg {c}^{-}\vee [\sqsubset ]p.$$

The translation of φ to an RL OMR -relational term is:

$$\tau (\varphi ) = -{C}^{-}\cup -(\sqsubset \,;\,-P),$$

where for simplicity of notation, τ(p) = P. By Theorem 15.3.3, for all object symbols x and y, OMR-validity of φ is equivalent to RL OMR -provability of the formula xτ(φ)y. Figure 15.1 presents an RL OMR -proof of this formula.