On complementary modalities

Yuko Murakami^{∗}

                     ymurakam@cogsci.l.chiba-u.ac.jp

JSPS fellow (Faculty of Letters, Chiba University)

1 Problem

The language here is a propositional bimodal language with □ and [e]. A complementary frame is ⟨W, R, R̄⟩ where R is a binary relation on W and R̄, the complement of R, serves as the accessibility relation to interpret [e].

Humberstone[1] gives an axiomatic system of the logic of valid sentences in the class of all complementary frames with a schema:

1. K for □ and [e]

2. Let S be a sequence of □ and [e], and W be the sequence of modalities where each ⋆ in S is

substituted by its dual. Then,

W(□p ∧ [e]q) → S(p ∨ q)  (1)

Problem 1. When R is an equivalence relation, is there any axiomatization of the logic without the axiom schema 1? Is the logic decidable? This short paper answers yes to both.

2 An axiomatic system

A system S(□, [e]) consists of:

1. Tautologies of classical propositional logic

2. S5 for □

3. B for [e]

4. [e]p → [e]□p ∧ □[e]p

5. ◇[e]p → [e]p

6. [e]p ∧ □p → [e]^{2}p Observation 2. [e]p ∧ □q → [e](◇¬p → q) ∧ □(◇¬p → q) is provable in S(□, [e]).

∗This research is supported by the JSPS Research fellowships for young scientists. Prof. Larry Moss and Dr. Ming Xu offer helpful suggestions. The author is responsible for any mistakes.

3 Completeness and decidability

Here completeness and decidability is to be shown by constructing a finite complementary model via filtration. A “copy-and-paste” of equivalence classes may be required during the construction.

Given a consistent formula A, construct a filtration set as follows:

X_{0}(A) = Sub(A) ∪ {[e]⊥}
X_{1}(A) = X_{0}(A) ∪ {[e]B, □¬□B : □B ∈ X_{0}(A)}
∪{□B, [e]□B, [e]^{2}B, [e]¬[e]B, [e]¬[e]^{2}B, □¬[e]B : [e]B ∈ X_{0}(A)}
X(A) = Sub(X_{1}(A) ∪ {¬B : B ∈ X_{1}(A)})

Obviously, X(A) is finite. Fix an arbitrary maximal consistent set Γ_{A} such that A ∈ Γ_{A}.

Let W be the class of maximal consistent sets. Define an equivalence relation ∼ as: Γ ∼ Γ′ iff Γ ∩ Γ_{A} = Γ′ ∩ Γ_{A}. Let [W] be the quotient set by ∼, and [Γ] be the equivalence class to which Γ belongs. Define binary relations on [W]:

R_{0}^{□}[Γ][Γ′] iff {A : □A ∈ Γ} ∩ X_{A} ⊆ Γ′
R_{0}^{[e]}[Γ][Γ′] iff {A : [e]A ∈ Γ} ∩ X_{A} ⊆ Γ′.

Let W_{0} = {[Γ] ∈ [W] : (R_{0}^{□} ∪ R_{0}^{[e]})^{∗}[Γ_{A}][Γ]}.

Lemma 3. For each x, y ∈ W_{0}, either R_{0}^{□}xy or R_{0}^{[e]}xy.

Proof. It suffices to show by induction that (R_{0}^{□} ∪ R_{0}^{[e]})[Γ_{A}][Γ] for every [Γ] ∈ W_{0}. The base is clear. Suppose (R_{0}^{□} ∪ R_{0}^{[e]})^{(}n + 1)[Γ_{A}][Γ]. By induction hypothesis, (R_{0}^{□} ∪ R_{0}^{[e]})^{2}[Γ_{A}][Γ]. Case 1: When (R_{0}^{□})^{2}[Γ_{A}][Γ], a standard routine shows R_{0}^{□}[Γ_{A}][Γ]. Case 2: The axiom [e]p → [e]□p ∧ □[e]p takes care of these two cases: (R_{0}^{□} ∘ R_{0}^{[e]})[Γ_{A}][Γ] and (R_{0}^{[e]} ∘ R_{0}^{□})[Γ_{A}][Γ]. Case 3: Suppose (R_{0}^{[e]})^{2}[Γ_{A}][Γ]. Consider Y = {[e]B ∈ X(A) : [e]B ∈ Γ_{A}}. Suppose there is any [e]C ∈ Y, C ∉ Γ. Then, [e]^{2}C ∉ Γ_{A} and ¬□C ∈ Γ must hold. Consider arbitrary □D ∈ Γ_{A} ∩ X(A). Since [e]C ∧ □D ∈ Γ_{A}, ¬□C → D ∈ Γ, which implies D ∈ Γ. Therefore, R_{0}^{□}[Γ_{A}][Γ].

W_{0} is finite. Enumerate the members of W_{0}, and for the i-th member Δ_{i} = [Γ_{i}], let x_{i} = {B ∈ X(A) : B ∈ Γ}. Let W_{1} be the set of x_{i}’s. Where x_{j} = {B ∈ X(A) : B ∈ Γ_{j}} (j = 1, 2), define: R_{1}^{⋆}x_{1}x_{2} iff R_{0}^{⋆}[Γ_{1}][Γ_{2}] (⋆ = □, [e]).

The case which requires extra caution is when there is any x ∈ W_{1} with R_{1}^{[e]}xx.

If there is no such x, the construction ends. Define v_{c} : P rop → ℘(W_{1}) to be v_{c}(p) = {x : p ∈ x}. Take M_{c} = ⟨W_{1}, R_{1}^{□}, R_{1}^{[e]}, v_{c}⟩ as a filteration model.

Otherwise, such R_{1}^{[e]}-reflexive points are to split. Let Z ⊆ W_{1} be the set of R_{1}^{[e]}-reflexive points. W_{c} = (W_{1} \ Z) ∪ (Z ⊎ Z). For each z ∈ Z, let (z, 0), (z, 1) denote the results of splitting.

R_{c}^{□}xy iff R_{1}^{□}xy  if x, y ∈ (W_{1} \ Z)
or x = (x, i), y = (y, j) and i = j
R_{c}^{[e]}xy iff not R_{c}^{□}xy

(2)

Identify (z, 0), (z, 1) with z. Let v_{c} : P rop → ℘(W_{c}) be v_{c}(p) = {x ∈ W_{c} : p ∈ x}. Let M_{c} = ⟨W_{c}, R_{c}^{□}, R_{c}^{[e]}, v_{c}⟩.

In each case, M_{c} is made to be a complementary model. The finite construction leads via a standard induction to:

Lemma 4. (Truth lemma) For each formula B ∈ Sub(A), M^{c}, x ⊧ B iff B ∈ x.

Corollary 5. S(□, [e]) is complete.

Corollary 6. S(□, [e]) is decidable.

References

[1] I. L. Humberstone(1983) Inaccessible Worlds. Notre Dame Journal of Formal Logic, 24, 346–352.