Kripke completeness of predicate extensions of cofinal subframe logics

SHIMURA Tatsuya

               shimura@math.cst.nihon-u.ac.jp

Department of Mathematics, College of Science and Technology, Nihon University

1 The problem.

In the study of non-classical logics, it is a natural and fundamental question to ask the completeness of predicate extensions of Kripke complete propositional logics.

For the subframe logics containing S4, we have the following characterization for the completeness of the predicate extensions with constant domains.

Theorem 1 (Shimura [5], Tanaka-Ono [7], Chagrov-Zakharyashev [1]) Let L be a subframe logic containing S4. The following are equivalent:

• L is canonical.

• L has the finite embedding property.

• Q-L + BF is Kripke complete.

In particular, we have the following corollary.

Corollary 1 (Shimura [5], cf. Shimura [3]) (1). Let {M_{i}} be a set of finite and rooted Kripke frames without non-trivial clusters.

Then, QS4 + {α(M_{i})} + BF is Kripke complete.

(2). Let M be a finite and rooted Kripke frame with a non-trivial cluster.

Then, QS4 + α(M) + BF is Kripke incomplete.

If we consider a similar characterization problem for cofinal subframe logics, it is natural to settle the following question. (The necessity of axioms like T (K) is discussed in the talk [5]).

Question 1 Find a necessary and sufficient condition for the Kripke completeness of QS4 + {α(M_{i}, ⊥)} + T (K) + BF.

Note that the canonicity of L is not sufficient for the completeness by the result of Skvortsov [6]. So, the answer of the above question seems much difficult than the subframe case.

Although we do not have the answer, we give a partial answer corresponding to Corollary 1.

Theorem 2 We consider the following conditions for finite and rooted (S4-) Kripke frame.

(C1) There is no non-trivial inner clusters.

(C2) The set of the inner points has a common upper bound c such that {c} is a trivial cluster.

Then, we have the following.

(1). Let {M_{i}} be a set of finite and rooted Kripke frames satisfying above conditions. Then, QS4 + {α(M_{i}, ⊥)} + T (K) + BF is Kripke complete.

(2). Let M be a finite and rooted Kripke frame. If lM does not satisfy one of the above conditions, QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

2 The sketch of the proof of Theorem 2 (1).

To axiomatize the cofinal subframe logics, we use a variant ¬C_{M_{i}} of Fine’s subframe formula ¬B_{M_{i}} and frame formula ¬F_{M_{i}}, where B_{M_{i}}, F_{M_{i}} and C_{M_{i}} are the following:

B_{M_{i}} = p_{r} ( r is the root of M_{i}) ∧ ⋀_{a≠b} □¬(p_{a} ∧ p_{b})

∧ ⋀_{aRb} □(p_{a} ⊃ ◇p_{b}) ∧ ⋀_{aR̸b} □(p_{a} ⊃ ¬◇p_{b})

F_{M_{i}} = □( ⋁_{a∈M_{i}} p_{a}) ∧ B_{M_{i}},

C_{M_{i}} = □◇( ⋁_{a∈M_{i}} p_{a}) ∧ B_{M_{i}}.

The main tool of the completeness proof is the same as in [3], that is, the method of canonical models. Let N be the canonical frame for QS4 + {α(M_{i}, ⊥)} + T (K) + BF. We show a contradiction from the assumption that there is a cofinal subreduction from N to some M_{i}. Let C′ = {c} be a maximal cluster of M_{i} such that c is a common upper bound of the inner points.

We show that there is a ’definable’ cofinal subreduction from N to M_{i}. A function h from a Kripke model to a Kripke frame M_{i} is said to be difinable if there are formulas F_{a} (a ∈ M_{i}) such that

u ∈ h^{−1}(a) ⇔ u ⊧ F_{a}.

The difficulty arises from the fact that the family {u|u ⊧ F_{a}} (a is maximal) must forms a partition of the maximal points of N. To avoid this difficulty, we construct the map in two steps. Firstly, we construct a disjoint family {u|u ⊧ F_{a}} (a is maximal, a ≠ c). Secondly, we define the map so that the rest maximal points are mapped to c. By virtue of the condition (C2), the map constructed turns to be a cofinal subreduction.

Lemma 1 There is a finite subframe N′ of N with the following conditions.

• There is a p-morphism g from N′ to M_{i}.

• Each maximal cluster of N′ is contained by some maximal cluster of N.

Proof) This is because of the conditions that T (K) is valid N and M_{i} contains no non-trivial inner clusters. ■

Lemma 2 (1). For each a ∈ N′, there exists a formula F_{a} satisfying the following:

a ⊧ F_{a}, a |̸= F_{b} (b ≠ a).

(2). For each maximal cluster C of N′, there exists a formula G_{C} satisfying the following:

a ⊧ □G_{C} (a ∈ C), a |̸= ◇G_{C} (a is maximal, a ∉ C).

(3). For each inner point a ∈ N′, there exists a formula H_{a} satisfying the following:

a |̸= □◇□H_{a} ⊃ H_{a}.

Definition 1

H = ⋀ □(□◇□H_{a} ⊃ H_{a})

P_{a} = \{ \begin{matrix}H ∧ □G_{C} ∧ ⋀_{b∈C} □◇F_{b} ∧ F_{a} & (a is maximal , a ≠ c, a ∈ C) \\ H ∧ ⋀_{b≠c,b is maximal} □¬P_{b} & (a = c) \\ \begin{aligned}¬(□◇□H_{a} & ⊃ H_{a}) ∧ F_{a} \\ & ∧ ⋀_{aR̸b} □¬F_{b} ∧ ⋀_{b≠a} ¬F_{b} ∧ ⋀_{aRb} ◇P_{b} \end{aligned} & (a is an inner point.) \end{matrix}

Lemma 3 (1). N_{0} = {u ∈ N|u ⊧ P_{a} for some a} is a cofinal subframe of N.

(2). For each u ∈ N_{0}, there exists exactly one a ∈ N′ with u ⊧ P_{a}. The map f defined by f(u) = g(a) is a cofinal subreduction from N to M_{i}.

(3). u ⊧ P_{0} implies u ⊧ C for some instance C of C_{M_{i}}.

3 The outline of the proof of Theorem 2 (2).

We treat the case dviding into three cases.

Lemma 4 If M does not satisfy the condition (C1), QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Proof) The incompleteness proof for QS4 + α(M) + BF works in this case. ■

Lemma 5 If the set of the inner points of M does not have a common upper bound, QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Lemma 6 If the inner points of M has a common upper bound but no trivial clusters are u QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Since the proofs of Lemma 5, 6 are quite complicated, we show the outline usinge typical examples.

The example for Lemma 6 is treated by Skvortsov [6] for intermediate predicate logics. But, his proof seems difficult to generalize since he uses Kripke bundle semantics.

We give a proof using a Kripke model. For each formula, the model behaves as a finite model, but it behaves as an infinite model for the whole formulas. The idea is described in Hughes-Cresswell [2].

Example 1 Let M and N be the following frames. There exist a formula A and a model ⟨N, ω, ⊧⟩ with the following conditions.

(1). A is not separable from L = QS4+α(M, ⊥)+T (K)+BF by Kripke frame semantics.

(2). Every instance of L is true in ⟨N, ⊧⟩.

(3). A is refuted in ⟨N, ⊧⟩.

[figure: a_{1}; a_{2}; a_{3}; b_{1}; b_{2}; b_{3}; ⋯]

For each language with finitely many constants, some a_{n} and b_{n} has completely same behaver under the valuation ⊧.

Example 2 Let M and N be the following frames. There exist a formula A and a model ⟨N, ω, ⊧⟩ with the following conditions.

(1). A is not separable from L = QS4+α(M, ⊥)+T (K)+BF by Kripke frame semantics.

(2). Every instance of L is true in ⟨N, ⊧⟩.

(3). A is refuted in ⟨N, ⊧⟩.

[figure] [figure: · · · · · ·]

For each language with finitely many constant symboles, some cluster behaves as a trivial cluster under ⊧.

References

[1] A. Chagrov, and M. Zakharyaschev, Modal logic, Clarendon Press, Oxford (1997)

[2] Hughes, G.E. and Cresswell, M.J., A new introduction to modal logic, Routledge, London (1986).

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

[4] Shimura, T., On some modal predicate logics with Glivenko type characterization. MLG meeting (2000-1-11).

[5] Shimura, T., Kripke incompleteness of predicate extensions of the modal logics axiomatized by a canonical formula for a frame with a nontrivial cluster, Studia Logica 65 (2000), 237–247.

[6] D. Skvortsov, On some Kripke complete and Kripke incomplete intermediate predicate logics, Studia Logica 61 (1998), 281–292.

[7] Y. Tanaka, and H. Ono, Rasiowa-Sikorski lemma and Kripke completeness of predicate and infinitary modal logics, Advances in Modal Logic ’98, (1998).