Subframe formulas for S4-type intuitionistic modal logic

Kazuyo Inoi

                    inoi@maphy.jcn.nihon-u.ac.jp

Junior College, Nihon University

The subframe formulas Y for S4-type intuitionistic modal logic L_{0} is introduced. It is shown that the logic L_{0} + Y + bw_{n} has the finite model property.

1 Intuitionistic modal logics

In this section, we repeat some definitions and notations in [3].

Formulas are constructed using by propositional variables, p_{0}, p_{1}, ⋯, logical symbols, ∧, ∨, ⊃, ¬, □, ⊤ and ⊥ (not included ◇).

The logic L_{0} is the logics obtained from 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.

The intuitionistic modal logics are extension of L_{0} and closed the above rules. A triple (N, ≤, R) is called an I-frame if the following conditions are satisfied.

• N is a non-empty set.

• ≤ is a partial order on N.

• R is a reflexive and transitive relation on N such that x ≤ y implies xRy for each x, y ∈ N.

Let M be an I-frame (M, ≤, R). M is said to be rooted if it has a least element with respect to R, that is, there is an element 0 ∈ M such that 0Ra and a ≰ 0 for any other element a ∈ M. This element 0 is said to be a root. If M is an I-frame, then we let

IS_{≤}(a) = {b : a ≤ b}
IS_{R}(a) = {b : aRb}

aR^{∼}b denotes aRb and bRa. w is said to be maximal with respect to A if

A ≡ B ⊃ C, w |̸= A ⇒ ∀v(w ≤ v and v ⊧ A),  (1)
A ≡ ¬B, w |̸= A ⇒ ∀v(w ≤ v and v ⊧ A),  (2)
A ≡ □B, w |̸= A ⇒ ∀v(w\overrightarrow{R}v and v ⊧ A).  (3)

A pair (M, ⊧) is said to be an I-model if, for all a ∈ M, any propositional variable p and any formulas A, B,

1. a ⊧ p and a ≤ b ⇒ b ⊧ p,

2. a ⊧ A ∧ B ⇔ a ⊧ A and a ⊧ B, 3. a ⊧ A ∨ B ⇔ a ⊧ A or a ⊧ B,

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

5. a ⊧ ¬A ⇔ ∀b(a ≤ b implies b |̸= A),

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

2 Preliminaries

In this section, we show some property of I-models. We can easily verify the next propositions. Proposition 2.1 L_{0} ⊢ □¬(□p ∨ □¬□p) ⊃ ⊥

L_{0} ⊢ ¬(¬p ∨ p) ⊃ ⊥

Let L ⊇ L_{0}, ML be a canonical model for L and u ∈ ML. Proposition 2.2 u is an element in maximal cluster iff □A ∨ □¬□A ∈ u for every wff A. Proposition 2.3 u is maximal with respect to ≤ iff ¬A ∨ A for every wff A. Proposition 2.4 For all u ∈ ML , there exists a maximal element with respect to ≤. Proposition 2.5 For all u ∈ ML, there exists a maximal element with respect to R.

Let bw_{n} be the following formula:

bw_{n} = ⋁_{i=0}^{n} □(□p_{i} → ⋁_{i≠j} □p_{j})(n ≥ 1).

Lemma 2.6 M validates bw_{n} iff each point in M has at most n R-incomparable successors.

For a formula A, we define the relation ∼_{F (A)} to get results on model equivalence with respect to A between two models. Let M and N are I-frames. We define ∼_{F (p)}, ≤_{F (p)}, ≡_{F (A)} and ∼_{F (A)} as follows:

(M, a) ∼_{F (p)} (N, v) ⇔ ∀p(a ⊧ p ⇔ w ⊧′ p)
(M, a) ≤_{F (A⊃B)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(a ≤ b → u ≤′ v) and
(M, b) ∼_{F (A)} (N, v) and
(M, b) ∼_{F (B)} (N, v))
(M, a) ≤_{F (¬A)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(a ≤ b → u ≤′ v) and
(M, b) ∼_{F (A)} (N, v)
(M, a) ≤_{F (□A)} (N, v) ⇔ ∀b ∈ M, ∃v ∈ N(aRb → uR′v), and
(M, b) ∼_{F (A)} (N, v)
(M, a) ≡_{F (A)} (N, v) ⇔ (M, a) ≤_{F (A)} (N, v) and
(N, v) ≤_{F (A)} (M, a)
(M, a) ∼_{F (A)} (N, v) ⇔ (M, a) ∼_{F (p)} (N, v) and
(M, a) ≡_{F (A)} (N, v)

For (M, w) ∼_{F (A)} (M, v), we write w ∼_{F (A)} v if M is understood. |w|_{F (A)} denotes the set {v ∈ M : w ∼_{F (A)} v}. Lemma 2.7 Let M and N be I-frames. For any formula A and a ∈ M, v ∈ N,

(M, a) ∼_{F (A)} (N, v) ⇒ (v ⊧ A → a ⊧ A)

Proof. By the induction on the construction of A

Lemma 2.8 Suppose A ⊃ B ∉ w (respectively, ¬A ∉ w) for w ∈ M_{L}, w is not maximal element with respect to A ⊃ B (respectively, ¬A). Then there exists v(v ∈ M_{L}, w ≤ v) which v is maximal with respect to A ⊃ B (respectively, ¬A).

Lemma 2.9 Suppose □A ∈ w, for w ∈ M_{L}, w is not maximal element with respect to □A. Then there exists v(v ∈ M_{L}, wRv) which v is maximal with respect to □A.

Definition 2.10 (p-morphism,subreduction) Let M and N be I-frames. A map f from N = (N, ≤_{N} , R_{N}) to M = (M, ≤_{M}, R_{M}) is called a p-morphism if the following conditions are satisfied, for any u, v ∈ N and a ∈ M,

(p-1) f is onto,

(p-2) If u ≤_{N} v then f(u) ≤_{M} f(v),

(p-3) If uR_{N}v then f(u)R_{M}f(v),

(p-4) If f(u) ≤_{M} a then there exists v such that u ≤_{N} v and f(v) = a,

(p-5) If f(u)R_{M}a then there exists v such that uR_{N}v and f(v) = a.

A map f from N to M is called a subreduction if f is a p-morphism from a subframe of N to M. And then, N is subreducible to M.

3 subframe formulas

In this section, we introduce subframe formulas for L_{0} by the method as Shimura defined for the intuitionistic logic in [4]. Fine showed the completeness of subframe logics Y (M, 0) for K4 [2]. It was shown by selecting finite points from canonical models. We show the completeness some logics containing L_{0} by the same method as Fine.

For a rooted and finite I-frame, we define the subframe formulas by the induction on the cardinality of a ↑_{≤}, a ↑_{R} as follows:

X_{≤}(M, a) = ⋁_{b≰a} p_{b} ∨ ⋁_{aR̸^{∼}d^{d∈IS_{≤}(a)}} Y (M, d) ∨ ⋁_{aR^{∼}e^{a∈IS_{≤}(e)}} X(M, e),

X_{R}(M, a) = ⋁_{cR̸a} □q_{c} ∨ ⋁_{e∈IS_{R}(a)} □Y (M, e),
X(M, a) = p_{a} ∧ □q_{a} ⊃ p ∨ X_{≤}(M, a) ∨ X_{R}(M, a),
Y_{R}(M, a) = ⋀_{a′∈Cl(a)}( ⋀_{a′′R^{∼}a′} □(□X(M, a′′) ⊃ X(M, a′))),
Y (M, a) = Y_{R}(M, a) ⊃ X(M, a).

Proposition 3.1 Let M be a finite and rooted I-frame and a, b ∈ M. Then,

1. if b ≤ a does not hold, L_{0} ⊢ p_{b} ⊃ Y (M, a),

2. if bRa does not hold, L_{0} ⊢ □q_{b} ⊃ Y (M, a),

3. if a ≤ b hold, Y (M, b) ⊃ Y (M, a),

4. if a ≤ b hold, Y (M, b) ⊃ Y (M, a),

5. if aRb hold, □Y (M, b) ⊃ Y (M, a).

Lemma 3.2 Let (N, ⊧) be an I-frame, u ∈ N and M be a finite and rooted I-frame. If u |̸= Y (M, a) then there exists v ∈ N such that

u ≤ v, v ⊧ p_{a} ∧ □q_{a} and v |̸= Y (M, a).

Lemma 3.3 Suppose there is a subreduction f from N to M, formula E and formulas sets {F_{a}; a ∈ M} and {□G_{a}; a ∈ M} such that

∃v(a ≰ f(v), u ≤ v) → u |̸= F_{a}
∃v(a R̸f(v), uRv) → u |̸= □G_{a}
∃v(uRv, v ∈ dom(f)) → u |̸= E

Then the formula obtained from Y (M) by substituting F_{a} (respectively, G_{a}) for p_{a} (respectively, q_{a}) for every a ∈ M and E for p is refuted on N.

Theorem 3.4 Let M be a finite and rooted I-frame. Then the following are equivalent, for any I-frame N,

• N |̸= Y (M),

• there is a subreduction f from N to M.

Proof. (⇒) Assume N |̸= Y (M). Define a partial map f from N to M

f(u) = \{ \begin{matrix}a & (u ⊧ p_{a} ∧ □q_{a} and u |̸= Y (M, a)), \\ undefined & (otherwise). \end{matrix}

Then, f is a subreduction from N to M. (⇐) For u ∈ N, define a valuation ⊧ on N as follows:

∃v(a ≰ f(v), u ≤ v) → u |̸= p_{a}
∃v(a R̸f(v), uRv) → u |̸= □q_{a}
∃v(uRv, v ∈ dom(f)) → u |̸= p

Lemma 3.5 Let L_{0} + {Y (M_{i})}_{i∈I} + bw_{n}. There no finite subframe of NL is reducible to M_{i}.

Lemma 3.6 Suppose that w ∈ ML, w |̸= A. Then there is a finite submodel N = (N, ≤′, R′, ⊧′) of w ↑_{R} and v |̸= A for v ∈ N.

Proof. By the induction on the construction A.

(i) If A is a propositional variable, let N = {w} and w = v. (ii) Otherwise. By Proposition 2.4 Proposition 2.5, there exists a point w′ such that w′ |̸= □A and w′ is maximal with respect to R. We define N by the induction on the cardinality of \{|v|_{F (A)} : w′ ≤ v\} and \{|v|_{F (A)} : w′\overrightarrow{R}v\}. Let N′ = {w′}. Suppose U = {u : w′ ∼ u}, X = {|u|_{F (A)} : u ∈ U}. Pick representatives x_{1}, x_{2}, ⋯, x_{n} from X such that each x_{i}(i = 1 ⋯ n) is maximal with respect to ≤. Let rank_{x_{i}} = |{|u|_{F (A)} : x_{i} ≤ u and u ∈ U}|. If rank_{x_{i}} = 1 then U_{x_{i}} = {x_{i}}. Otherwise, let Y = {|x_{ij}|_{F (A)} : x_{i} ≤ x_{ij} and x_{ij} ∈ U}. Pick representatives y_{1}, y_{2}, ⋯, y_{l} from Y such that each y_{i}(i = 1 ⋯ l) is maximal with respect to ≤. Let U_{x_{i}} = U_{y_{1}} ∪ U_{y_{2}} ∪ ⋯ ∪ U_{y_{l}} and U = ⋃_{i=1}^{n} U_{x_{i}}. Next for each w_{i} ∈ U, let S = \{|s|_{F (A)} : w_{i} ≤ s and w_{i}\overrightarrow{R}s\}, and S′ = \{|s′|_{F (A)}\S : w_{i}\overrightarrow{R}s′\}. If S = {|w_{i}|_{F (A)}} or S = ∅ then let T_{w_{i}}^{≤} = ∅. Otherwise, pick representatives s_{1}, s_{2}, ⋯, s_{m} from S such that each s_{i}(i = 1 ⋯ m) is maximal with respect to ≤. And Let T_{w_{i}}^{≤} = N_{s_{1}} ∪ N_{s_{2}} ∪ ⋯ ∪ N_{s_{m}}. If S′ = {|w_{i}|_{F (A)}} or S′ = ∅ then let T_{w_{i}}^{R} = ∅. Otherwise, pick representatives s′_{1}, s′_{2}, ⋯, s′_{n} from S′ such that each s_{i}(i = 1 ⋯ n) is maximal with respect to R. And Let T_{w_{i}}^{R} = N_{s′_{1}} ∪ N_{s′_{2}} ∪ ⋯ ∪ N_{s′_{n}}. Set T_{w_{i}} = T_{w_{i}}^{≤} ∪ T_{w_{i}}^{R} and T = T_{w_{1}} ∪ T_{w_{2}} ⋯ T_{w_{p}}.

Let N = N′ ∪ U ∪ T.

Theorem 3.7 L_{0} + {Y (M_{i})}_{i∈I} + bw_{n} has finite model property. Corollary 3.8 L_{0} + {Y (M_{i})}_{i∈I} + bw_{n} is complete.

References

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

[2] K. FINE, Logics containing K4 part II, Journal of Symbolic Logic 50(1985), pp.619-651.

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

[4] T. SHIMURA, Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas, Studia Logica 52(1993), pp.23-40.

[5] M. ZAKHARYASCHEV, Canonical formulas for K4 part I: basic results, Journal of Symbolic Logic 57(1992), pp.1377-1402.