Products of Modal Logics by General Frames

Yasusi Hasimoto

                          yasusi-h@jaist.ac.jp

Graduate School of Information Science, Japan Advanced Institute of Science and Technology

1 Products of Modal Logics by Kripke Frames

Let F = (W, R) and G = (V, S) be Kripke frames. As Shehtman introduced in [3], we define the products of Kripke frames as F ×_{s} G := (W × V, R^{∨}, S^{∨}), where R^{∨} = {((x, y), (z, y)) | xRz}, S^{∨} = {((x, y), (x, z)) | ySz}. Moreover we will define as follows.

For any modal logic L, F (L) := {F | F ⊧ L}.

For any class C of Kripke frames, L(C) := {φ | F ⊧ φ for any F ∈ C}.

For any classes C_{1}, C_{2} of Kripke frames, C_{1} ×_{s} C_{2} := {F ×_{s} G | F ∈ C_{1}, G ∈ C_{2}}.

For modal logics L_{1}, L_{2}, we define the products of logics as L_{1} ×_{s} L_{2} := L(F (L_{1}) ×_{s} F (L_{2})).

The properties of L_{1} ×_{s} L_{2} is, for example, investigated as follows (see [1]).

• The logic L_{1} ×_{s} L_{2} is Kripke complete. (Trivial.)

• L_{1} ×_{s} L_{2} ⊇ [L_{1}, L_{2}], where [L_{1}, L_{2}] := L_{1} ∗ L_{2} ⊕ □_{1}□_{2}p ↔ □_{2}□_{1}p ⊕ ◇_{1}□_{2}p → □_{2}◇_{1}p.

• If L_{1}, L_{2} are PTC-logics (i.e. the logics axiomatized by a set of pseudotransitive formulas ◇^{m}□p → □^{n}p and/or closed formulas), then L_{1} ×_{s} L_{2} is product-matching (i.e. L_{1} ×_{s} L_{2} = [L_{1}, L_{2}]).

• If L is axiomatized by a set of □p → □^{n}p, ◇□p → p and/or closed formulas, then L ×_{s} S5 has f.m.p..

But the products (×_{s}) of logics have a bad property. We do NOT always have

L(C_{1}) ×_{s} L(C_{2}) = L(C_{1} ×_{s} C_{2}), (1)

for any classes C_{1}, C_{2} of Kripke frames. The logic LIN ×_{s} S5 give us a counterexample [2].

In the following (Sections 4), we will define another products (×) of logics on which the property (1) holds.

2 Products of Modal Logics by General Frames

Let F = (W, R, P) and G = (V, S, Q) be general frames. That is, P is a modal algebra of sets on Kripke frame F, which contains ∅ and is closed under ∩, ∪, −, □, where □X = {x ∈ W | xRy ⇒ y ∈ X}. Also we set κF as (W, R, 2^{W}). We define the products of general frames as follows. F × ×G := (W × V, R × S, P × ×Q), where

R × S := {((x, y), (t, u)) | xRt, ySu},
P × ×Q := ma({X × Y | X ∈ P, Y ∈ Q}),

i.e. the smallest modal algebra containing {X × Y | X ∈ P, Y ∈ Q}.

Note that (W, R) ×_{s} (V, S) = (W × V, R × Δ, Δ × S), where Δ denotes a diagonal relation.

Theorem 2.1  P × ×Q = {⋃_{i∈I} X_{i} × Y_{i} | X_{i} ∈ P, Y_{i} ∈ Q, I : finite}.

Proof. It is implied by following (2)–(7).

•  ∅ = ∅ × ∅(= ∅ × V = W × ∅).  (2)
•  ⋃_{i∈I} X_{i} × Y_{i} ∩ ⋃_{j∈J} T_{j} × U_{j} = ⋃_{(i,j)∈I×J}(X_{i} ∩ T_{j}) × (Y_{i} ∩ U_{j}).  (3)

•  ⋃_{i∈I} X_{i} × Y_{i} ∪ ⋃_{j∈J} T_{j} × U_{j} = ⋃_{k∈I⊔J} A_{k} × B_{k},  (4)

where I ⊔ J = {(i, 0) | i ∈ I} ∪ {(j, 1) | j ∈ J}, A_{(i,0)} = X_{i}, A_{(j,1)} = T_{j}, B_{(i,0)} = Y_{j}, B_{(j,1)} = U_{j}.

•  − ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{J∈2^{I}}(− ⋃_{i∈J} X_{i}) × (− ⋃_{i∈−J} Y_{i}).  (5)

•  ◇ ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{i∈I} ◇X_{i} × ◇Y_{i}.  (6)

•  □ ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{A⊆2^{I}}(□ ⋂_{J∈A} ⋃_{i∈J} X_{i}) × (□ ⋃_{J∈A} ⋂_{i∈J} Y_{i}).  (7)

Moreover, the following holds.

• ⋃_{i∈I} X_{i} × Y_{i} = ⋃_{j∈J} T_{j} × U_{j}

⟺ ∀i ∈ I, ∃A ⊆ 2^{J} such that X_{i} ⊆ ⋂_{J′∈A} ⋃_{j∈J′} T_{j}, Y_{i} ⊆ ⋃_{J′∈A} ⋂_{j∈J′} U_{j},  (8)
and ∀j ∈ J, ∃A ⊆ 2^{I} such that T_{j} ⊆ ⋂_{I′∈A} ⋃_{i∈I′} X_{i}, U_{j} ⊆ ⋃_{I′∈A} ⋂_{i∈I′} Y_{i}.

Proposition 2.2 κF × ×κG = κ(F × ×G) ⟺ either F or G is finite.

Proposition 2.3 Let α be ◇^{m_{1}}□^{n_{1}}p_{1} ∧ ⋯ ∧ ◇^{m_{k}}□^{n_{k}}p_{k} → φ(p_{1}, …, p_{k}), where φ is constructed by ∧, →, □, ◇ from p_{1}, …, p_{k}. Then F ⊧ α, G ⊧ α ⇒ F × ×G ⊧ α, and κF ⊧ α, κG ⊧ α ⇒ κ(F × ×G) ⊧ α.

3 The Dual Algebras

For any general frame F = (W, R, P), we denote the dual algebra of F by F^{+} = (P, ∩, ∪, −, ∅, □).

For any (normal) modal algebra A = (A, ∧, ∨, ¬, 0, □), we denote the dual frame of A by A_{+} = (P F (A), RA, PA), where

1. P F (A) is the set of all prime filters of A

2. xRA y ⟺^{def} ∀a ∈ A(□a ∈ x ⇒ a ∈ y),

3. PA = {{x ∈ P F (A) | a ∈ x} | a ∈ A}.

We define the products of modal algebras as follows. For modal algebras A, B, A × ×B := (A_{+} × ×B_{+})^{+}

By (2)–(8), we can easily get the following proposition.

Proposition 3.1 F_{1}^{+} ≃ F_{2}^{+}, G_{1}^{+} ≃ G_{2}^{+} ⇒ (F_{1} × ×G_{1})^{+} ≃ (F_{2} × ×G_{2})^{+}. Especially, A ≃ F^{+}, B ≃ G^{+} ⇒ A × ×B ≃ (F × ×G)^{+}.

Hence for general frames F, G, we have

(F × ×G)^{+} ≃ F^{+} × ×G^{+}. (9) Recall that

a general frame F = (W, R, P) is descriptive (i.e. ∃A: modal algebra, F ≃ A_{+} ) ⟺

• differentiated ∀x, y ∈ W (x ≠ y ⇒ ∃X ∈ P such that x ∈ X, y ∉ X),

• tight ∀x, y ∈ W (x R̸y ⇒ ∃X ∈ P such that x ∈ X, y ∉ X),

• compact ∀A ⊆ P((⋂ A_{0} ≠ ∅ for finite A_{0} ⊆ A) ⇒ ⋂ A ≠ ∅). Proposition 3.2 If general frames F, G are descriptive, then the product F × ×G is also descriptive. Hence for modal algebras A, B, we have

(A × ×B)_{+} ≃ A_{+} × ×B_{+}. (10)

4 Products of Modal Logics by General Frames

For any modal logic L, we denote by F (L) the set of all general frames which validate L, and by V (L) the set of all modal algebras which validate L. For modal logics L_{1}, L_{2}, we define

L_{1} × ×L_{2} := L(F (L_{1}) × ×F (L_{2})). By (9) and (10), we have

L_{1} × ×L_{2} = L(V (L_{1}) × ×V (L_{2})). Let K be a class of modal algebras.

V (K) denotes the smallest variety containing K. H(K) denotes the smallest class containing K closed under homomorphic images. S(K) denotes the smallest class containing K closed under subalgebras. P (K) denotes the smallest class containing K closed under direct product.

For any modal algebra A, we denote by fA a isomorphism from A to (A_{+})^{+}. Theorem 4.1

1. If h : A_{1} → A_{2} and g : B_{1} → B_{2} are homomorphic onto maps, then h × ×g : A_{1} × ×B_{1} → A_{2} × ×B_{2}

defined by

h × ×g(⋃_{i∈I} X_{i} × Y_{i}) = ⋃_{i∈I} f_{A_{2}} ∘ h ∘ fA_{1}^{−1}(X_{i}) × f_{B_{2}} ∘ g ∘ fB_{1}^{−1}(Y_{i})

is also homomorphic onto map.

2. If A_{1} is a subalgebra of A_{2} and B_{1} is a subalgebra of B_{2}, then A_{1} × ×B_{1} is also a subalgebra of A_{2} × ×B_{2}.

3. ∏_{λ∈Λ} A_{λ} × × ∏_{μ∈M} B_{μ} is a subalgebra of ∏_{(λ,μ)∈Λ×M} A_{λ} × ×B_{μ}.

Hence for classes K_{1}, K_{2} of modal algebras,

1. H(K_{1}) × ×H(K_{2}) ⊆ H(K_{1} × ×K_{2}),

2. S(K_{1}) × ×S(K_{2}) ⊆ S(K_{1} × ×K_{2}),

3. P (K_{1}) × ×P (K_{2}) ⊆ SP (K_{1} × ×K_{2}).

Therefore we have the following theorem. Theorem 4.2 Let K_{1} and K_{2} be classes of modal algebras, and let C_{1} and C_{2} be classes of general frames. Then

1. V (V (K_{1}) × ×V (K_{2})) = V (K_{1} × ×K_{2}),

2. L(K_{1}) × ×L(K_{2}) = L(K_{1} × ×K_{2}),

3. L(C_{1}) × ×L(C_{2}) = L(C_{1} × ×C_{2}).

Now we define another products (×) of logics instead of products (×_{s}) of logics.

Let A = (A, ∧, ∨, ¬, 0, □A) and B = (B, ∧, ∨, ¬, 0, □B) be modal algebras, and let F = (W, R, P) and G = (V, S, Q) be general frames. Then we define as follows. A^{∘} := (A, ∧, ∨, ¬, 0, □A, □B) with □Bb = b, ∘B := (B, ∧, ∨, ¬, 0, □A, □B) with □Aa = a. F^{∘} := (W, R, Δ, P), ∘G := (V, Δ, S, Q). F × G := F^{∘} × ×^{∘}G. For modal logics L_{1}, L_{2}, L_{1} × L_{2} := L(F (L_{1}) × F (L_{2})).

Since (A_{+})^{∘} = (A^{∘})_{+} and (F^{+})^{∘} = (F^{∘})^{+} hold, we have the following theorem. Theorem 4.3 Let K_{1}, K_{2} be classes of modal algebras, and let C_{1}, C_{2} be classes of general frames. Then

1. V (K^{∘}) = V (K)^{∘}, V (^{∘}K) = ^{∘}V (K),

2. L(K_{1}) × L(K_{2}) = L(K_{1}^{∘} × ×^{∘}K_{2}),

3. L(C_{1}) × L(C_{2}) = L(C_{1} × C_{2}).

Note that L_{1} × L_{2} = (L_{1} ∗ (K ⊕ □p ↔ p)) × ×((K ⊕ □p ↔ p) ∗ L_{2}).

The following proposition about properties of L_{1} × L_{2} holds. Proposition 4.4 Let L_{1}, L_{2} be modal logics. Then

1. If L_{1} and L_{2} are consistent mono-modal logics, then L_{1} × L_{2} is a conservative extension of L_{1} and L_{2}.

2. L_{1} × L_{2} ⊇ [L_{1}, L_{2}],

3. If L_{1} andL_{2} have f.m.p., then L_{1} × L_{2} has product f.m.p.(i.e. L_{1} × L_{2} = L(F_{f}(L_{1}) × F_{f}(L_{2}))), hence L_{1} × L_{2} also has f.m.p.. (F_{f}(L) denotes the set of all general frames which validate L.)

4. If one of L_{1} and L_{2} has f.m.p. and the other is Kripke complete, then L_{1} × L_{2} is also Kripke complete.

References

[1] D. Gabbay and V. Shehtman, Products of modal logics, Part I . L. J. of IGPL, 6(1), pp. 73 – 146, 1998.

[2] M. Reynolds, A decidable temporal logic of parallelism. (Forthcoming)

[3] V. Shehtman, Two-dimensional modal logics. Math. Zametki, 5, pp. 759 – 772, 1978. (In Russian)