Mosaic for product

Szabolcs Mikulás^{∗} Department of Computer Science King’s College London

                   szabolcs@dcs.kcl.ac.uk

Abstract

The aim of this paper is to show on a toy example that the mosaic method can serve as an alternative to standard modal logical techniques in the realm of products of modal logics.

Contents

1 Introduction 2 2 Mosaic 2 3 The key lemma 3 4 Completeness 5 5 Complexity 6

∗Supported by EPSRC No. GR/L82441. Thanks are due to everybody who has worked on the mosaic method.

1 Introduction

The aim of this paper is to show that the mosaic method can serve as an alternative to standard modal logical techniques in the realm of products of modal logics.

The results below about the binary product S5^{2} of the modal logic S5 are not new. My hope is that a systematic presentation of an application of the mosaic method to a product of modal logics may convince some innocent souls that using the mosaic technique might be fun. For the more experienced reader:

Isn’t it amazing how smoothly the mosaic method works for S5^{2}?

For the even more experienced reader:

Can we use (a variant of) the mosaic method to prove the decidability of K4^{2} (provided it is decidable)?

First let us recall the definition of S5^{2}. The language consists of the propositional connectives ∧ and ¬ and the modalities ◇ and ◇. A frame is of the form U × V for some sets U and V, called the base sets. A model 𝔐 is a frame U × V together with an evaluation 𝔨 : P → P(U × V) of the propositional variables. Truth is defined in the usual way — the non-propositional cases are:

(u, v) ⊩ ◇φ[𝔨] ⟺ (w, v) ⊩ φ[𝔨] for some (w, v) ∈ U × V
(u, v) ⊩ ◇φ[𝔨] ⟺ (u, w) ⊩ φ[𝔨] for some (u, w) ∈ U × V.

We will use the standard abbreviations, e.g., □ for ¬◇¬.

In the next section, we will define mosaics and saturated sets of mosaics. In section 3, a key lemma is proved, stating that the existence of a model is equivalent to the existence of a saturated set of mosaics. We will use the standard mosaic idea: mosaics serve as basic building blocks, and the saturation conditions guarantee that we can glue mosaics together to form a model. Applying this lemma, we get easy proofs for the completeness and complexity of S5^{2}.

2 Mosaic

We start with the basic definitions.

Definition 2.1 Let W ⊆ U × V for some sets U and V, and let Ξ be a set of formulas that is closed under subformulas. Let (W, λ) be a structure labelled by subsets of Ξ, i.e., λ : W → P(Ξ).

We say that (W, λ) is a coherent labelled structure (a CLS) if the following conditions hold: for every u, v, w and φ, ψ,

1. ¬φ ∈ λ(u, v) ⟺ φ ∉ λ(u, v),

2. φ ∧ ψ ∈ λ(u, v) ⟺ φ, ψ ∈ λ(u, v),

3. φ ∈ λ(u, v) ⇒ ◇φ ∈ λ(w, v),

4. φ ∈ λ(u, v) ⇒ ◇φ ∈ λ(u, w),

5. ◇φ ∈ λ(u, v) ⟺ ◇φ ∈ λ(w, v),

6. ◇φ ∈ λ(u, v) ⟺ ◇φ ∈ λ(u, w), provided that the relevant pairs are in W and the formulas are in Ξ.

By a defect of a labelled structure (W, λ) we mean a pair ((u, v), φ) such that (u, v) ∈ W, φ ∈ λ(u, v) and either

• φ is ◇ψ and ψ ∉ λ(w, v) for every (w, v) ∈ W, or

• φ is ◇ψ and ψ ∉ λ(u, w) for every (u, w) ∈ W.

It turns out that in the case of S5^{2} it is enough to consider rather small CLSs that can serve as basic building blocks.

Definition 2.2 By a mosaic we mean a coherently labelled structure (W, λ) such that |W | = 1.

Usually we will denote mosaics by their labels: if W = {(u, v)}, then we will identify the mosaic (W, λ) by the formula set λ(u, v).

Since CLSs can contain defects, we need conditions that guarantee that defects can be “cured” by gluing mosaics to each other.

Definition 2.3 Let M be a set of mosaics and X be a set of formulas. We say that M is a saturated set of mosaics for X (an X-SSM) if the following hold:

1. there is μ ∈ M such that X ⊆ μ,

2. given a mosaic μ ∈ M and a formula ◇φ ∈ μ, there is a mosaic μ′ ∈ M such that φ ∈ μ′ and ({(0, 0), (1, 0)}, λ) with λ(0, 0) = μ and λ(1, 0) = μ′ is a CLS,

3. given a mosaic μ ∈ M and a formula ◇φ ∈ μ, there is a mosaic μ′ ∈ M such that φ ∈ μ′ and ({(0, 0), (0, 1)}, λ) with λ(0, 0) = μ and λ(0, 1) = μ′ is a CLS,

4. given three mosaics μ, μ′, μ′′ ∈ M, such that the structures ({(0, 0), (1, 0)}, λ) with λ(0, 0) = μ and λ(1, 0) = μ′ and ({(0, 0), (0, 1)}, λ) with λ(0, 0) = μ and λ(0, 1) = μ′′ are CLSs, there is a mosaic ν ∈ M such that ({(0, 0), (1, 0), (0, 1), (1, 1)}, λ) with λ(0, 0) = μ, λ(1, 0) = μ′, λ(0, 1) = μ′′ and λ(1, 1) = ν is a CLS; cf. Figure 1.

If X is a singleton set {ξ}, we will speak of ξ-SSM (instead of {ξ}-SSM).

3 The key lemma

In this section we show that the existence of a model is equivalent to the existence of a saturated set of mosaics.

Lemma 3.1 A formula set X is satisfiable iff there exists an X-SSM.

Proof: First assume that X is satisfiable, say 𝔐 = (U × V, 𝔨) satisfies X at (u, v): (u, v) ⊩ ξ[𝔨] for all ξ ∈ X. Let Ξ be the smallest set of formulas that is closed under subformulas and Ξ ⊇ X. For every (x, y) ∈ U × V, we let

μ(x, y) = {φ ∈ Ξ : (x, y) ⊩ φ[𝔨]}.

μ′′ μ  μ  μ′  ⇒  μ  μ′ μ′′  ν

Figure 1: Saturation condition 4

It is straightforward to check that every μ(x, y) is a CLS, and thus a mosaic. The set

M = {μ(x, y) : (x, y) ∈ U × V }

is a saturated set of mosaics for X: every defect can be “cured”, since each mosaic is part of the same model and we took each μ(x, y) ((x, y) ∈ U×V); given μ, μ′ = μ(u, v) and μ′′ = μ(u′, v′) satisfying the hypothesis of the saturation condition 4, we can find the mosaic ν = μ(u, v′) to meet the requirements of the condition.

For the other direction assume that M is an X-SSM (using some label set Ξ ⊇ X). We have to define a model that satisfies X; by a step-by-step construction we build a labelled structure on ω × ω that does not contain any defect, thus it can be easily turned into a model for X.^{1}

Let us enumerate all the possible defects:

P = {((n, m), φ) : (n, m) ∈ ω × ω, φ a diamond formula}.

0th step: Let μ_{X} ∈ M be such that X ⊆ μ_{X}. We let 𝔚_{0} = (W_{0}, λ_{0}) where W_{0} = {(0, 0)} and λ_{0}(0, 0) = μ_{X}. Clearly 𝔚_{0} is a coherent square. Successor step: Let us assume that, in the nth step, a coherent rectangle 𝔚_{n} = (W_{n}, λ_{n}) has been defined with W_{n} = h_{n} × v_{n} for some natural numbers h_{n} and v_{n}. Further, we assume that 𝔚_{n} is a union of elements of M: for every (x, y) ∈ W, μ(x, y) = λ_{n}(x, y) is an element of M. Let ((k, l), φ) be the first element of P that is an actual defect of the CLS 𝔚_{n}. Wlog we can assume that φ has the form ◇ψ — vertical defects can be treated similarly.

We let W_{n+1} = (h_{n} + 1) × v_{n} and define λ_{n+1} as follows. For (x, y) ∈ W_{n}, we let λ_{n+1}(x, y) = λ_{n}(x, y).

By the induction hypothesis, μ = μ(k, l) ∈ M. Thus, by saturation condition 2, there is a mosaic μ′ ∈ M such that ψ ∈ μ′ and ({(0, 0), (1, 0)}, λ) with

1We denote the set of natural numbers by ω. For any natural number n, we assume that n is the set of natural numbers smaller than n. Thus 0 = ∅ and k + 1 = {0, …, k}.

k ly μ  μ′ μ′′  νh_{n}

Figure 2: Squarifying 𝔚_{n+1}

λ(0, 0) = μ and λ(1, 0) = μ′ is a CLS. We let λ_{n+1}(h_{n}, l) = μ′. It remains to define the labels for the pairs (h_{n}, y) with y ∈ v_{n} ∖ {l}. Fix such a y and consider the pair (k, y). By the induction hypothesis, μ′′ = λ_{n}(k, y) is an element of M. Since 𝔚_{n} is a CLS, and by the choice of μ′, we have that the three mosaics μ, μ′, μ′′ satisfy the hypothesis of the saturation condition 4. Then we can find a mosaic ν ∈ M such that ({(0, 0), (0, 1), (1, 0), (1, 1)}, λ) with λ(0, 0) = μ, λ(1, 0) = μ′, λ(0, 1) = μ′′ and λ(1, 1) = ν is a CLS. We define λ_{n+1}(h_{n}, y) = ν. See Figure 2.

It is easy to check that 𝔚_{n+1} is indeed a coherent rectangle. Further, the possible defect ((k, l), ◇ψ) cannot be an actual defect of any 𝔚_{m} for m > n, since we “cured” this defect in the n + 1st step. Limit step: We let 𝔚 = (W, λ) where W = ⋃_{n∈ω} W_{n} and λ(x, y) = λ_{i}(x, y) with i ∈ ω such that (x, y) ∈ W_{i} (note that λ(x, y) is independent from the choice of i). Clearly 𝔚 is a CLS and it does not contain any defect. We are ready to define the model 𝔐 = (W, 𝔨). For any atom p occurring in Ξ, let 𝔨(p) = {(u, v) ∈ W : p ∈ λ(u, v)}. Now, an easy induction on formulas shows the truth lemma: for every φ ∈ Ξ and (u, v) ∈ W,

φ ∈ λ(u, v) ⟺ (u, v) ⊩ φ[𝔨].

Hence 𝔐 satisfies X: (0, 0) ⊩ ξ[𝔨] for each ξ ∈ X.

4 Completeness

In this section, we fix the labelling set Ξ to be the set of all formulas (in a countable language).

The idea of a mosaic-based completeness proof is to show that the set of maximal consistent sets (MCSs) is a saturated set of mosaics. Then, by Lemma 3.1, for every consistent set of formulas X, we can find a model satisfying X.

It turns out that in the case of S5^{2}, the “obvious” axioms are enough to give a complete inference system. We propose the following axioms:

1. axioms for propositional logic

2. S5-axiomatization for ◇: φ → ◇φ φ → □◇φ ◇◇φ → ◇φ

3. S5-axiomatization for ◇

4. ◇□φ → □◇φ.

We have the usual derivation rules: modus ponens, universal generalization and substitution. Checking soundness of the inference system is left to the reader.

Given MCSs Γ and Φ, we define

ΓHΦ ⟺ {ψ : □ψ ∈ Γ} = {ψ : □ψ ∈ Φ}
ΓV Φ ⟺ {ψ : □ψ ∈ Γ} = {ψ : □ψ ∈ Φ}.

Lemma 4.1 Let X be a consistent set of formulas. Then there exists an X-SSM.

Proof: We show that the set of all MCSs form a saturated set of mosaics. Since X can be extended to a MCS, this gives us an X-SSM.

Obviously every MCS satisfies the coherency conditions. Saturation conditions 2 and 3 follow by standard S5-consideration.

Now assume ΓV Ψ and ΓHΦ. We have to show the existence of a MCS Δ such that ΨHΔ and ΦV Δ. We define

Δ′ = {ψ : □ψ ∈ Ψ} ∪ {φ : □φ ∈ Φ}.

We claim that Δ′ is consistent. Let □ψ_{1}, …, □ψ_{n} ∈ Ψ and □φ_{1}, …, □φ_{m} ∈ Φ. We abbreviate ψ_{1} ∧ … ∧ ψ_{n} as ψ and φ_{1} ∧ … ∧ φ_{m} as φ. Note that we have □ψ ∈ Ψ and □φ ∈ Φ. Then, by ΓHΦ, ◇□φ ∈ Γ. By the Church–Rosser axiom 4, □◇φ ∈ Γ. Recall that □ψ ∈ Ψ and that ΓV Ψ. Hence □ψ ∧ ◇φ ∈ Ψ. Thus ψ ∧ φ must be consistent (by S5). Now, let Δ be a MCS extending Δ′. Clearly Δ meets the requirements.

5 Complexity

In this section, we show how to get decidability and optimal complexity upper bound.

Let ξ be the formula that we want to decide if it is satisfiable. We let Ξ be the set of subformulas of ξ. By Lemma 3.1, it is enough to decide the existence of a ξ-SSM.

Lemma 5.1 Determining the existence of a ξ-SSM is decidable.

Proof: By the usual argument: (i) enumerate the (finite) set of all mosaics labelled using the set of subformulas of ξ, (ii) check if one of the subsets containing a ξ-mosaic satisfies the saturation conditions.

We note that the above decision procedure in fact gives us an optimal upper bound for the complexity of the logic. Indeed, given a formula ξ, there are roughly |ξ| many subformulas. Hence there are at most 2^{|ξ|} mosaics, and a mosaic consists of polynomially many formulas. Thus a potential ξ-SSM can be given as an input of exponential complexity. Checking if every member is in fact a mosaic (i.e., if satisfies the coherency conditions) and whether the saturation conditions are met can be done in polynomial time (in terms of the complexity of the input). Thus we have a non-deterministic exponential time algorithm for deciding if there exists a ξ-SSM — S5^{2} is at most nexptime hard.

We also note that our logic has the finite base property, i.e., every nonvalid formula can be refuted in a model with finite bases. The step-by-step construction given above yields an infinite model. However, using larger mosaics and some combinatorics one can show that all defects can be repaired after finitely many steps.^{2} Another way of proving this fact is to use the connection to first-order logic with two variables and its finite base property.

2See a later version of this paper.