On some modal predicate logics with Glivenko type characterization.

SHIMURA Tatsuya

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

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

2000.1.11 (at MLG meeting)

1 Problem

Ghilardi [3] showed that QS4.1, the least predicate extension of S4.1 = S4 + □◇p ⊃ ◇□p, is not Kripke complete. Hughes-Cresswell [4] showed that QS4.1 + BF is Kripke incomplete, where BF is the Barcan formula ∀x□A(x) ⊃ □∀x A(x).

So, we consider the following problem.

Problem 1

(1). Find the Kripke completion of QS4.1.

That is, find the logic characterized by the modal predicate Kripke frames in which □◇p ⊃ ◇□p is valid.

(2). Find the Kripke completion of QS4.1 + BF.

That is, find the logic characterized by the modal predicate Kripke frames of constantdomains in which □◇p ⊃ ◇□p is valid.

Note that □◇p ⊃ ◇□p is valid in a Kripke frame (M, U) if and only if M has the following property:

For every u ∈ M, there is a maximal trivial cluster above w, that is, there is an element v such that uRv and vRw implies w = v for all w.

In this talk, I show a syntactical characterization of the Kripke completion of QS4.1 can be obtained by the method described in Shimura [6], and that of QS4.1+BF by modifying the method in Shimura [7].

2 Glivenko type characterization

It is well-known that the cut-free system GS4 for the modal propositional logic S4 gives a useful machinery to prove some syntactical properties and the completeness of S4. Shimura [6] gave some kinds of cut-free sequent style systems and showed that a similar machinery works for the logics defined by them.

The propositional logic S4.1 is one of the logics defined by the sequent style systems. That is, we can define it as the logic defined by the the sequent style system obtained from GS4 by adding the sequents of the form □Γ → provable in GTriv, where Triv = S4 + p ⊃ □p.

In other words, S4.1 can be characterized as the least logic with the following propety:

Triv ⊢ A ⇔ L ⊢ ◇□A.

The completeness proof of S4.1 by means of this sequent style system tells us that the characterization of the frames validating S4.1 is nothing but the following:

For every world w, there exits a world w′ above w in which Triv is valid. By transferring the above fact to predicate case, we can obtain the answer to Problem 1 (1).

Theorem 1 The Kripke completion is the logic defined by the sequent style system obtained from GQS4 by adding all the sequents of the form □Γ → provable in GQTriv.

3 Axiomatization.

We should find a formula C with the folloing property to give an axiomatizatiion of the Kripke completion of QS4.1.

QTriv ⊢ A ⇒ QS4.1 + C ⊢ ◇□A. If we try to prove the above assertion by induction on the complexity of the proof in GQTriv, the

crucial case is that the last inference is (→ ∀) or (∃ → ). So, we should take C as □∀x◇□A(x) ⊃ ◇□∀x A(x), which is the formula given by Corsi-Ghilardi [1].

Note that this formula is equivalent to the McKinsey-Tarski translation T (K) of Kroda axiom K = ∀x¬¬A(x) ⊃ ¬¬∀x A(x).

The logic axiomatized by T (K) over QS4 has the following characterization. Theorem 2 QS4 + T (K) is characteized as the least logic Lwith the folloing Glivenko type property.

QS5 ⊢ A ⇔ L ⊢ ◇□A. We can summarize the above facts as follows:

Fact 1 • QS4.1 + T (K) is Glivenko type characterization by QTriv

• QS4.1 + T (K) is the Kripke completion of QS4.1,

• QS4.1 + T (K) has modal disjunction property,

• QS4.1 + T (K) has modal existence property,

• QS4.1 + T (K) has interpolation property. Fact 2

• QS4 + T (K) has the Glivenko type characterization by QS5

• QS4 + T (K) has modal disjunction property,

• QS4 + T (K) has modal existence property, Note that QS4 + T (K) does not have the interpolation property since QS5 does not have it. We have few examples of modal predicate logics with the interpolation property. Moreover, we have

no general method to determine whether a given logic has the interpolation property or not. So the following question may be interesting. Question 1 (1). Does QS4.1 have interpolation property? (2). Does QS4.1 + T (K) + BF have interpolation property?

4 Completeness for the logics with the Barcan axiom.

First note that T (K) must be valid in the Kripke frames in which □◇p ⊃ ◇□p is valid. This implies the Kripke completion of QS4.1 + BF must contains T (K).

So we have to investigate the structure of the Kripke models with constant domains in which all the instances of T (K) are true.

Lemma 3 (cf. Shimura [7, Lemma 3.8]) Let (M, D, ⊧) be a canonical model with constant domains and (Γ, Δ) ∈ M the root of M. Then, if all the instances of T (K) belong to Γ, there exits a final cluster above any element of M.

Lemma 4 Let (M, D) be a Kripke frame with constant domains in which there exits a final cluster above any element of M. Then, □◇p ⊃ ◇□p is not valid in (M, D) if and only if there is a non-trivial final cluster in M.

Since QS4 + BF is strongly Kripke complete with respect to Kripke frames with constant domains, we can apply the method of canonical models by the aid of the above lemmas.

Theorem 5

(1). QS4 + T (K) + BF is Kripke complete.

(2). QS4.1 + T (K) + BF is Kripke complete.

This implies the following:

Fact 3 QS4 + T (K) + BF and QS4.1 + T (K) + BF have the following properties:

• modal disjunction property,

• modal existence property.

We can generalize the above completeness result as follows:

Theorem 6 (cf. Shimura [7]) Let M be the frame in the following figure and {M_{i}} a set of finite Kripke frames. If there is no cofinal subreduction from M_{i} to M for every M_{i}, QS4 + {α(M_{i}, ⊥)} + T (K) + BF is Kripke complete.

[figure: Figure 1:]

It is natural to ask whether L + T (K) + BF is complete or not for every cofinal subframe logic L. The answer was implicitely given in Isoda and Shimura [5]. In fact, the incompleteness proof of QS4.1.4+BF actually proves that of QS4.1.4 + T (K) + BF.

Theorem 7 (Isoda-Shimura [5]) Then, QS4.1.4 + T (K) + BF = QS4 + α(M, ⊥) + T (K) + BF is Kripke incomplete.

Added in proof: The author noticed after the talk that Theorem 6 is wrong. It seems that we can correct the statement by adding two more conditions on non-exsistence of cofinal subreductions to the frames M_{i}, but the author does not check whether this correction works yet.

References

[1] Corsi, G., and Ghilardi, S., Directed frames, Archive for Mathematical Logic 29 (1989), 53–67.

[2] Gabbay, D. M., Application of trees to intermediate logics,Journal of symbolic logic 37 (1972), 135–138.

[3] Ghilardi, S., presheaf semantics and independence results for some non-classical first-order logics, Archive for Mathematical Logic 29 (1989), 125–136.

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

[5] Isoda, E., and Shimura, T., Kripke incompleteness of some predicate extensions of modal subframe logics without finite embedding property, Bulletin of Section of Logic 27 (1998), pp. 182–189.

[6] Shimura, T., Cut-free systems for modal logics containing S4, Reports on Mathematical Logic 26 (1992), 39–65.

[7] 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.

[8] Umezawa, T., On some properties of intermediate logics, Proceedings of Japan Academy 35 (1959), 575–577.