Kripke incompleteness of predicate extentions of Gabbay-de Jongh’s logic of the finite binary trees.

Tatsuya SHIMURA

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

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

1 Introduction.

In the previous papers [4, 5], the author gave several completeness and incompleteness results on some predicate extensions with the constant domain of intermediate and modal propositional logics by means of the theory of canonical formulas (cf. [1]).

However, these results are on subframe and cofinal subframe logics, and little is known for non cofinal subframe logics.

In this note, we show the Kripke incompleteness of the intermediate predicate logic H_{∗} +Tr_{2} +K +D, where Tr_{2} is the axiom of Gabbay-de Jongh’s logic of the finite binary trees [2] ⋀_{i=0}^{2}((p_{i} ⊃ ⋁_{j≠i} p_{j}) ⊃ ⋁_{j≠i} p_{j}) ⊃ ⋁_{i=0}^{2} p_{i}, K is Kuroda’s axiom ∀x¬¬A(x) ⊃ ¬¬∀xA(x) and D is the axiom of constant domain ∀x(A(x) ∨ B) ⊃ (∀xA(x) ∨ B).

Our result is the following.

Theorem 1 Let L be an intermediate logic with the following conditions:

• L is Kripke complete.

• L is contained in H_{∗} + Tr_{2} + K + D.

Then, the propositional part of L is the intuitionistic logic.

To prove the theorem, we construct a Kripke model ⟨T̂, D, ⊧⟩ and a formula A satisfying the following three conditions:

(i). Every instance of Tr_{2}, K and D is true in ⟨T̂, D, ⊧⟩.

(ii). A cannot be separated from H_{∗} + Tr_{2} + K + D by Kripke frames, that is, A is valid in the Kripke frames for H_{∗} + Tr_{2} + K + D.

(iii). A is refuted in ⟨T̂, D, ⊧⟩.

2 Outline of the proof.

It is known that Gabbay-de Jongh’s logic H + Tr_{2} is complete but not strongly complete. This fact is implicitely showed in [3]. Another proof is given in [1, Theorem 6.2].

Since the expressive power of predicate logics is stronger than that of propositional logics, it may be possible to transfer the proof of the non-strong completeness [1, Theorem 6.2] to an incompleteness proof of predicate extensions of H + Tr_{2}.

2^{≤ω} denotes the 0-1 sequences of length at most ω and 2^{<ω} denotes the finite 0-1 sequences. lh(s) denotes the length of s ∈ 2^{<ω}.

We denote s ⊆ t if s ∈ 2^{ω} is an initial segment of t ∈ 2^{≤ω}. s ⊊ t is the abbreviation of s ⊆ t and s ≠ t. For s ∈ 2^{<ω} and t ∈ 2^{≤ω}, s∗t denotes the concatenation of s and t. For s ∈ 2^{≤ω} and n, s|n denotes the initial segment of length n of s.

We define partially ordered sets T, T̂ and T_{n} as follows:

T = 2^{<ω}, T = ⟨T, ⊆⟩; T̂ = 2^{≤ω}, T̂ = ⟨T̂, ⊆⟩, T_{n} = ⟨2^{≤n}, ⊆⟩.

The proof of the non-strong completeness [1, Theorem 6.2] used the fact that every instance of Tr_{2} is true in the Kripke model for propositional logic ⟨T̂, ⊧⟩ defined by s ⊧ p_{t} ⇔ t ⊊ s, where p_{t} (t ∈ 2^{<ω}) are propositional variables.

So, we define the Kripke model ⟨T̂, D, ⊧⟩ as follows:

• D = 2^{<ω},

• s ⊧ p(t) ⇔ t ⊊ s.

As we have expected, we can prove the following.

Lemma 1 Quantifier elimination holds in the model ⟨T̂, D, ⊧⟩. More precisely, for every formula A, there exist constants t_{1}, t_{2}, dots, t_{n} ∈ D such that

⟨⟩ ⊧ A ≡ (p(t_{1}) ∨ p(t_{2}) ∨ ⋯ ∨ p(t_{n})).

Since the axioms K and D are valid in frame ⟨T̂, D⟩, the above lemma implies the condition (i).

We define the formula A as follows:

P = ∀x((¬¬p(x) ⊃ p(x)) ⊃ (p(x) ∨ ¬p(x)))
Q_{1}(x, y, z) = p(x) ≡ (¬¬p(y) ∨ ¬¬p(z))
Q_{2}(y, z) = ¬(¬¬p(y) ∧ ¬¬p(z))
Q_{3}(x, y) = (¬¬p(y) ⊃ p(y)) ⊃ (¬¬p(x) ⊃ p(x))
A = (P ∧ ∀x∃y, z(Q_{1}(x, y, z) ∧ Q_{2}(y, z) ∧ Q_{3}(x, y) ∧ Q_{3}(x, z))) ⊃ ∀x(¬¬p(x) ⊃ p(x))

It is not difficult to verify the condition (iii).

Lemma 2 A is refuted at ⟨⟩ in ⟨T̂, D, ⊧⟩.

So, the rest is to show the condition (ii). Suppose A is refuted in a Kripke model ⟨N, U, ⊧⟩. Without loss of generality, we may assume A is

refuted at the least element 0 of N.

By induction on the length of s, we can choose x_{s} ∈ U(0) (s ∈ T) and u_{s} (s ∈ T) such that

u_{s} ⊧ ¬¬p(x_{s}), u_{s} |̸= p(x_{s})
0 ⊧ Q_{1}(x_{s}, x_{s∗⟨0⟩}, x_{s∗⟨1⟩}) ∧ Q_{2}(x_{s∗⟨0⟩}, x_{s∗⟨1⟩}) ∧ Q_{3}(x_{s}, x_{s∗⟨0⟩}) ∧ Q_{3}(x_{s}, x_{s∗⟨1⟩}).

It can be proved the partial map

f(u) = \{ \begin{matrix}s & u = u_{s} \\ undefined & otherwise \end{matrix}

is a subreduction from N to T.

We can extend f to a total map g from N to T̂ with the following conditions.

• g is order preserving.

• The restriction of g to g^{−1}(T) is a p-morphism from g^{−1}(T) to T.

By the above conditions, we can prove that N characterizes the intuitionistic logic H.

Lemma 3 (cf. Smoryński [6]) Suppose A is refuted in a Kripke model ⟨N, U, ⊧⟩.

Every finite frame is a p-morphic image of N. So, N characterizes intH.

3 Remarks.

We can consider several problems.

One interpretation of our theorem is that we have not known a good axiom to complete Gabbayde Jongh’s logic. There is a complete intermediate logic H_{∗} + Tr_{2} + (p ∨ ¬p) ∨ ∃x∀y(A(x) ≡ A(y)) whose propositional part is H + Tr_{2}. Since this logic is almost a propositional logic, it is natural to ask the following.

Problem 1 Find a non-trivial finitely axiomatizable intermediate predicate logic whose propositional part is Gabbay-de Jongh’s logic.

Our incompleteness proof heavily depends on the fact that the propositional part is Gababy-de Jongh’s logic.

Problem 2 Reformulate our result by means of canonical formulas.

The problem is to change the propositional part.

Problem 3 Let J be a Kripke complete intermediate logic. Determin J_{∗} + K + D is complete or not. In particular, how about the following cases.

• J is Scott’s logic.

• J is Kreisel-Putman’s logic.

Since Scott’s logic is not strongly complete, it may be possible to apply the similar technique to Gabbay-de Jongh’s logic. However, the problem is much difficult for Kreisel-Putman’s logic since Kreisel-Putman’s logic is elementary.

References

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

[2] D.M. Gabbay, and D.H. de Jongh, Sequences of decidable and finitely axiomatizable intermediate logics with the disjunction property, Journal of Symbolic Logic 39 (1974), pp. 67-79.

[3] V.B. Shehtman On incomplete propositional logics, Doklady Akademii Nauk SSSR 235 (1977), 542-545. (English translation) Soviet Mathematics, Doklady 18 (1977), 985-989.

[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] T. Shimura, 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] C. Smorynski, Investigations of Intuitionistic Formal Systems by Means of Kripke Models, Thesis, University of Illinois.