An efficient construction of counter–models for modal logic K4

Motohiko Mouri

                            mouri@jaist.ac.jp

JAIST, Tatsunokuti, Ishikawa, 923–1292, Japan

                      http://www.jaist.ac.jp/~mouri

1 Introduction

In this paper, we will give an efficient construction of counter–models for modal logic K4. Our method is based on the decision procedure with efficient loop-checking in [1]. A major difficulty for K4 lies in the fact that though we can always find a finite counter–model with a tree-form for intuitionistic logic[3], a finite counter–model for K4 will contain some clusters in it. Therefore, constructing a finite counter– model from a refutation tree will need a new idea. This is done in Section 3 by introducing two kinds of blocks.

2 Decision procedure for K4

Our decision procedure for K4 is obtained by modifying the procedure given in [1]. The algorithm is in fact the same, but we choose to implement it as a sequent calculus rather than a tableau system.

The resulting decision procedure is presented below (Figure 1). Two differences with standard sequent systems are that our sequents consist of multisets rather than lists and that we add certain sets of formulas (called ‘histories’) to sequents, which show when rules for modality are applicable.

□Γ, p_{1}, ⋯, p_{n} → q_{1}, ⋯, q_{m}, □Δ ⟨□Γ|□Σ⟩ (init)_{s}(□Δ ⊂ □Σ)

□Γ, p_{1}, ⋯, p_{n} → q_{1}, ⋯, q_{m} ⟨□Π|□Σ⟩ (init)_{t}

Γ, A, B → Δ ⟨□Π|□Σ⟩ Γ, A ∧ B → Δ ⟨□Π|□Σ⟩ (∧L) Γ → Δ, A ⟨□Π|□Σ⟩ Γ → Δ, B ⟨□Π|□Σ⟩ Γ → Δ, A ∧ B ⟨□Π|□Σ⟩ (∧R)

Γ → A, Δ ⟨□Π|□Σ⟩ Γ¬A → Δ ⟨□Π|□Σ⟩ (¬L)  Γ, A → Δ ⟨□Π|□Σ⟩ Γ → Δ, ¬A ⟨□Π|□Σ⟩ (¬R)
□Γ, Γ → A_{1} ⟨□Γ|□Σ, □Θ⟩ ⋯ □Γ, Γ → A_{m} ⟨□Γ|□Σ, □Θ⟩

□Γ, p_{1}, ⋯, p_{n} → □A_{1}, ⋯, □A_{m}, □Δ, q_{1}, ⋯ q_{l} ⟨□Γ|□Σ⟩ (□)_{s}

(□Θ ≡ □A_{1}, ⋯ □A_{n}, □Θ ∩ □Σ = ∅, □Δ ⊂ □Σ)

□Γ, Γ → A_{1} ⟨□Γ|□Θ⟩ ⋯ □Γ, Γ → A_{m} ⟨□Γ|□Θ⟩

□Γ, p_{1}, ⋯, p_{n} → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} ⟨□Π|□Σ⟩ (□)_{t}

(□Θ ≡ □A_{1}, ⋯, □A_{n}, □Γ ⊋ □Θ)

Figure 1: Decision procedure for K4

We write A ∨ B and A ⊃ B to denote shorted forms of ¬(¬A ∧ ¬B) and ¬(A ∧ ¬B), respectively. Note that (□)_{s} and (□)_{t} rules should be understood as ‘or’–branch, but not as ‘and’–branch. Therfore,

if one of the upper sequents is provable, then the lower sequent is provable. In order to distinguish it from other usual rules, we use a double line (=), instead of a single line.

The original system from [1] is obtained by removing (□)_{t} and (init)_{t} rules. Though our decision procedure are essentially the same as the one in [1], we need these rules when we construct counter– models. We have the following.

Theorem 2.1 The system in Figure 1 gives a decision procedure for modal logic K4.

Proof: See [1].

Finally, we come to ‘history’. Take for example the (init)_{t} rule.

□Γ, p_{1}, ⋯, p_{n} → q_{1}, ⋯, q_{m} ⟨□Π|□Σ⟩ (init)_{t}

The pair ⟨□Π|□Σ⟩ is called a history. The pairs occurrencing in other rules are similar. The first element of the pair (□Π in (init)_{t} rule) is called valid history, because the boxed formulae are valid at the corresponding world in counter–model. The second element of the pair (□Σ in (init)_{t} rule) is called invalid history. because the boxed formulae are invalid at the corresponding world. Histories provide efficient loop–check in syntax, and give looplessness in semantics.

3 Counter-model construction

In this section, we will show how to construct counter–models.

To construct a Kripke–model, we consider refutation tree which is obtained from the decision procedure for an unprovable sequent. We will define a Kripke–model from the reftation tree.

Definition 3.1 (block) We call a block a part of refutation tree beginning with initial sequent, (□)_{s} or (□)_{t} rule and ending to (□)_{s} or (□)_{t} rule. A block is a subtree of refutation tree contained between double line(=) and another double line. Symmetric block is a block which begins with (□)_{s} or (init)_{s}rule. Transitive block is a block which begins with (□)_{t} or (init)_{t} rule. Initial block is a block which begins with an initial sequent. Symmetric initial block is a block which begins with (init)_{s} initial sequent. transitive initial block is a block which begins with (init)_{t} initial sequent.

Definition 3.2 (counter model) We construct a corresponding Kripke–model and a world for a refutation tree as follows. Case 1. symmetric initial block beginning with □Γ, p_{1}, ⋯, p_{n} → q_{1}, ⋯, q_{m}, □Δ⟨□Γ|□Σ⟩: It corresponds to (M, w) such that M = (W, R, ⊧), W = {w}, R = (w, w), w ⊧ p_{1} ∧ ⋯ ∧ p_{n}.

Case 2. transitive initial block: Identical to symmetric case.

Case 3. symmetric block

⋯ □Γ, Γ → S_{i} ⟨□Γ|□Σ, □Θ⟩ ⋯ □Γ, Γ → T_{j} ⟨□Γ|□Σ, □Θ⟩ ⋯ □Γ, p_{1}, ⋯, p_{n} → □S_{1}, ⋯, □S_{m}, □T_{1}, ⋯, □T_{l}, □Δ, q_{1}, ⋯ q_{k} ⟨□Γ|□Σ⟩ (□)_{s} (1 ≤ i ≤ m, 1 ≤ j ≤ l):

Let □Γ, Γ → S_{1}⟨□Γ|□Σ, □Θ⟩, ⋯, □Γ, Γ → S_{m}⟨□Γ|□Σ, □Θ⟩ be end–sequents of symmetric blocks and each of them correspond to (M_{S_{i}}, w_{S_{i}}), where M_{S_{i}} = (W_{S_{i}}, R_{S_{i}}, ⊧). Let □Γ, Γ → T_{1}⟨□Γ|□Σ, □Θ⟩, ⋯, □Γ, Γ → T_{l}⟨□Γ|□Σ, □Θ⟩ be the end sequents of transitive blocks and each of them correspond to (M_{T_{i}}w_{T_{i}}), where M_{T_{i}} = (W_{T_{i}}, R_{T_{i}}, ⊧).

The symmetric block above corresponds to (M, w), where M = (W, R ⊧, w) such that W = {w}∪W_{S_{1}} ∪ ⋯∪W_{S_{m}}∪W_{T_{1}}∪⋯∪W_{T_{l}}, R′ = {(w, w_{S_{1}}), ⋯, (w, w_{S_{m}}), (w, w_{T_{1}}), ⋯, (w, w_{T_{l}})}∪{(w_{S_{1}}, w), ⋯, (w_{S_{m}}, w)}∪ R_{S_{1}} ∪ ⋯ ∪ R_{S_{m}} ∪ R_{T_{1}} ∪ ⋯ ∪ R_{T_{l}}, R = transitive closer of R′, w ⊧ p_{1} ∧ ⋯ ∧ p_{n}.

\begin{aligned}Syn ; ⋮ . & ⋯ & Syn ; ⋮ . & ⋯ & T ra ; ⋮ . & ⋯ & T ra ; ⋮ . \\ & & & & & & (□)_{s} \end{aligned} ; ⋮ .⟺ [figure: • ⋯ •  • ⋯ •; •]

Case 4. transitive block

⋯ □Γ, Γ → S_{i} ⟨□Π|□Θ⟩ ⋯ □Γ, Γ → T_{j} ⟨□Π|□Θ⟩ ⋯ □Γ, p_{1}, ⋯, p_{n} → □S_{1}, ⋯, □S_{m}, □T_{1}, ⋯, □T_{l}, □Δ, q_{1}, ⋯ q_{k} ⟨□Γ|□Σ⟩ (□)_{t} (1 ≤ i ≤ m, 1 ≤ j ≤ l):

Let □Γ, Γ → S_{1}⟨□Π|□Θ⟩, ⋯, □Γ, Γ → S_{m}⟨□Π|□Θ⟩ be end–sequents of symmetric blocks and each of them correspond to (M_{S_{i}}, w_{S_{i}}), where M_{S_{i}} = (W_{S_{i}}, R_{S_{i}}, ⊧). Let □ → T_{1}⟨□Π|□Θ⟩, ⋯, □ → T_{l}⟨□Π|□Θ⟩ be the end sequents of transitive blocks and each of them correspond to (M_{T_{i}}w_{T_{i}}), where M_{T_{i}} = (W_{T_{i}}, R_{T_{i}}, ⊧).

The symmetric block above corresponds to (M, w), where M = (W, R ⊧, w) such that W = {w}∪W_{S_{1}} ∪ ⋯∪W_{S_{m}}∪W_{T_{1}}∪⋯∪W_{T_{l}}, R′ = {(w, w_{S_{1}}), ⋯, (w, w_{S_{m}}), (w, w_{T_{1}}), ⋯, (w, w_{T_{l}})}∪{(w_{S_{1}}, w_{S_{2}}), ⋯, (w_{S_{1}}, w_{S_{m}}), ⋯, (w_{S_{m}}, w_{S_{1}}), ⋯, (w_{S_{m}}, w_{S_{(m−1)}})} ∪ R_{S_{1}} ∪ ⋯ ∪ R_{S_{m}} ∪ R_{T_{1}} ∪ ⋯ ∪ R_{T_{l}}, R = transitive closer of R′, w ⊧ p_{1} ∧ ⋯ ∧ p_{n}.

\begin{aligned}Syn ; ⋮ . & ⋯ & Syn ; ⋮ . & ⋯ & T ra ; ⋮ . & ⋯ & T ra ; ⋮ . \\ & & & & & & (□)_{t} \end{aligned} ; ⋮ .⟺ [figure: •; •; •; ⋯; •; •]

Theorem 3.3 Models constructed by our method are indeed counter–models.

Proof: Similar to the proof for S4 in [2].

4 Conclusion

In this paper, we give an effective way of constructing counter–models for modal logic K4 from a decision procedure. By our method, each counter–model is represented as a tree of semi–clusters, where semi– cluster is the structure consisted of a possible world and a cluster. In each semi–cluster, a set of boxed formulae is valid. The higher in the tree structure a semi–cluster is, the more valid boxed formulae it has, as the example in Figure 2 shows.

PSfrag replacements

⊧ Γ, A, C

⊧ Γ, A, D
⊧ Γ, A
⊧ Γ, B
⊧ Γ

Figure 2: Structure of K4 couner–model

References

[1] Alain Heuerding, Michael Seyfried and Heinrich Zimmermann: Efficient loop-check for backward proof search in some non-classical propositional logics, In P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi, editors, Tableaux 96, LNCS 1071, 210-225, 1996.

[2] Motohiko Mouri An efficient contraction of counter–models for modal logic S4, Bulletin of the Section of Logic, vol 30 No.2, 2001, 79–86.

[3] L. Pinto and R. Dyckhoff, Loop–free construction of counter–models for intuitionistic propositional logic, Symposia Gaussiana, Conf. A (Behara, Fritsch, and Lintz, editors), Walter de Gruyter & Co., Berlin, 1995, 225–232.