Similarity on a tableau method between modal propositional logic S5 and classical propositional logic Cl

Yasuhito SUZUKI

                      x-suzuki@cce.numazu-ct.ac.jp

Department of Control and Computer Engineering, Numazu College of Technology

Abstract

A.Chagrov and M.Zakharyashcev show that there exist embeddings between propositional modal logic S5 and classical propositional logic Cl in terms of frame semantics ([CZ97]). So, it is natural to consider that there is also something similar on tableau method between S5 and Cl. Combining a few propositions in [CZ97], we can quite easily find a new tableau method for S5, which resembles for Cl.

1 Notation

Through this report, except treating classical tableau, we will use propositional modal formulas, only. They are introduced in usual way; Let P be the set of propositional variables. Letters p, q, r, …, p_{0}, p_{1}, … will denote propositional variables. The set of propositional modal formulas is constructed from P, ∧, ∨, ⊃, □, ◇ and ⊥ in usual way. Greek letters φ, ψ, χ, … will denote formulas. We consider ⊤ and the negation ¬φ of formula φ as abbreviations of ⊥ ⊃ ⊥ and φ ⊃ ⊥, respectively. We call a formula which outermost connective is □ box formula. In box formulas, we separate formulas which second outermost connective are disjunction, and call such a formula box disjunctive formula.

As for model, we suppose frame semantics. The truth relation and validity are introduced similar to [CZ97], as follows; Let W and R be a denumerable set of possible worlds and equationl relation on W, respectively. A frame F is a pair ⟨W, R⟩, a valuation V is a function from P to 2^{W}, and a model M is a pair ⟨F, V⟩. Suppose x and y are arbitrary possible worlds, and C is a class of frames, then;

(M, x) |̸= ⊥,
(M, x) ⊧ p iff x ∈ V(p),
(M, x) ⊧ φ ∧ ψ iff (M, x) ⊧ φ and (M, x) ⊧ ψ,
(M, x) ⊧ φ ∨ ψ iff (M, x) ⊧ φ or (M, x) ⊧ ψ,
(M, x) ⊧ φ ⊃ ψ iff (M, x) |̸= φ or (M, x) ⊧ ψ,
(M, x) ⊧ □φ iff for all y(xRy ⇒ (M, y) ⊧ φ),
(M, x) ⊧ ◇φ iff for some y(xRy and (M, y) ⊧ φ),
M ⊧ φ iff for all x((M, x) ⊧ φ),
F ⊧ φ iff for all V(M ⊧ φ),
(F, x) ⊧ φ iff for all V((M, x) ⊧ φ),
C ⊧ φ iff for all F(F ∈ C ⇒ F ⊧ φ).

φ is true at x in M if (M, x) ⊧ φ. φ is false at x in M if φ is not true. φ is true in M if M ⊧ φ. φ is valid in F if F ⊧ φ. A set Γ of formulas is characterized by a class C of frames if C ⊧ φ for any φ(∈ Γ), and is denoted by C ⊧ Γ. A generated subframe of a given frame ⟨W, R⟩ is a pair ⟨V, S⟩ such that V and S is a closure of R for some subset of W and a restriction of R by V, respectively. A generated submodel of a given model ⟨F, V⟩ is a pair ⟨G, U⟩ where G is a generated subframe of F and U is a restriction of V by the base set of G.

2 Frame which is constructed from one cluster

In our report, a cluster has a main role. For any possible world x, a cluster C(x) is defined as follows;

C(x) = {y : xRy and yRx}.

Under an equivalence relation R, C(x) means an equivalence class of W/R. A.Chagrov and M.Zakharyascev introduced the following proposition for a frame with a transitive relation.

Proposition 2.1 (3.7 of [CZ97]) Suppose x is a possible worlds in a model M built on a transitive frames and φ an arbitrary fromula. Then for every y ∈ C(x),

(M, x) ⊧ □φ iff (M, y) ⊧ □φ,
(M, x) ⊧ ◇φ iff (M, y) ⊧ ◇φ.

This proposition 2.1 asserts that any box formula has same truth value in each clusters. Next,

Proposition 2.2 (3.11 of [CZ97]) If N is a generated submodel of M then, for every point x in N and every modal formula φ,

(N , x) ⊧ φ iff (M, x) ⊧ φ.

Proposition 2.3 (3.13 of [CZ97]) Let K be the set of theorems of propositional modal logic K. Then,

K = {φ : F ⊧ φ for all rooted frames F}.

The set of theorems of S5 is the set of formulas which are valid in all frames with equivalence relation. As for the case of S5, a rooted frame means that one cluster frames. By proposition 2.2 and 2.3, we can easily show that S5 is characterized by the class of frames which is constructed from one cluster. That is,

Proposition 2.4 Let S5 be the set of theorems of S5. Then,

S5 = {φ : F ⊧ φ for any frame which is constructed from one cluster F}.

By proposition 2.4, it is sufficient to know cardinal of W when expressing frame for S5. Combining propositions 2.1and 2.4, it is natural to dispose box formulas from another types of formulas if we consider tableau proof for S5.

3 Tableau proof of S5

We will introduce a tableau proof method of S5. The essence of this method was introduced first in [Suz97], but the method in [Suz97] is difficult to read because it is intended to implement in a computer system. To simplify it, a similar point between our method and tableau proof of Cl becomes clear.

Basically, tableau method makes a tree structure which is called tableau tree. Beth tableau is a pair (Γ, Δ) of two sets Γ, Δ of formulas. Roughly speaking, Γ of Beth tableau indicates a set of formulas which truth value are true, and Δ indicates a set of formulas which truth value are false. For normal tableau system, each node of a tableau tree is Beth tableau, and each Beth tableau corresponds to a possible world of a frame. In our system, each node of tableau tree corresponds to a model (that is, a set of Beth tableaus).

In this report, S5 tableau is a set of Beth tableau. To dispose box formulas and box disjunctive formulas, we prepare special Beth tableaus in S5 tableau. Each S5 tableau has two special Beth tableaus.

One is called □-tableau (denoted by (Γ_{□} , Δ_{□} )), and another □-∨-tableau (denoted by (Γ_{□∨} , Δ_{□∨} )), respectively. Thus, S5 tableau itself is denoted by [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. S5 tabelau tree is a tree structure which is constructed from S5 tableaus.

In our tableau method, two types of tableau extension rules are introduced. Each rule is applied to a formula of Beth tableau on leaf S5 tableaus. Formula which is applied rule is marked with check mark. Checked formulas do not become target of applying rules. Checked formula (\overline{φ}) and non-checked formula (φ) are treated the identical element (checked-formula) in any set if both \overline{φ} and φ are elements of the set. Tableau extension rule is applied to non-checked formulas of all Beth tableaus except □-∨-tableau, and tableau box disjunctive extension rule is applied to non-checked formulas of □-∨-tableau.

Tableau extension rule is defined as follows;

• ⊥ ∈ Γ(Γ_{□} ): Stop applying extension rule to this S5 tableau.

• ¬φ ∈ Γ(Γ_{□} ): Check ¬φ, and add φ into Δ (Δ_{□} ).

• φ ∧ ψ ∈ Γ(Γ_{□} ): Check φ ∧ ψ, and add φ, ψ into Γ (Γ_{□} ).

• φ ∨ ψ ∈ Γ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ∨ ψ in Γ in each child, and add φ into Γ of one child and ψ into Γ of another child.

• φ ⊃ ψ ∈ Γ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ⊃ ψ from Γ in each child, and add φ into Δ of one child and ψ into Γ of another child.

• φ ∨ ψ ∈ Γ_{□} : Check φ ∨ ψ in Γ_{□} , and add φ ∨ ψ to Γ_{□∨} .

• φ ⊃ ψ ∈ Γ_{□} : Check φ ⊃ ψ in Γ_{□} , and add ¬φ ∨ ψ to Γ_{□∨} .

• □φ ∈ Γ(Γ_{□} ): Check □φ, and add φ into Γ_{□} (Γ_{□} ).

• ◇φ ∈ Γ(Γ_{□} ): Suppose {φ_{1}, …, φ_{h}} and {φ_{h+1}, …, φ_{k}} are the set of checked formulas of Γ_{□∨} and the set of checked formulas of Δ_{□∨} , respectively. For each i, φ_{i} is denoted by α_{i}^{0} ∨α_{i}^{1} when 1 ≤ i ≤ h and by α_{i}^{0} ∧ α_{i}^{1} when h + 1 ≤ i ≤ k. Make 2^{k} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{k}}, and add them as children of this S5 tableau. For each S5 tableau children T_{s}, add a Beth tableau ({φ, α_{1}^{j_{1}}, …, α_{h}^{j_{h}}}, {α_{h+1}^{j_{h+1}}, …, α_{k}^{j_{k}}}) such that s = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{k}2^{k−1}. Check ◇φ of all Γ-nodes of Beth tableaus including □-tableau at last.

• ⊥ ∈ Δ(Δ_{□} ): Check ⊥.

• φ ∧ ψ ∈ Δ: Make two copies of S5 tableau, and add them as children of this node. Then, check φ ∧ ψ from Δ in each child, and add φ into Δ of one child and ψ into Δ of another child.

• φ ∧ ψ ∈ Δ_{□} : Check φ ∧ ψ, and add φ ∧ ψ to Δ_{□∨} .

• φ ∨ ψ ∈ Δ(Δ_{□} ): Check φ ∨ ψ, and add φ, ψ into Δ (Δ_{□} ).

• φ ⊃ ψ ∈ Δ(Δ_{□} ): Check φ ⊃ ψ, and add φ into Γ (Γ_{□} ) and ψ into Δ (Δ_{□} ).

• □φ ∈ Δ(Δ_{□} ): Suppose {φ_{1}, …, φ_{h}} and {φ_{h+1}, …, φ_{k}} are the set of checked formulas of Γ_{□∨} and the set of checked formulas of Δ_{□∨} , respectively. For each i, φ_{i} is denoted by α_{i}^{0} ∨ α_{i}^{1} when 1 ≤ i ≤ h and by α_{i}^{0} ∧α_{i}^{1} when h+1 ≤ i ≤ k. Make 2^{k} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{k}}, and add them as children of this S5 tableau. For each S5 tableau children T_{s}, add a Beth tableau ({α_{1}^{j_{1}}, …, α_{h}^{j_{h}}}, {φ, α_{h+1}^{j_{h+1}}, …, α_{k}^{j_{k}}}) such that s = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{k}2^{k−1}. Check □φ of all Δ-nodes of Beth tableaus including □-tableau at last.

• ◇φ ∈ Δ(Δ_{□} ): Check ◇φ, and add φ into Δ_{□} (Δ_{□} ).

Tableau box disjunctive extension rule is defined as follows;

• φ ∨ ψ ∈ Γ_{□∨} : Check φ ∨ ψ. Denote φ and ψ by α^{0} and α^{1}, respectively. Suppose n is the number of Beth Tableaus of S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. Make 2^{n} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{n}}, and add them as children of this S5 tableau. For each Beth tableau (Γ_{i}, Δ_{i}) of T_{j}, add α^{j_{i}} to Γ_{i} such that j = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{n}2^{n−1}.

• φ ∧ ψ ∈ Δ_{□∨} : Check φ ∧ ψ. Denote φ and ψ by α^{0} and α^{1}, respectively. Suppose n is the number of Beth Tableaus of S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})]. Make 2^{n} copies of S5 tableau and indexes each copies like T_{1}, …, T_{2^{n}}, and add them as children of this S5 tableau. For each Beth tableau (Γ_{i}, Δ_{i}) of T_{j}, add α^{j_{i}} to Δ_{i} such that j = j_{1}2^{0} + j_{2}2^{1} + ⋯ + j_{n}2^{n−1}.

We will show two examples of applying to S5 tableau.

Example 3.1 Let S5 tableau [(∅, ∅) : (∅, ∅) : (∅, {◇p ⊃ □◇p})] be given. Then,

[(∅, ∅) : (∅, ∅) : (∅, \{◇p ⊃ □◇p\})] ⇒ [(∅, ∅) : (∅, ∅) : (\{◇p\}, \{□◇p, \overline{◇p ⊃ □◇p}\})]
⇒ [(∅, ∅) : (∅, ∅) : (\{\overline{◇p}\}, \{□◇p, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅)]
⇒ [(∅, ∅) : (∅, ∅) : (\{\overline{◇p}\}, \{\overline{□◇p}, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅), (∅, \{◇p\})]
⇒ [(∅, \{p\}) : (∅, ∅) : (\{\overline{◇p}\}, \{\overline{□◇p}, \overline{◇p ⊃ □◇p}\}), (\{p\}, ∅), (∅, \{\overline{◇p}\})]

Example 3.2 Let S5 tableau [(∅, ∅) : (∅, ∅) : ({□(p ∨ ◇q)}, ∅)] be given. Then,

[(∅, ∅) : (∅, ∅) : (\{□(p ∨ ◇q)\}, ∅)] ⇒ [(\{p ∨ ◇q\}, ∅) : (∅, ∅) : (\{\overline{□(p ∨ ◇q)}\}, ∅)]
⇒ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{p ∨ ◇q\}, ∅) : (\{\overline{□(p ∨ ◇q)}\}, ∅)]
⇒ \{ \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{p, \overline{□(p ∨ ◇q)}\}, ∅)] \\ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{◇q, \overline{□(p ∨ ◇q)}\}, ∅)] \end{matrix}

⇒ \{ ; \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{p, \overline{□(p ∨ ◇q)}\}, ∅)] \\ \{ & \begin{matrix}[(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{◇q}, \overline{□(p ∨ ◇q)}\}, ∅), (\{p, q\}, ∅)] \\ [(\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{p ∨ ◇q}\}, ∅) : (\{\overline{◇q}, \overline{□(p ∨ ◇q)}\}, ∅), (\{\overline{◇q}, q\}, ∅)] \end{matrix} \end{matrix}

It is natural condsidered from the above examples, closeness on S5 tableau is defined as follows.

Definition 3.3 S5 tableau [(Γ_{□} , Δ_{□} ) : (Γ_{□∨} , Δ_{□∨} ) : (Γ_{1}, Δ_{1}), …, (Γ_{n}, Δ_{n})] is closed if (Γ_{□} ∪ Γ_{i}) ∩ (Δ_{□} ∪ Δ_{i}) ≠ ∅ holds for some i.

Closeness of S5 tabelau tree and ⊢ are defined in usual way. Then, the following completeness result holds.

Proposition 3.4 For any formula φ, ⊢ φ holds, if and only if, ⊧ φ.

4 Conclusion

Modal logic S5 is characterized by the class of one cluster frames. Meanwhile propositional classical logic Cl is characterized by the singleton of the one point frame. Combining with proposition 2.1 and 2.4, we could devide modal formulas into three layers in our tableau method. We tried to simplify extension rules. If box disjunctive formula in Γ (and its dual in Δ) does not appear in our tableau tree, our method quite resembles to Cl tableau. Box disjunctive formulas are the reason why increasing nodes of S5 tableau. We conjecture that box disjunctive formula becomes the cause of deviding S5 from Cl.

References

[CZ97] Alexander Chagrov and Michael Zakharyaschev. Modal Logic. Oxford, 1997.

[Suz97] Yasuhito Suzuki. The realization of the hybrid multi-modal logic theorem prover in the term rewriting system cafeobj. Sequent calculs � Kripke semantics �������������, �� �������� 1021, pp. 96–111, 1997.