Logics of finite width for Some Intuitionistic Modal Logic

Kazuyo Inoi Junior college, Nihon University

             E-mail: inoi@info.jcn.nihon-u.ac.jp

Abstract

Fine [1] showed the completeness of logics of finite width for K4. We treat the logic containing the S4-type intuitionistic modal logic L_{0}.

For the logic L_{0}, we show the completeness of the logics of finite width with respect to one relation.

1 Preliminaries.

In [2], Ono introduced the intuitionistic modal logic L_{0} and it is shown the logic is complete for the I-frame.

We repeat the axioms of the intuitionistic modal logic L_{0} and I-frame. L_{0} is the logic obtained from the intuitionistic logic H by adding the following axioms, □p ⊃ p, □p ⊃ □□p, □(p ⊃ q) ⊃ (□p ⊃ □q), and closed under the rules of substitution, necessitation and modus ponens. A triple F = (M, ≤, R) is called an I-frame if the following conditions are satisfied.

• M is a non empty set.

• ≤ is a partial order on M.

• R is a pre-order on M, that is, x ≤ y implies xRy for each x, y ∈ M.

A relation ⊧ between M and the set of propositional variables is said to be a valuation on F if

a ⊧ p and a ≤ b ⇒ b ⊧ p

holds for every a, b ∈ M and every variable p. We can extend a valuation on M and the set of formulas in the following way.

1. a ⊧ A ∧ B ⇔ a ⊧ A and a ⊧ B,

2. a ⊧ A ∨ B ⇔ a ⊧ A or a ⊧ B,

3. a ⊧ A ⊃ B ⇔ ∀b(a ≤ b)b |̸= A or b ⊧ B, 4. a ⊧ ¬A ⇔ ∀b(a ≤ b implies b |̸= A),

5. a ⊧ □A ⇔ ∀b(aRb implies b ⊧ A).

The pair (F, ⊧) of I-frame F and a valuation ⊧ on F is said to be an I-model.

A formula A is said to be true in (F, ⊧) if a ⊧ A holds for any a ∈ M. A formula A is said to be valid in F if a is true in any model (F, ⊧), and any a ∈ M.

We write FL instead of the canonical frame for a logic L and ML instead of the canonical model for a logic L. If a logic L′ is the restriction of L to finite subset of propositional valiables then L′ is said to be weak.

Lemma 1.1 Suppose M = (M, ≤, R, ⊧) is an I-model, A′ is a formula substituted B_{i} for p_{i} in A and M′ = (M, ≤, R, ⊧′) is an I-model such that

∀x ∈ M(M′, x) ⊧′ p_{i} ⇔ (M, x) ⊧ B_{i}, i = 0, 1, ⋯, n.

Then

(M′, x) ⊧′ A ⇔ (M, x) ⊧ A′.

Lemma 1.2 Suppose Δ is closed under substitution and true in M = (M, ≤, R, ⊧_{M}). Then Δ is true in each definable variant N = (M, ≤, R, ⊧_{N}).

Lemma 1.3 Suppose L′ is the weak restriction of a logic L. Then L is true in ML′.

2 The logics of finite ≤-width.

In this section, we define the formula of ≤-width n.

For n ≥ 1, let BW_{n} be the formula

⋁_{i=0}^{n} □(p_{i} ⊃ ⋁_{j≠i} p_{j}).

w and v are said to be ≤-incomparable if the elements are incomparable with respect to the relation ≤. An I-frame (M, ≤, R) is of ≤-width n if it does not contain (n + 1) mutually ≤-incomparable elements. A frame F is of finite ≤-width if it is of ≤-width n for some n. A logic L is of finite ≤-width if L ⊇ L_{0} + BW_{n} for some n > 0.

Theorem 2.1 Suppose L is a logic of finite ≤-width and a frame F = (M, ≤, R) is generated from FL by w. Then F is of finite ≤-width.

Lemma 2.2 Suppose an I-frame (M, ≤, R) is of finite ≤-width. If there is a infinite sequence w_{0}, w_{1}, ⋯ in M such that w_{j} R̸^{←}w_{i}forj > i. Then the sequence w_{0}, w_{1}, ⋯ consists of infinite subsequence v_{0}, v_{1}, ⋯ such that v_{i} ≤ v_{i+1} and v_{i} ≠ v_{i+1} for i = 0, 1, · · ·.

Let (M, ≤, R) be an I-model. w is ≤-deep if there is a elements w_{0}, w_{1}, ⋯ such that w_{i} ∈ M, w_{0} = w, w_{i} ≤ w_{i+1} and w_{i} ≠ w_{i+1} for i = 0, 1, · · ·. Let U_{w}^{≤} = {u ∈ M : w ≤ u and u is not ≤ -deep} and U_{w}^{R} = {u ∈ M : wRu and u is not ≤ -deep}. A ≤-deep w is called ≤-static if U_{w}^{≤} = U_{v}^{≤} for any ≤-deep v ∈ M(w ≤ v). A ≤-deep w is called R-static if U_{w}^{R} = U_{v}^{R} for any ≤-deep v ∈ M(w ≤ v).

For u ∈ M, let u_{p} = {p : u ⊧ p(p is a propositional variable)} and let |u|_{p} = {v_{p} : v ∈ M, u ≤ v and v is ≤ -deep}. A ≤-deep w is called ≤-stationary if |w|_{p} = |v|_{p} for any ≤-deep v ∈ M(w ≤ v).

Lemma 2.3 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and ≤-static.

Lemma 2.4 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and R-static.

Lemma 2.5 Let (M, ≤, R, ⊧) be an weak I-frame of finite ≤-width. For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep and ≤-stationary.

By Lemma 2.3, Lemma 2.4 and Lemma 2.5 For any ≤-deep w ∈ M, there is v(v ∈ M, w ≤ v) such that ≤-deep, ≤-static, R-static and ≤-stationary. So, we can get the next theorem.

Theorem 2.6 Suppose L is a logic of finite ≤-width. Then ML contains no infinite ≤-ascending chain.

Theorem 2.7 Suppose L is a logic of finite ≤-width. Then ML contains no infinite R-ascending chain.

Let F = (M, ≤, R) is an I-frame. A set V is said to be a ≤-cover for U ⊂ M if V ⊆ U and (∀u ∈ U)(∃v ∈ V)(u = v or u < v). F has finite ≤-cover property if each U ⊂ M has a finite ≤-cover.

Theorem 2.8 Let L′ be a weak logic of finite ≤-width and F = (M, ≤, R) be generated from FL by w. Then f has finite ≤-cover property.

3 Completeness results.

Let M = (M, ≤_{M}, R_{M}, ⊧_{M}) and N = (N, ≤_{N}, R_{N}, ⊧_{N}) be I-models and w ∈ M, v ∈ N. We defind the relations (M, w) ≤_{A} (N, v), (M, w) ≡_{A} (N, v) and (M, w) ∼_{A} (N, v) by induction on the construction of a formula A:

(M, w) ∼_{0} (N, v) ⇔ (w ⊧_{M} p ↔ v ⊧_{N} p) for any propositional variable p;
(M, w) ≤_{B⊃C} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and w ≤_{M} u ⇒
v ≤_{N} t, (M, u) ∼_{B} (N, t) and (M, u) ∼_{C} (N, t)];
(M, w) ≤_{¬B} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and w ≤_{M} u ⇒

v ≤_{N} t and (M, u) ∼_{B} (N, t)];
(M, w) ≤_{□B} (N, v) ⇔ ∀u ∈ M∃t ∈ N[w ≠_{M} u and wR_{M}u ⇒
vR_{N}t and (M, u) ∼_{B} (N, t)];
(M, w) ≡_{A} (N, v) ⇔ (M, w) ≤_{A} (N, v) and (N, v) ≤_{A} (M, w);
(M, w) ∼_{A} (N, v) ⇔ (M, w) ∼_{0} (N, v) and (M, w) ≡_{A} (N, v).

Let |w|_{A} = {v ∈ M : w ∼_{A} v}.

A model M is A-simple if there is finite V ⊂ M such that

• V covers |w|_{A} for each w ∈ M, and

• for all u, t ∈ M − V, ({v ∈ V : u ≤ v} = {v ∈ V : t ≤ v} and {v ∈ V : uRv} = {v ∈ V : tRv}) ⇒ u ∼_{0} t.

Lemma 3.1 Suppose (M, ≤, R) is an I-model of finite ≤-width. If a formula A is true in all weak A-simple models (M, ≤, R, ⊧) then A is valid in (M, ≤, R).

Proposition 3.2 Suppose M = (M, ≤, R, ⊧) is a natural model of finite ≤-width. Then there exist formula D_{w} such that w ⊧ D_{w}, w ∈ M and v |̸= D_{w}, v ∈ M(w ≰ v).

Lemma 3.3 Suppose M = (M, ≤, R, ⊧_{M}) is a natural model of finite ≤-width and N = (M, ≤, R, ⊧_{N}) is a simple weak model. Then there exist formulas A_{1}, A_{2}, ⋯, A_{n} such that w ⊧_{N} p_{i} ⇔ w ⊧_{M} A_{i}, for i = 0, 1 , ⋯ n.

Lemma 3.4 Let L be a logic of finite ≤-width and L′ be the weak restriction of L. Then FL′ is a frame for L.

Theorem 3.5 Each logic of finite ≤-width is complete.

References

[1] K. FINE, Logics containing K4 part I, Journal of Symbolic Logic 39(1974), pp.31-42.

[2] H. ONO, On some intuitionistic modal logics, Publ. RIMS, Kyoto Univ.13(1977), pp.687-722.