Dual Tableaux for Classical Modal Logics

Abstract

In a narrow sense, modal logic is a logic obtained from the classical logic by endowing it with unary propositional operations intuitively corresponding to ‘it is necessary that’ and ‘it is possible that’. These operations are intensional, i.e., the truth of a formula built with the operation does not depend only on the truth of the subformula to which the operation is applied but also on a relevant state or a situation in which the truth is considered. A development of the semantics of modal logics in terms of a relational structure of states is due to Stig Kanger [Kan57] and Saul Kripke [Kri63]. Algebraic semantics of these standard modal logics is provided by Boolean algebras with normal and additive operations [JT52]. Since the origin of Kripke semantics, intensional logics have been introduced to computer science as an important tool for its formal methods.

1 Introduction

In a narrow sense, modal logic is a logic obtained from the classical logic by endowing it with unary propositional operations intuitively corresponding to ‘it is necessary that’ and ‘it is possible that’. These operations are intensional, i.e., the truth of a formula built with the operation does not depend only on the truth of the subformula to which the operation is applied but also on a relevant state or a situation in which the truth is considered. A development of the semantics of modal logics in terms of a relational structure of states is due to Stig Kanger [Kan57] and Saul Kripke [Kri63]. Algebraic semantics of these standard modal logics is provided by Boolean algebras with normal and additive operations [JT52]. Since the origin of Kripke semantics, intensional logics have been introduced to computer science as an important tool for its formal methods.

In a broad sense modal logic is a field of studies of logics with intensional operations. The operations may have various intuitive interpretations and are relevant in a variety of fields. In logical theories intensional operations enable us to express qualitative degrees of truth, belief, knowledge, obligation, permission, etc. Elements of the relevant relational structures are then interpreted as possible worlds, situations, instants of time, etc. In computer science intensional operations serve as formal tools for expressing dynamic aspects of physical or cognitive processes. In these cases elements of the relational structures are interpreted as the states of a computer program, the tuples of a relational database, the objects of an information system with incomplete information, the agents of multiagents systems, etc.

The basic systems of modal logic in a modern form are due to Clarence Irving Lewis (see [Lew20, LL59, Zem73]). They evolved from his treatment of implication in search for elimination of the paradoxes of the classical implication of Frege–Russell. A development and broad range of research in modal logic and its applications can be traced through an extensive literature of the subject, see e.g., [Fey65, HC68, Seg71, Gal75, Gab76, Boo79, Che80, HC84, vB85, Boo93, Gol93, vB96, CZ97, HKT00, BdRV01, BvBW06].

In this chapter we present a relational formalization of modal logics which originated in [Orł91]. Given a modal logic L, we show how one can construct a relational logic, RL _L, and a dual tableau for RL _L so that it provides a validity checker for the logic L. We show that in fact the RL _L-dual tableau does more: it can be used for proving entailment of an L-formula from a finite set of L-formulas, model checking of L-formulas in finite L-models, and verification of satisfaction of L-formulas in finite L-models. The relational formalization of modal logics presented in this chapter provides a paradigm for all the relational formalisms and dual tableaux considered in PartsIII,IV, andV of the book.

2 Classical Propositional Logic

The vocabulary of the language of the classical propositional logic, PC, consists of the following pairwise disjoint sets:

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

• {, ∨, ∧ } – the set of propositional operations of negation ¬, disjunction ∨, and conjunction ∧.

The set of PC-formulas is the smallest set including $\mathbb{V}$and closed with respect to the propositional operations. We admit the operations of implication, →, and equivalence, ↔, as the standard abbreviations, that is for all PC-formulas ϕ and ψ: $\varphi\rightarrow\Psi\stackrel{\mathrm{df}}{=}\neg\varphi\vee\Psi;$ $\varphi\leftrightarrow\Psi\stackrel{\mathrm{df}}{=}(\neg \varphi \vee \Psi)\wedge(\neg \Psi \vee \varphi)$

Let {0, 1} be a two-element Boolean algebra whose elements represent truth-values ‘false’ and ‘true’, respectively. A PC-model is a structure $\mathcal{M} = (\{0,1\},v)$, where $v: \mathbb{V} \rightarrow \{ 0,1\}$is a valuation of propositional variables in {0, 1}. A PC-formula ϕ is said to be true in a PC-model $\mathcal{M} = (\{0,1\},v)$whenever the following conditions hold:

• $\mathcal{M}\models p$iff v(p) = 1, for every propositional variable p;

• $\mathcal{M}\models \neg \phi$iff $\mathcal{M}\nvDash \phi$;

• $\mathcal{M}\models \phi \vee \psi$iff $\mathcal{M}\models \phi$or $\mathcal{M}\models \psi$;

• $\mathcal{M}\models \phi \wedge \psi$iff $\mathcal{M}\models \phi$and $\mathcal{M}\models \psi$.

A PC-formula ϕ is PC-valid whenever it is true in all PC-models.

3 Propositional Modal Logics

The vocabulary of a modal language consists of the following pairwise disjoint sets:

• $\mathbb{V}$– a countable set of propositional variables and/or constants;

• A set of relational constants;

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

• A set of modal propositional operations is included in the set:

  $$\{[R],\langle R\rangle,[[R]],\langle \!\langle R\rangle \!\rangle : R\mbox{ is a relational constant}\}.$$

The modal operations ⟨R⟩ and ⟨​⟨R⟩​⟩ are definable in terms of [R] and [[R]], respectively, as follows:

$$\langle R\rangle \phi \stackrel{\mathrm{df}}{=}\neg [R]\neg \phi,\quad \langle \!\langle R\rangle \!\rangle \stackrel{\mathrm{df}}{=}\neg [[R]]\neg \phi.$$

The propositional operations [R], ⟨R⟩, [[R]], and ⟨​⟨R⟩​⟩ are referred to as necessity, possibility, sufficiency, and dual sufficiency, respectively.

The set of modal formulas is the smallest set including the set $\mathbb{V}$and closed with respect to the propositional operations.

If the set of relational constants is a singleton set, say {R}, then the modal propositional operations [R], ⟨R⟩, [[R]], and ⟨​⟨R⟩​⟩ are often written as □, ◊, [[ ]], and ⟨​⟨⟩​⟩, respectively. Some modal languages include propositional constants which are interpreted as singletons; they are referred to as nominals. If the cardinality of the set of relational constants is at least 2 or the language includes at least two different and not mutually definable modal operations, then the logic is referred to as multimodal.

Let a modal language be given. A model for the modal language is a structure $\mathcal{M} = (U,m)$such that U is a non-empty set, whose elements are referred to as states, and m is a meaning function such that the following conditions are satisfied:

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

• m(R) ⊆ U ×U, for every relational constant R.

The relations m(R) are referred to as the accessibility relations.

A frame is a structure $\mathcal{F} = (U,m)$such that U is a non-empty set and m is a map which assigns binary relations on U to relational constants. If there are finitely many relational constants in a modal language, then in the frames we often list explicitly all the corresponding relations and usually we denote them with the same symbols as the corresponding constants in the language. A model $\mathcal{M} = (U,m)$is said to be based on a frame $\mathcal{F} = (U,m)$whenever m is the restriction of m′ to the set of relational constants.

A formula ϕ is said to be satisfied in a model $\mathcal{M}$by a state s ∈ U, $\mathcal{M},s\models \phi$, whenever the following conditions are satisfied:

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

• $\mathcal{M},s\models \phi \vee \psi$iff $\mathcal{M},s\models \phi$or $\mathcal{M},s\models \psi$;

• $\mathcal{M},s\models \phi \wedge \psi$iff $\mathcal{M},s\models \phi$and $\mathcal{M},s\models \psi$;

• $\mathcal{M},s\models \neg \phi$iff $\mathcal{M},s\nvDash \phi$;

• $\mathcal{M},s\models [R]\phi$iff for every s′ ∈ U, if (s, s′) ∈ m(R), then $\mathcal{M},s\models \phi$;

• $\mathcal{M},s\models \langle R\rangle \phi$iff there is s′ ∈ U such that (s, s′) ∈ m(R) and $\mathcal{M},s\models \phi$;

• $\mathcal{M},s\models [[R]]\phi$iff for every s′ ∈ U, if $\mathcal{M},s\models \phi$, then (s, s′) ∈ m(R);

• $\mathcal{M},s\models \langle \!\langle R\rangle \!\rangle \phi$iff there is s′ ∈ U such that (s, s′) ∉ m(R) and $\mathcal{M},s\nvDash \phi$.

As usual, given a model $\mathcal{M}$and a state s, ‘$\mathcal{M},s\nvDash \phi$’ is an abbreviation of ‘not $\mathcal{M},s\models \phi$’. Throughout the book, by a modal logic we mean the pair L = (a modal language, a class of models of the language). Given a modal logic L, we write L-language and L-model for the relevant components of L. Formulas of the L-language are referred to as L-formulas.

An L-formula ϕ is said to be true in an L-model $\mathcal{M} = (U,m)$, $\mathcal{M}\models \phi$, whenever for every s ∈ U, $\mathcal{M},s\models \phi$, and it is L-valid whenever it is true in all L-models. An L-formula ϕ is said to be true in the L-frame $\mathcal{F}$, $\mathcal{F}\models \phi$for short, whenever ϕ is true in all the L-models based on $\mathcal{F}$. Note that in every L-model the propositional operations ¬, ∨, and ∧ receive their standard meaning as classical operations of negation, disjunction, and conjunction of PC, respectively.

Standard Modal Logics

The standard modal logics are K, T, B, S4, and S5. Their common language is a modal language with a single relational constant R and with the modal operations [R] and ⟨R⟩.

The models of these logics are of the form $\mathcal{M} = (U,R,m)$where:

• $\mathcal{M}$is a K-model iff R is a binary relation on U;

• $\mathcal{M}$is a T-model iff R is a reflexive relation on U (i.e., 1′ ⊆ R);

• $\mathcal{M}$is a B-model iff it is a T-model such that R is a symmetric relation on U (i.e., R ^{− 1} ⊆ R);

• $\mathcal{M}$is an S4-model iff it is a T-model such that R is a transitive relation on U (i.e., R ; R ⊆ R);

• $\mathcal{M}$is a S5-model iff it is a B-model and S4-model (i.e., R is an equivalence relation on U).

All the standard modal logics are decidable. For details of the proof see e.g., [BvBW06].

4 Relational Formalization of Modal Logics

The logic RL(1, 1′) serves as a basis for the relational formalisms for modal logics whose Kripke-style semantics is determined by frames with binary accessibility relations (see [Orł97bs]). Let L be a modal logic. The relational logic RL _L appropriate for expressing L-formulas is obtained from RL(1, 1′) by endowing its language with relational constants representing the accessibility relations from the models of L-language and with propositional constants of L (if there are any) which will be interpreted appropriately as relations.

The vocabulary of the relational logic RL _L consists of the symbols from the following pairwise disjoint sets:

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

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

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

• ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{L}}} =\{ 1,1\} \cup \{ R : R\mbox{ is a relational constant of $\mathsf{L}$}\}$∪{C _c : c is a propositional constant of L} – a set of relational constants;

• $\{-,\cup,\cap,;{,}^{-1}\}$– the set of relational operations.

Object symbols, relational terms, and RL _L-formulas are defined as in RL(1, 1′)-logic (see Sect. 2.3).

An RL _L -structure is an RL(1, 1′)-model $\mathcal{M} = (U,m)$(see Sect. 2.7) such that:

• m(R) ⊆ U ×U, for every relational constant R of L;

• m(C _c ) ⊆ U ×U, for every propositional constant c of L.

An RL _L -model is an RL(1, 1′)-model $\mathcal{M} = (U,m)$such that:

• m(C _c ) = X ×U, where X ⊆ U, for any propositional constant c of L; it follows that propositional constants of L are represented in RL _L as right ideal relations;

• The domains of relations m(C _c ) satisfy the constraints posed on propositional constants c in L-models; examples of such constants can be found in Sects. 11.3, 15.2, and 16.5;

• For all relational constants representing the accessibility relations of L, all the properties of these relations from L-models are assumed in RL _L -models; many examples of such properties can be found in Sects. 7.5, 11.4, and 16.3.

If in a modal logic L there are finitely many accessibility relations, then in the RL _L-models we list explicitly these relations and we denote them with the same symbols as the corresponding constants in the language.

As established in Sect. 2.7, the models of RL _L with 1′ interpreted as the identity are referred to as standard RL _L -models.

Translation

The translation of modal formulas into relational terms starts with a one-to-one assignment of relational variables to the propositional variables. Let τ′ be such an assignment. Then the translation τ of formulas is defined inductively:

• τ(p) = τ′(p) ; 1, for any propositional variable $p \in \mathbb{V}$;

• τ(c) = C _c ; 1, for any propositional constant $c \in \mathbb{V}$;

• $\tau (\neg \phi ) = -\tau (\phi )$;

• τ(ϕ ∨ ψ) = τ(ϕ) ∪τ(ψ);

• τ(ϕ ∧ ψ) = τ(ϕ) ∩ τ(ψ);

and for every relational constant R of L:

• τ(⟨R⟩ϕ) = R ; τ(ϕ);

• $\tau ([R]\phi ) = -(R\,;\,-\tau (\phi ))$;

• $\tau (\langle \!\langle R\rangle \!\rangle \phi ) = -R\,;\,-\tau (\phi )$;

• $\tau ([[R]]\phi ) = -(-R\,;\,\tau (\phi ))$.

It follows that translation of defined propositional operations → and ↔ is:

• $\tau (\phi \rightarrow \psi ) = -\tau (\phi ) \cup \tau (\psi )$;

• $\tau (\phi \leftrightarrow \psi ) = (-\tau (\phi ) \cup \tau (\psi )) \cap (-\tau (\psi ) \cup \tau (\phi )))$.

Hence, when passing from modal formulas to relational terms we replace propositional variables and constants by relational variables and relational constants, respectively, and propositional operations by relational operations. The crucial point here is that the accessibility relation is ‘taken out’ of the modal operation and it becomes an argument of an appropriate relational operation. In particular, possibility operation is replaced by the relational composition of two relations: the relation representing an accessibility relation and the relation resulting from the translation of the formula which is in the scope of the possibility operation. In this way to any formula ϕ of a modal logic there is associated a relational term τ(ϕ). The above translation assigns to any modal formula a right ideal relation i.e., a relation Q that satisfies Q = Q ; 1. It follows from the following proposition:

Proposition7.4.1.

For every set U, the following conditions are satisfied:

• 1. The family of right ideal relations on U is closed on −, ∪, and ∩;

• 2. For any relation R on U and any right ideal relation P on U, R ; P is a right ideal relation;

• 3. If P is a right ideal relation on U, then for all s,s′∈ U: (s,s′) ∈ P iff for every t ∈ U, (s,t) ∈ P.

Proof.

1. and 3. follow directly from the definition of right ideal relations. For 2., note that since P = P ; 1, $R\,;\,P = R\,;\,(P\,;\,1) = (R\,;\,P)\,;\,1$. □

In some examples of dual tableaux proofs presented in the book a simpler translation of the formula to be proved is sufficient such that τ(p) = τ′(p) for every propositional variable p appearing in the formula.

The translation τ is defined so that it preserves validity of formulas.

Proposition7.4.2.

Let L be a modal logic and let ϕ be an L-formula. Then, for every L-model $\mathcal{M} = (U,m)$there exists an RL _L -model $\mathcal{M} = (U,m)$ with the same universe as that of $\mathcal{M}$ such that for all s,s′∈ U, $\mathcal{M},s\models \phi$ iff (s,s′) ∈ m′(τ(ϕ)).

Proof.

Let ϕ be an L-formula and let $\mathcal{M} = (U,m)$be an L-model. We define an RL _L-model $\mathcal{M} = (U,m)$as follows:

• m′(1) = U ×U;

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

• m′(τ(p)) = m(p) ×U, for every propositional variable p;

• m′(τ(c)) = m(c) ×U, for any propositional constant $c \in \mathbb{V}$;

• m′(R) = m(R);

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

Now, we prove the proposition by induction on the complexity of formulas. Let s, s′ ∈ U.

Let ϕ = p, $p \in \mathbb{V}$. Then $\mathcal{M},s\models p$iff s ∈ m(p) iff (s, s′) ∈ m′(τ(p)), since m′(τ(p)) is a right ideal relation.

Let ϕ = ψ ∨ θ. Then $\mathcal{M},s\models \psi \vee \theta$iff $\mathcal{M},s\models \psi$or $\mathcal{M},s\models \theta$iff, by the induction hypothesis, (s, s′) ∈ m′(τ(ψ)) or (s, s′) ∈ m′(τ(θ)) iff (s, s′) ∈ m′(τ(ψ)) ∪m′(τ(θ)) iff (s, s′) ∈ m′(τ(ψ ∨ θ)).

Let ϕ = ⟨R⟩ψ. By the induction hypothesis, for all t, s′ ∈ U, we have $\mathcal{M},t\ \models \ \psi$iff (t, s′) ∈ m′(τ(ψ)). Therefore, $\mathcal{M},s\models \phi$iff there exists t ∈ U such that (s, t) ∈ m(R) and $\mathcal{M},t\models \psi$iff, by the induction hypothesis, there exists t ∈ U such that (s, t) ∈ m′(R) and (t, s′) ∈ m′(τ(ψ)) iff (s, s′) ∈ m′(R ; τ(ψ)) iff (s, s′) ∈ m′(τ(ϕ)).

Let ϕ = [[R]]ψ. Then $\mathcal{M},s\models \phi$iff for every t ∈ U, if $\mathcal{M},t\models \psi$, then (s, t) ∈ m(R) iff, by the induction hypothesis, for every t ∈ U, if (t, s′) ∈ m′(τ(ψ)), then (s, t) ∈ m′(R) iff (s, s′) ∉ m′( − R ; τ(ψ)) iff (s, s′) ∈ m′(τ(ϕ)).

In the remaining cases the proofs are similar. □

Proposition7.4.3.

Let L be a modal logic and let ϕ be an L-formula. Then, for every standard RL _L-model $\mathcal{M} = (U,m)$there exists an L-model $\mathcal{M} = (U,m)$ with the same universe as that of $\mathcal{M}$ such that for all s,s′∈ U, the condition of Proposition 7.4.2 holds.

Proof.

Let ϕ be an L-formula and let $\mathcal{M} = (U,m)$be a standard RL _L-model. We define an L-model $\mathcal{M} = (U,m)$as follows:

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

• For every propositional constant c, s ∈ m(c) iff there is s′ ∈ U such that (s, s′) ∈ m′(τ(c));

• m(R) = m′(R).

We can prove that $\mathcal{M},s\models \phi$iff (s, s′) ∈ m′(τ(ϕ)) in a similar way as in Proposition 7.4.2. □

Proposition7.4.4.

Let L be a modal logic and let ϕ be an L-formula. Then, for every L-model $\mathcal{M}$there exists an RL _L -model $\mathcal{M}$ such that for all object variables x and y, $\mathcal{M}\models \phi$ iff $\mathcal{M}\models x\tau (\phi )y$ .

Proof.

Let ϕ be an L-formula, let $\mathcal{M} = (U,m)$be an L-model. We construct a standard RL _L-model $\mathcal{M} = (U,m)$as in the proof of Proposition 7.4.2. Let x and y be any object variables. Assume $\mathcal{M}\models \phi$. Suppose there exists a valuation v in $\mathcal{M}$such that $\mathcal{M},v\nvDash x\tau (\phi )y$. Then (v(x), v(y)) ∉ m′(τ(ϕ)). However, by Proposition 7.4.2, models $\mathcal{M}$and $\mathcal{M}$satisfy $\mathcal{M},v(x)\models \phi$iff (v(x), v(y)) ∈ m′(τ(ϕ)). Therefore, $\mathcal{M},v(x)\nvDash \phi$, and hence $\mathcal{M}\nvDash \phi$, a contradiction. Now, assume $\mathcal{M}\models x\tau (\phi )y$. Suppose there is s ∈ U such that $\mathcal{M},s\nvDash \phi$. Let s′ be any element of U. By Proposition 7.4.2, $\mathcal{M},s\models \phi$if and only if (s, s′) ∈ m′(τ(ϕ)). Let v be a valuation in $\mathcal{M}$such that v(x) = s and v(y) = s′. Since $\mathcal{M},s\nvDash \phi$, (v(x), v(y)) ∉ m′(τ(ϕ)), so $\mathcal{M},v\nvDash x\tau (\phi )y$, and hence $\mathcal{M}\nvDash x\tau (\phi )y$, a contradiction. □

Due to Proposition 7.4.3, the following can be proved:

Proposition7.4.5.

Let L be a modal logic and let ϕ be an L-formula. Then, for every standard RL _L-model $\mathcal{M}$there exists an L-model $\mathcal{M}$ such that for all object variables x and y, the condition of Proposition 7.4.4 holds.

From Theorem2.7.2, Propositions 7.4.4, and 7.4.5, we get:

Theorem7.4.1.

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

• 1. ϕ is L-valid;

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

Proof.

(1. → 2. ) Let ϕ be L-valid. Suppose xτ(ϕ)y is not RL _L -valid. Then, there exists a standard RL _L -model $\mathcal{M}$such that $\mathcal{M}\nvDash x\tau (\phi )y$. By Proposition 7.4.5, there is an L-model $\mathcal{M}$such that $\mathcal{M}\nvDash \phi$, which contradicts the assumption of L-validity of ϕ.

(2. → 1. ) Let ϕ be an L-formula such that xτ(ϕ)y is RL _L -valid. Suppose ϕ is not L-valid. Then there exists an L-model $\mathcal{M}$such that $\mathcal{M}\nvDash \phi$. By Proposition 7.4.4, there exists an RL _L -model $\mathcal{M}$such that $\mathcal{M}\nvDash x\tau (\phi )y$, a contradiction. □

Relational dual tableaux for modal logics are extensions of RL(1, 1′)-dual tableau. We add to the RL(1, ′1)-system the specific rules and/or axiomatic sets that reflect properties of the specific relational constants corresponding to accessibility relations and propositional constants (if there are any) of the logic in question. Given a logic L, a relational dual tableau for L, RL _L-dual tableau, enables us to prove facts about the relations from the models of L expressed in the language of L or in the language of RL _L.

Given a modal logic L, an RL _L-set is a finite set of RL _L-formulas such that the first-order disjunction of its members is true in all RL _L-models. Correctness of a rule is defined in a similar way as in the relational logics of classical algebras of binary relations (see Sect. 2.4).

Following the method of proving soundness and completeness of RL-dual tableau described in Sect. 2.6, we can prove soundness and completeness of the RL _L -dual tableau in a similar way. To prove soundness, it suffices to show that all the rules are RL _L -correct and all the axiomatic sets are RL _L -sets (see Proposition 7.5.1). In order to prove completeness we need to prove the closed branch property, the branch model property, and the satisfaction in branch model property. Then the completeness proof is the same as the completeness proof of RL(1, 1′)-dual tableau (see Sects. 2.5 and 2.7). In Table 7.1 we recall the main facts that have to be proved.

Table7.1 The key steps in the completeness proof of relational dual tableaux

5 Dual Tableaux for Standard Modal Logics

Let L be a standard modal logic as presented in Sect. 7.3 (see p. 10). The relational logic appropriate for expressing L-formulas, RL _L , is obtained from logic RL(1, 1′) by expanding its language with a relational constant R representing the accessibility relation from the models of L-language. If a relation R in the models of logic L is assumed to satisfy some conditions, e.g., reflexivity (logic T), symmetry (logicB), transitivity (logic S4) etc., then in the corresponding logic RL _L we add the respective conditions as the axioms of its models. The translation of a modal formula of L into a relational term of RL _L is defined as in Sect. 7.4.

By Theorem 7.4.1 the following holds:

Theorem7.5.1.

For every formula ϕ of a standard modal logic L and for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is L-valid;

• 2. xt(ϕ)y is RL _L -valid.

Dual tableaux for standard modal logics in their relational formalizations are constructed as follows. We add to the RL(1, 1′)-dual tableau the following rules:

• Logic T: (ref R),

• Logic B: (ref R) and (sym R),

• Logic S4: (ref R) and (tran R),

• Logic S5: (ref R), (sym R), and (tran R).

We recall that these rules are of the form (see Sect. 6.6):

For all object symbols x and y,

$$\begin{array}{l@{\quad }l} \mbox{ (ref R)}\, \frac{xRy} {x1y,xRy} \quad &\mbox{ (sym R)}\,\frac{xRy} {yRx} \\ \mbox{ (tran R)}\, \frac{xRy} {xRz,xRy\,\vert \,zRy,xRy}\quad &\mbox{ z is any object symbol } \\ \quad \end{array}$$

As defined in Sect. 7.4, given a standard modal logic L, an RL _L-structure is of the form $\mathcal{M} = (U,R,m)$, where (U, m) is an RL(1, 1′)-model and R is a binary relation on U. An RL _L-model is an RL _L-structure such that relation R satisfies the constraints posed in L-models.

Theorem7.5.2 (Correspondence).

Let L be a standard modal logic and let $\mathcal{K}$be a class of RL _L -structures. Relation R is reflexive (resp. symmetric, transitive) in all structures of $\mathcal{K}$ iff the rule (ref R), (resp. (sym R), (tran R)) is $\mathcal{K}$ -correct.

For the proof see Theorem6.6.1. Theorem 7.5.2 leads to:

Proposition7.5.1.

Let L be a standard modal logic. Then:

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

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

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

We recall that the completion conditions determined by the rules (ref R), (sym R), and (tran R) are:

For all object symbols x and y,

Cpl(ref R) If xRy ∈ b, then x1′y ∈ b;Cpl(sym R) If xRy ∈ b, then yRx ∈ b;Cpl(tran R) If xRy ∈ b, then for every object symbol z, either xRz ∈ b or zRy ∈ b.

The notions of a complete branch of an RL _L-proof tree, a complete RL _L-proof tree, and an open branch of an RL _L-proof tree are defined as in RL-logic (see Sect. 2.5). In order to prove completeness, we need to define a branch model and to show the three theorems of Table 7.1.

The branch model is defined as in the completeness proof of RL(1, 1′)-dual tableau, that is ${R}^{b}\,=\,{m}^{b}(R)\,=\,\{(x,y)\,\in \,{U}^{b}\,\times \,{U}^{b}\,:\,xRy\,\not\in \,b\}$. Using the completion conditions, it is easy to show that R ^b satisfies the conditions assumed in the corresponding L-models (see the proof of Proposition6.6.3). Hence, the branch model property is satisfied. In similar way as in RL(1, 1′)-dual tableau (see also RL _EQ -dual tableau in Sect. 6.6), we can prove the closed branch property and the satisfaction in branch model property:

Proposition7.5.2 (Satisfaction in Branch Model Property).

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

Then, completeness can be proved as for RL(1, 1′)-dual tableau.

Theorem7.5.3 (Soundness and Completeness of Relational Logics for Standard Modal Logics).

Let L be a standard modal logic and let ϕ be an RL _L -formula. Then, the following conditions are equivalent:

• 1. ϕ is RL _L -valid;

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

• 3. ϕ is RL _L -provable.

Finally, by Theorem 7.5.1 and Theorem 7.5.3, we obtain:

Theorem7.5.4 (Relational Soundness and Completeness of Standard Modal Logics).

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

• 1. ϕ is L-valid;

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

Example.

We present a translation and a relational proof of a formula of logic K. Note that RL _K -proof system is exactly the same as RL(1, 1′)-system, because in K-models the accessibility relation is an arbitrary binary relation. Consider the following K-formula:

$$\phi = ([R]p \wedge [R]q) \rightarrow [R](p \wedge q).$$

For reasons of simplicity, let τ(p) = P and τ(q) = Q. The translation τ(ϕ) of the formula ϕ into a relational term of logic RL _K is:

$$-[-(R\,;\,-P) \cap -(R\,;\,-Q)] \cup -(R\,;\,-(P \cap Q)).$$

We show that the formula ϕ is K-valid, by showing that xτ(ϕ)y is RL _K -valid. Figure 7.1 presents its RL _K -proof.

6 Entailment in Modal Logics

The logic RL(1, 1′) can be used to verify entailment of formulas of non-classical logics, provided that they can be translated into binary relations. Let L be a modal logic. In order to verify the entailment we apply the method presented in Sect. 2.11. We translate L-formulas in question into relational terms of the logic RL _L and then we use the method of verification of entailment for RL _L-logic as shown in Sect. 2.11.

Fig.7.1

An RL _K-proof of K-formula ([R]p ∧ [R]q) → [R](p ∧ q)

For example, in every model $\mathcal{M}$of K-logic the truth of the formula p → q in $\mathcal{M}$implies the truth of [R]p → [R]q in $\mathcal{M}$. The translation of these formulas to RL _K-terms is:

$$\tau (p \rightarrow q) = -P \cup Q,$$

$$\tau ([R]p \rightarrow [R]q) = --(R\,;\,-P) \cup -(R\,;\,-Q),$$

where for simplicity τ(p) = P and τ(q) = Q. To verify the entailment we need to show that $-P \cup Q = 1$implies $--(R\,;\,-P) \cup -(R\,;\,-Q) = 1$. According to Proposition2.2.1(7.), we need to show that the formula:

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

is RL _K -provable. Figure 7.2 presents an RL _K -proof of this formula.

Fig.7.2

An RL _K -proof showing that p → q entails [R]p → [R]q

Furthermore, observe that in every model $\mathcal{M}$of K-logic the truth of R ; R ⊆ R in $\mathcal{M}$implies the truth of [R]p → [R][R]p in $\mathcal{M}$. The translation of the latter formula to RL _K-term is:

$$--(R\,;\,-P) \cup -(R\,;\,--(R\,;\,-P)),$$

where for simplicity τ(p) = P. To verify the entailment we need to show that $-(R\,;\,R) \cup R = 1$implies $--(R\,;\,-P) \cup -(R\,;\,--(R\,;\,-P)) = 1$. According to Proposition2.2.1(7.), we need to show that the formula:

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

is RL _K -provable. Figure 7.3 presents its RL _K -proof.

Fig.7.3

An RL _K -proof showing that R ; R ⊆ R entails [R]p → [R][R]p

7 Model Checking in Modal Logics

The method presented in Sect. 3.4 can be used for model checking in finite models of modal logics. The general idea is as follows. Let $\mathcal{M}$be a finite model of a modal logic L and let ϕ be an L-formula. In order to verify whether ϕ is true in $\mathcal{M}$, we construct a relational logic RL _L and an RL _L-model $\mathcal{M}$such that for all object variables x and y, the problem ‘$\mathcal{M}\models \phi$?’ is equivalent to the problem ‘$\mathcal{M}\models x\tau (\phi )y$?’. Then, we apply the method of model checking for the relational logic RL _L, the model $\mathcal{M}$, and the formula xτ(ϕ)y as presented in Sect. 3.4. For that purpose, we consider an instance ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$of the logic RL _L. Then, we obtain:

Theorem7.7.1 (Relational Model Checking in Modal Logics).

For every L-formula ϕ, for every finite L-model $\mathcal{M}$ , and for all object variables x and y, the following statements are equivalent:

• 1. $\mathcal{M}\models \phi$

• 2. xτ(ϕ)y is ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$ -provable.

By way of example, consider modal logic K. Let $\mathcal{M} = (U,R,m)$be a K-model such that U = {a,b,c}, m(p) = {a}, and the accessibility relation is R = { (a,b),(b,c),(a,c)}. Let ϕ be the formula of the form ¬⟨R⟩⟨R⟩p. Let us consider the problem: ‘is ϕ true in $\mathcal{M}$?’. The translation of the formula ϕ is:

$$\tau (\phi ) = -(R\,;\,(R\,;\,(P\,;\,1))),$$

where τ′(p) = P. Using the construction from the proof of Proposition 7.4.2 it is easy to prove that there exists an RL _K -model $\mathcal{M}$such that for all object variables x and y, $\mathcal{M}\models \phi \,\mbox{ iff }\,\mathcal{M}\models x\tau (\phi )y$.

The model $\mathcal{M} = (U,R,m)$is an RL _K-model such that U′ = U, R′ = R, and m′ is the meaning function satisfying:

$$m(P) =\{ (\mathtt{a,a}),(\mathtt{a,b}),(\mathtt{a,c})\}.$$

Let x and y be any object variables. The model checking problem ‘is ϕ true in $\mathcal{M}$?’ is equivalent to the problem ‘is the formula xτ(ϕ)y true in $\mathcal{M}$?’. For the latter we apply the method presented in Sect. 3.4. The vocabulary of the language adequate for testing whether $\mathcal{M}\models x\tau (\phi )y$consists of the following pairwise disjoint sets of symbols:

• ${\mathbb{O}\mathbb{V}}_{{\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}}$- a countable infinite set of object variables;

• ${\mathbb{O}\mathbb{C}}_{{\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}} =\{ {c}_{\mathtt{a}},{c}_{\mathtt{b}},{c}_{\mathtt{c}}\}$– the set of object constants;

• ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}} =\{ R,P,1,1\}$– the set of relational constants;

• $\{-,\cup,\cap,;{,}^{-1}\}$– the set of relational operations.

An ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-model is the structure $\mathcal{N} = (W,R,n)$, where:

• W = {a,b,c};

• n(c _a ) = a, n(c _b ) = b, and n(c _c ) = c;

• n(1) = W ×W;

• n(1′) = { (a,a), (b,b), (c,c)};

• n(P) = { (a,a), (a,b), (a,c)};

• $R = n(R) =\{ (\mathtt{a,b}),(\mathtt{b,c}),(\mathtt{a,c})\}$;

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

The rules of ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-dual tableau which are specific for the model checking problem in question have the following forms:

$$(-R\mathtt{ij})\quad \frac{x-Ry} {x1{c}_{\mathtt{i}},x-Ry\,\vert \,y1{c}_{\mathtt{j}},x-Ry}$$

for every (i,j) ∈ { (a,a), (b,a), (b,b), (c,a), (c,b), (c,c)};

$$(-P\mathtt{ij})\quad \frac{x-Py} {x1{c}_{\mathtt{i}},x-Py\,\vert \,y1{c}_{\mathtt{j}},x-Py}$$

for every (i,j) ∈ { (b,a), (b,b), (b,c), (c,a), (c,b), (c,c)};

$$\begin{array}{rlrlrl} &(1)\quad \frac{} {x-1{c}_{\mathtt{a}}\,\vert \,x-1{c}_{\mathtt{b}}\,\vert \,x-1{c}_{\mathtt{c}}} & & \\ &(\mathtt{i\neq j})\quad \frac{} {{c}_{\mathtt{i}}1{c}_{\mathtt{j}}}\quad \text{ for any}\ \mathtt{i,j} \in \{\mathtt{a,b,c}\},\mathtt{i\neq j} & & \end{array}$$

The ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-axiomatic sets are:

• {c _i Rc _j }, for every (i,j) ∈ { (a,b), (b,c), (a,c)};

• {c _i − Rc _j }, for every(i,j) ∈ { (a,a), (b,a), (b,b), (c,a), (c,b), (c,c)};

• {c _i Pc _j }, for every (i,j) ∈ { (a,a), (a,b), (a,c)};

• {c _i − Pc _j }, for every (i,j) ∈ { (b,a), (b,b), (b,c), (c,a), (c,b), (c,c)}.

Let x and y be object variables. The truth of ϕ in model $\mathcal{M}$is equivalent to ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-provability of xτ(ϕ)y. Figure 7.4 presents an ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-proof of xτ(ϕ)y. The subtree Π ₁ is presented in Fig. 7.5. The subtrees Π ₂ and Π ₃ are presented in Figs. 7.6 and 7.7, respectively. Observe that in a diagram of Fig. 7.7 the applications of the rules ( − P ca), ( − P cb), and ( − P cc) result in the nodes with formulas v1′c _a , v1′c _b , and v1′c _c . Therefore, in the picture we identify all these nodes.

Fig.7.4

An ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-proof of the truth of K-formula ⟨R⟩⟨R⟩p → ⟨R⟩p in the model $\mathcal{M}$

Fig.7.5

The subtree Π ₁

Fig.7.6

The subtree Π ₂

Fig.7.7

The subtree Π ₃

8 Verification of Satisfaction in Modal Logics

The method of verification of satisfaction in finite models presented in Sect. 3.5 can be also used in the case of standard modal logics. Let $\mathcal{M} = (U,R,m)$be a finite model of a modal logic L, let ϕ be an L-formula, and let a ∈ U be a state. In order to verify whether ϕ is satisfied in $\mathcal{M}$by the state a, we construct a relational logic RL _L, an RL _L-model $\mathcal{M} = (U,R,m)$, and a valuation v _a in $\mathcal{M}$such that for all object variables x and y, the problem ‘$\mathcal{M},\mathtt{a}\models \phi$?’ is equivalent to the problem ‘$\mathcal{M},{v}_{\mathtt{a}}\models x\tau (\phi )y$?’. Then, we apply the method of verification of satisfaction as presented in Sect. 3.5 to the relational logic RL _L, the model $\mathcal{M}$, the formula xτ(ϕ)y, and elements v _a (x) and v _a (y) of U′. We construct an instance ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$of the logic RL _L and we obtain:

Theorem7.8.1 (Relational Satisfaction in Standard Modal Logics).

For every L-formula ϕ, for every finite L-model $\mathcal{M} = (U,R,m)$ , and for every state a ∈ U, the following statements are equivalent:

• 1. $\mathcal{M},\mathtt{a}\models \phi$

• 2. ${c}_{{v}_{\mathtt{a}}(x)}\tau (\phi ){v}_{\mathtt{a}}(y)$ is ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$ -provable.

As an example of an application of the method, consider the modal logic K. Let $\mathcal{M} = (U,R,m)$be a K-model such that U = {a,b}, m(p) = {a} and the accessibility relation is R = { (b,a)}. Let ϕ be the formula ⟨R⟩p. Let us consider the problem: ‘is ϕ satisfied in $\mathcal{M}$by state b?’ The translation of the formula ϕ is τ(ϕ) = (R ; (P ; 1)), where τ′(p) = P. By Proposition 7.4.2, there exist a standard RL _K -model $\mathcal{M}$and a valuation v _b in $\mathcal{M}$such that for all object variables x and y, $\mathcal{M},\mathtt{b}\models \phi$iff $\mathcal{M},{v}_{\mathtt{b}}\models x\tau (\phi )y$.

The RL _K -model $\mathcal{M} = (U,R,m)$is such that U′ = U, R′ = R, and m′ is the meaning function satisfying:

$$m(P) =\{ (\mathtt{a,a}),(\mathtt{a,b})\}.$$

Let v _b be a valuation such that v _b (x) = b and v _b (y) = a. Then $\mathcal{M}$and v _b satisfy the condition: $\mathcal{M},\mathtt{b}\models \phi$iff $\mathcal{M},{v}_{\mathtt{b}}\models x\tau (\phi )y$.

Therefore the satisfaction problem ‘is ϕ satisfied in $\mathcal{M}$by state b?’ is equivalent to the problem ‘(b,a) ∈ m′(τ(ϕ))?’. By Proposition3.5.1 this is equivalent to ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-provability of c _b τ(ϕ)c _a .

${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-dual tableau contains the rules and axiomatic sets of RL(1, 1′)-dual tableau adjusted to ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-language and the rules and axiomatic sets specific for the satisfaction problem as presented in Sect. 3.5:

• The rules are: ( − R aa), ( − R ab), ( − R bb), ( − P bb), ( − P ba), (1′), and (a≠b);

• The axiomatic sets are those that include either of the following subsets: {c _b Rc _a }, {c _a Pc _a }, {c _a Pc _b }, {c _a − Rc _a }, {c _b − Rc _b }, {c _a − Rc _b }, {c _b − Pc _b }, and {c _b − Pc _a }.

It is easy to see that the formula xτ(ϕ)y is satisfied in $\mathcal{M}$by valuation v _b , thoughit is not true in $\mathcal{M}$. Therefore, the formula ⟨R⟩p is satisfied in $\mathcal{M}$by state b, while it is not true in $\mathcal{M}$. Figure 7.8 presents an ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-proof of c _b τ(ϕ)c _a , which shows that the formula ⟨R⟩p is satisfied in $\mathcal{M}$by state b.

Fig.7.8

An ${\mathsf{RL}}_{\mathcal{M},x\tau (\phi )y}$-proof showing that ⟨R⟩p is satisfied in $\mathcal{M}$by state b