ON STRONG NEIGHBOURHOOD COMPLETENESS OF MODAL AND

INTERMEDIATE PROPOSITIONAL LOGICS (Part II)^{∗}

Valentin Shehtman

Abstract

The property of strong neighbourhood completeness was introduced in the first part of this paper. By modifying the ultrabouqet construction, we prove this property for all Kripke-complete normal K4-logics and for a large class of Kripke-complete polymodal logics (called ‘acyclic). On the other hand, we present a simple counterexample of a polymodal logic with the f.m.p. which is not strongly neighbourhood complete.

Contents

1 Introduction 2 2 Ultrabouqets of transitive frames. 4 3 From K-completeness to S-N-completeness 7 4 S-N-incompleteness 9 5 Conclusion 10

∗This research was supported by the Russian Foundation for Fundamental Research

1 Introduction

This paper is a continuation of [8], but a happy occasion on which it has been written – Johan Van Benthem’s 50th birthday – suggests us to look at the topic from a more general viewpoint. Indeed, it is closely related to Correspondence Theory, a large area in modal logic discovered 25 years ago, mainly in the works of Johan Van Benthem. The original problems studied by Correspondence Theory were definability of first-order properties and classes of frames by modal formulas , cf. the introduction to [2]. But nowadays we could understand Correspondence Theory in a broader sense, as studying questions of the following two kinds:

• What features of classical first-order formulas (theories) are modal?

• What features of modal formulas (logics) are first-order and what are highorder?

Questions of the first type are considered in the recent book [1]. This paper refers to the second type; it studies a modal logic analogue of compactness.

The strong neighbourhood completeness property we are interested in, was proved in [8] for all Kripke-complete intermediate logics and for many modal logics above K4. Here we prove that Kripke-completeness implies strong neighbourhood completeness for all extensions of K4 and for all ‘acyclic’ polymodal logics. On the other hand, we construct a simple counterexample for this implication in the polymodal case.

The terminology and notations from part I are retained here with little variations. Now we consider n-modal formulas built up from the set of proposition letters P L = {p_{1}, ⋯, p_{m}, ⋯}, and the connectives ¬, ∧, □_{1}, ⋯, □_{n}; the connectives ⊃, ∨, ⊥, ◇_{i} are derived^{1} The set of all n-modal formulas is denoted by MF_{n}.

As usual, the minimal n-modal logic K_{n} is the smallest set of n-modal formulas, containing all classical tautologies, the axioms:

□_{i}(p ⊃ q) ⊃ (□_{i}p ⊃ □_{i}q),

and closed under Substitution, Modus Ponens, and □_{i}-introduction (for i ≤ n).

A set S ⊆ MF_{n} is consistent with respect to a modal logic L (or L-consistent ) if ¬(A_{1} ∧ ⋯ ∧ A_{n}) ∉ L whenever A_{1}, ⋯, A_{n} ∈ S.

An n-modal neighbourhood frame is a tuple X = (X, □_{1}, ⋯, □_{n}), where X is a non-empty set, □_{i} are unary operations on P (X) (the power set of X), satsfying the identities:

□_{i}(Y ∩ Z) = □_{i}Y ∩ □_{i}Z,
□_{i}X = X.

A neighbourhood model over X = (X, □_{1}, ⋯, □_{n}) is a pair (X , ϕ), with a mapping ϕ : P L → P (X). ϕ is extended to all modal formulas:

1We use the notations □ and ◇ (without the subscript 1) in the 1-modal case

ϕ(¬A) = X − ϕ(A), ϕ(A ∧ B) = ϕ(A) ∩ ϕ(B), ϕ(□_{i}A) = □_{i}ϕ(A).

A modal formula A is true at a point x of a model (X , ϕ) if x ∈ ϕ(A) (notation: X , ϕ, x ⊧ A; or just x ⊧ A); it is valid in X (notation: X ⊧ A) if it is true at any point of any model over X. A set of formulas S is said to be valid in X (notation: X ⊧ S) if every formula from S is valid. In this case X is said to be a (neighbourhood) S-frame . A set S is satisfied at a point x of a neighbourhood model (X , ϕ) if X , ϕ, x ⊧ A for any A ∈ S (notation: X , ϕ, x ⊧ S ); S is satisfied in X if it is satisfied in some point of some neighbourhood model over X. It is well-known that every Kripke frame F = (W, R_{1}, ⋯, R_{n}) is associated with a neighbourhood frame X (F) = (W, □_{1}, ⋯, □_{n}), where □_{i}Y = {x | R_{i}(x) ⊆ Y }; and thus Kripke semantics is reducible to neighbourhood semantics.

Recall that an n-modal logic L is neighbourhood complete (or N-complete ) if for every n-modal formula A ∉ L there exists a neighbourhood L-frame in which A is non-valid. L is neighbourhood complete (or N-complete ) if the same is true in Kripke semantics.

A class Φ of n-modal Kripke (or neighbourhood) frames determines the modal logic ML(Φ) = {A ∈ MF | ∀F ∈ Φ F ⊧ A}. A logic is K-complete iff it is determined by some class of Kripke frames; similarly, for N-completeness.

L is strongly neighbourhood (respectively, Kripke-) complete (in brief, S-N-complete; S-K-complete ) if every L-consistent set of n-modal formulas is satisfied in some neighbourhood L-frame. ^{2}

Note that every logic determined by an elementary class of frames is always S-K-complete, so the difference between these properties can be seen only in the ‘non-elementary area’.

In the most general case we have the following diagram:

S-K-completeness ⟶ K-completeness
↓  ↓
S-N-completeness ⟶ N-completeness

It is known that K-completeness does not imply S-K-completeness (cf. [8] for the references). Also it is true that S-N-completeness does not imply Kcompleteness (even for intermediate logics). This follows from [8] and [7]; the detailed proof will be published elsewhere. In this paper we show that Kcompleteness does not imply S-N-completeness in the polymodal case. On the other hand, we prove that for the monomodal logics containing K4:

S-K-completeness ⟶ K-completeness ⟶
S-N-completeness ⟶ N-completeness
(⟵?)

The question whether N-completeness implies S-N-completeness for logics above K4, remains open. However this implication can be confirmed in many cases ([8], Theorem 5.8).

2In [8] the same definitions were given also for intermediate logics. However the Definition 1.3 in [8] contains a misprint. Actually it should read as follows:

an intermediate logic L is S-N-complete if every L-consistent pair of sets of intuitionistic formulas is satisfied in some neighbourhood L-frame.

2 Ultrabouqets of transitive frames.

The main tools used in [8] in strong completeness proofs were ultrabouqets, the modal logic analogues of ultraproducts. They were defined for transitive antisymmetric (monomodal) Kripke frames (‘trantises’). Now we will extend the definition to arbitrary transitive frames.

First, let us recall that, for an ultrafilter U in ω and a statement Φ(n) of our meta-language, ∀^{∞}n Φ(n) abbreviates {n | Φ(n)} ∈ U. The “generalized quantifier ∀^{∞} distributes over all propositional connectives.

Recall also that a cluster in a transitive Kripke frame (W, R) is an equivalence class w.r.t. the relation {(x, y) | xRy ∧yRx∨x = y}; an irreflexive cluster consists of a single irreflexive point.

Consider a countable family of transitive frames F_{n} = (X_{n}, R_{n}), n ∈ ω. Assume that each F_{n} contains the least reflexive cluster C_{n}(and thus, X_{n} = R(C_{n})). Take an ultrafilter U in ω, and let C = ∏_{U} C_{n} be the corresponding ultraproduct of sets. For every sequence (a_{n})_{n∈ω} , let [a_{n}]_{n∈ω} (or, [a_{n}] in brief) be the corresponding element of C (so [a_{n}]_{n∈ω} = [b_{n}]_{n∈ω} iff ∀^{∞}n a_{n} = b_{n}). Without any loss of generality we may assume that C ∩ X_{n} = ∅ for every n. Now we glue all F_{n} together, by identifying every C_{n} with C.

Speaking precisely, let

X_{n}^{−} = X_{n} − C_{n}, X = C ∪ ⋃_{n}({n} × X_{n}^{−}).

Every a ∈ X_{n}^{−} can be identified with (n, a) ∈ X; so we can consider X_{n}^{−} as a subset of X. Let R be the relation in X such that

(m, x)R(n, y) ⇔ m = n & xR_{n}y; R(C) = X.

Then obviously, R is transitive.

For any V ⊆ X let

□V = V_{1} ∪ V_{0},

where

V_{1} = {x | x ∉ C & R(x) ⊆ V },

V_{0} = \{ \begin{matrix}\{u\}, & if ∀^{∞}n X_{n}^{−} ⊆ V and C ⊆ V; \\ ∅ & otherwise. \end{matrix}

Similarly to [8], Lemma 2.4 one can show that (X, □) is a neighbourhood K4frame.

Definition 2.1 The neighbourhood frame (X, □) defined above is called the ultrabouqet of the family (F_{n})_{n∈ω} w.r.t. the ultrafilter U and denoted by ⋁_{U} F_{n} .

Definition 2.2 In the above context, let ψ_{n} be a valuation in F_{n} = (X_{n}, R_{n}), ψ be a valuation in (X, □) = ⋁_{U} F_{n} such that for any proposition letter p,

∀n ψ(p) ∩ X_{n}^{−} = ψ_{n}(p) ∩ X_{n}^{−};
[c_{n}] ∈ ψ(p) ⇔ ∀^{∞}n c_{n} ∈ ψ_{n}(p).

Then ψ is called the ultrabouqet of the family (ψ_{n})_{n∈ω} and denoted by ⋁_{U} ψ_{n}.

It is easily checked that the family (ψ_{n}) uniquely defines ψ.

Lemma 2.3 Let ψ_{n} , F_{n} be the same as in the previous Definition, and let ψ = ⋁_{U} ψ_{n}. Then for any modal formula A,

(1) ∀n ψ(A) ∩ X_{n}^{−} = ψ_{n}(A) ∩ X_{n}^{−};

(2) [c_{n}] ∈ ψ(A) ⇔ ∀^{∞}n c_{n} ∈ ψ_{n}(A).

PROOF. By induction, similar to [8], Lemma 2.8. Let us consider the case A = □B in (2).

[c_{n}] ∈ ψ(□B) ⇔ C ⊆ □ψ(B) ⇔ C ⊆ ψ(B) & ∀^{∞}n X_{n}^{−} ⊆ ψ(B)
⇔ C ⊆ ψ(B) & ∀^{∞}n X_{n}^{−} ⊆ ψ_{n}(B).

Also

C ⊆ ψ(B) ⇔ ∀^{∞}n C_{n} ⊆ ψ_{n}(B).

In fact, assume that C ⊆ ψ(B), but not ∀^{∞}n C_{n} ⊆ ψ_{n}(B). Then ∀^{∞}n C_{n} ⊈ ψ_{n}(B), and thus there exists a sequence of d_{n} ∈ C_{n} such that ∀^{∞}n d_{n} ∉ ψ_{n}(B) (for, take an element in (C_{n} − ψ_{n}(B)) whenever this set is nonempty; otherwise take an arbitrary element in C_{n}). By the inductive hypothesis we obtain that [d_{n}] ∉ ψ(B), in a contradiction with C ⊆ ψ(B). So we have

[c_{n}] ∈ ψ(□B) ⇔ ∀^{∞}n C_{n} ⊆ ψ_{n}(B) & ∀^{∞}n X_{n}^{−} ⊆ ψ_{n}(B) ⇔ ∀^{∞}n C_{n} ⊆ ψ_{n}(□B)

⇔ ∀^{∞}n c_{n} ∈ ψ_{n}(□B). ⊣

Lemma 2.4 Let A be a modal formula, F_{n} = (X_{n}, R_{n}), n ∈ ω be K4 -frames validating A. Assume that each F_{n} contains the least reflexive cluster C_{n}. Then A is valid in any ultrabouqet ⋁_{U} F_{n}.

PROOF. Suppose the contrary, i.e. that φ(A) ≠ X, for some valuation φ in (X, □) = ⋁_{U} F_{n} . If X_{n}^{−} − φ(A) ≠ ∅ for some n, then the generated subframe argument shows that A is non-valid in F_{n}. Thus c_{1} ∉ φ(A) for some c_{1} ∈ C. Let p_{1}, ⋯, p_{m} be the list of all proposition letters occurring in A, and consider the following equivalence relation in C:

x ≡_{0} y ⇔ ∀i ≤ m (x ∈ φ(p_{i}) ⇔ y ∈ φ(p_{i})).

First let us assume that

(X, □), φ, c_{1} ⊧ ¬p_{1} ∧ ⋯ ∧ ¬p_{m}.  (1)

Let c_{1}, ⋯, c_{k} be the maximal set of non-equivalent points in C (w.r.t ≡_{0}). Consider the valuation ψ in X, such that for every q ∈ P L

x ∈ ψ(q) ⇔ x ∈ φ(q), if x ∈ (X − C) ∪ {c_{1}, ⋯, c_{k}};
x ∉ ψ(q), if x ∈ C − {c_{1}, ⋯, c_{k}}.

For every c_{i} choose a sequence (c_{in})_{n∈ω} , such that c_{i} = [c_{in}]_{n∈ω} , and take the valuations ψ_{n} in F_{n} such that for every q

ψ_{n}(q) ∩ C_{n} = {c_{in} | c_{i} ∈ φ(q)}, ψ_{n}(q) ∩ X_{n}^{−} = ψ(q) ∩ X_{n}^{−}.

Then we have:

[a_{n}] ∈ ψ(q) ⇔ ∀^{∞}n a_{n} ∈ ψ_{n}(q).  (2)

In fact, by the definition of ψ, ψ_{n} and the properties of ∀^{∞},

∀^{∞}n a_{n} ∈ ψ_{n}(q) ⇔ ∀^{∞}n (a_{n} = c_{1n} & c_{1} ∈ ψ(q) ∨ ⋯ ∨ a_{n} = c_{kn} & c_{k} ∈ ψ(q))

⇔ ∀^{∞}n (a_{n} = c_{1n} & c_{1} ∈ ψ(q)) ∨ ⋯ ∨ ∀^{∞}n (a_{n} = c_{kn} & c_{k} ∈ ψ(q))
⇔ ∃i ≤ k([a_{n}] = c_{i} & c_{i} ∈ ψ(q)) ⇔ [a_{n}] ∈ ψ(q).
c_{1} ∉ ψ(A) ⇒ ∀^{∞}n F_{n}|̸=A.  (3)

For, ψ = ⋁_{U} ψ_{n} by (1), and thus c_{1} ∉ ψ(A) implies ∀^{∞}n c_{1n} ∉ ψ_{n}(A) by Lemma 2.3.

c_{1} ∉ ψ(A).  (4)

To verify this, we show by induction that for any formula E in p_{1}, ⋯, p_{m}

∀i ≤ k (c_{i} ∈ ψ(E) ⇔ c_{i} ∈ φ(E)).  (5)

Only the case E = □B is non-trivial. We have

c_{i} ∈ ψ(□B) ⇔ C ⊆ ψ(B) & ∀^{∞}n X_{n}^{−} ⊆ ψ(B) ⇔ C ⊆ ψ(B) & ∀^{∞}n X_{n}^{−} ⊆ φ(B),

due to the definition of φ . Now it suffices to prove

C ⊆ ψ(B) ⇔ C ⊆ φ(B).  (6)

(⇒ ) Let C ⊆ ψ(B). Then c_{1}, ⋯, c_{k} ∈ φ(B) by (5), and also d ∈ φ(B) for every d ∈ C − {c_{1}, ⋯, c_{k}}. For, by the choice of c_{1}, ⋯, c_{k} , we have d ≡_{0} c_{i} for some i, and an easy inductive argument shows that (w.r.t. the valuation φ ) the same formulas in p_{1}, ⋯, p_{m} are true in d, c_{i} .

(⇐) Let C ⊆ φ(B). Then c_{1}, ⋯, c_{k} ∈ ψ(B) by (5), and again, d ∈ ψ(B) for every d ∈ C − {c_{1}, ⋯, c_{k}}. In fact, d ∉ ψ(p_{j}) for j ≤ m, and thus (w.r.t the valuation ψ and formulas in p_{1}, ⋯, p_{m}), d is equivalent to c_{1} .

This completes the proof of (6) and (5). Now c_{1} ∉ φ(A) implies (4), and from (4) , (3) we get ∀^{∞}n F_{n}|̸=A, which contradicts the assumption of the Lemma. Therefore (1) is impossible.

Now instead of (1), let us assume that

(X, □), φ, c_{1} ⊧ ¬p′_{1} ∧ ⋯ ∧ ¬p′_{m},

where each p′_{j} is either p_{j} or ¬p_{j}. Take the valuation φ′, such that for every j ≤ m, φ′(p_{j}) = φ(p′_{j}); then obviously, φ′(p′_{j}) = φ(p_{j}); and hence

φ(A(p_{1}, ⋯, p_{m})) = φ′(A(p′_{1}, ⋯, p′_{m})).

Now we have that A′ = A(p′_{1}, ⋯, p′_{m}) is valid in every F_{n} , and also

c_{1} ∉ φ′(A′); (X, □), φ′, c_{1} ⊧ ¬p_{1} ∧ ⋯ ∧ ¬p_{m},

and so the previous argument leads us to a contradiction again. Therefore φ(A) = X. ⊣

3 From K-completeness to S-N-completeness

Theorem 3.1 Every K-complete monomodal logic containing K4 is S-N-complete.

PROOF. Similar to [8], Theorem 3.3. Suppose L = ML(Φ) for a class Φ of transitive 1-modal Kripke frames. Consider an L-consistent countable set of formulas S = {A_{n} | n ∈ ω} , then every formula B_{n} = ⋀_{i=0}^{n} A_{i} is Lconsistent, and thus there exists a frame F_{n} ∈ Φ and a valuation ϕ_{n} , such that F_{n}, ϕ_{n}, x_{n} ⊧ B_{n} . Obviously, (B_{n} ⊃ B_{m}) ∈ K4 if m ≤ n. Now there are two cases.

(i) The set {n | x_{n} is reflexive } is infinite.

Let {n_{1}, n_{1}, ⋯, } be the increasing enumeration of this set; then n_{k} ≥ k. Also let y_{k} = x_{n_{k}}, and let (X_{k}, ψ_{k}) be the submodel of (F_{n_{k}}, ϕ_{n_{k}}) generated by y_{k}. By the properties of generated subframes, we have

X_{k} ⊧ L and X_{k}, ψ_{k}, y_{k} ⊧ B_{n_{k}}; hence X_{k}, ψ_{k}, y_{k} ⊧ B_{k}(because n_{k} ≥ k).

Take some non-principal ultrafilter U in ω, and consider the ultrabouqet X = ⋁_{U} X_{n} . Then X ⊧ L, by Lemma 2.4.

On the other hand, take the valuation ψ = ⋁_{U} ψ_{n} . Since we have X_{n}, ψ_{n}, y_{n} ⊧ C_{n} , it follows that (for any k)

∀n ≥ k y_{n} ∈ ψ_{n}(A_{k}),

and thus

∀^{∞}n y_{n} ∈ ψ_{n}(A_{k}),

because U is non-principal. Then by Lemma 2.3, [y_{n}] ∈ ψ(A_{k}), and therefore X, ψ, [y_{n}] ⊧ S.

(ii) The set {n | x_{n} is reflexive} is finite. Then the set {n | x_{n} is irreflexive} is infinite, and we may use the same argument as in the proof of Theorem 3.3 from [8]. ⊣

Definition 3.2 A cycle of length m > 1 in a Kripke frame F = (W, R_{1}, ⋯, R_{l}) is a sequence of distinct points x_{1}, ⋯, x_{m} such that x_{1}Rx_{2}R ⋯ Rx_{m−1}Rx_{m}Rx_{1}, where R = R_{1} ∪ ⋯ ∪ R_{l}. A Kripke frame without cycles is called acyclic .

Definition 3.3 A reflexifity type of a point x in a Kripke frame F = (W, R_{1}, ⋯, R_{l}) is the set rt(x) = {i | xR_{i}x}.

Definition 3.4 For every n ∈ ω, let F_{n} = (X_{n}, R_{n1}, ⋯, R_{nl}) be an acyclic generated frame with a root x_{n}, and assume that all the x_{n} are of the same reflexivity type. The bouqet of the frames F_{n} is the frame (X, R_{1}, ⋯, R_{l}), where

X = {u} ∪ ⋃_{n}({n} × X_{n}^{−}), X_{n}^{−} = X_{n} − {x_{n}}, u ∉ ⋃_{n} X_{n},

(m, x)R_{i}(n, y) ⇔ m = n & xR_{ni}y; uR_{i}(n, y) ⇔ x_{n}R_{ni}y; rt(u) = rt(x_{1}).

As usual, X_{n}^{−} is identified with ({n} × X_{n}^{−}).

For an ultrafilter U in ω, we define the ultrabouqet ⋁_{U} F_{n} as the neighbourhood frame (X, □_{1}, ⋯, □_{l}), where

□_{j}V = V_{j}^{0} ∪ V_{j}^{1},
V_{j}^{1} = {x | x ≠ u & R_{j}(x) ⊆ V },

V_{j}^{0} = \{ \begin{matrix}\{u\}, & if ∀^{∞}n R_{nj}(x_{n}) − \{x_{n}\} ⊆ V ( and also u ∈ V if uR_{j}u) \\ ∅ & otherwise. \end{matrix}

Definition 3.5 Let F_{n} be the same as in the previous Definition, and for every n, let ψ_{n} be a valuation in F_{n}. We define the valuation ψ = ⋁_{U} ψ_{n} in ⋁_{U} F_{n} such that for any proposition letter p,

∀n ψ(p) ∩ X_{n}^{−} = ψ_{n}(p) ∩ X_{n}^{−};
u ∈ ψ(p) ⇔ ∀^{∞}n x_{n} ∈ ψ_{n}(p).

The following two lemmas are quite similar to the case considered in [8]:

Lemma 3.6 Let ψ = ⋁_{U} ψ_{n}. Then for any l-modal formula A, (1) ∀n ψ(A) ∩ X_{n}^{−} = ψ_{n}(A) ∩ X_{n}^{−} ;

(2) u ∈ ψ(A) ⇔ ∀^{∞}n x_{n} ∈ ψ_{n}(A).

Lemma 3.7 In the assumptions of Definition 3.5, let A be an l-modal formula which is valid in every F_{n}. Then A is valid in any ultrabouqet ⋁_{U} F_{n}.

Theorem 3.8 Every modal logic determined by a class of acyclic Kripke frames is S-N-complete.

PROOF. Similar to Theorem 3.3 from [8] and to Theorem 3.1 above. Suppose L = ML(Φ) for a class Φ of acyclic Kripke frames. Consider an L-consistent countable set of formulas S = {A_{n} | n ∈ ω}. For B_{n} = ⋀_{i=0}^{n} A_{i} there exists a frame F_{n} ∈ Φ and a valuation ϕ_{n} , such that F_{n}, ϕ_{n}, x_{n} ⊧ B_{n} . Then some reflexivity type is represented by infinitely many of x_{n}. Let n_{1}, n_{2}, ⋯ be the increasing enumeration of these numbers n, and let (X_{k}, ψ_{k}) be the submodel of (F_{n_{k}}, ϕ_{n_{k}}) generated by y_{k} = x_{n_{k}}. For a non-principal ultrafilter U in ω, consider the ultrabouqet X = ⋁_{U} X_{n} and the valuation ψ = ⋁_{U} ψ_{n}. Then X ⊧ L, by Lemma 3.7, and X, ψ, u ⊧ S by Lemma 3.6. ⊣

Corollary 3.9 Every uniform logic (in the sense of [5]) containing D is S-N-complete.

PROOF. The normal form construction from [5] (cf. also [3]) shows that every uniform logic above D is determined by a class of finite acyclic frames. ⊣

In particular, the famous logic M = K+□◇p ⊃ ◇□p which is “very secondorder” in Kripke semantics [2], becomes better in neighbourhood semantics.

4 S-N-incompleteness

Now let us construct a rather natural bimodal logic which is K-complete, but S-N-incomplete. Consider the formula AGrz = ¬(p∧□(p ⊃ ◇(¬p∧◇p)). Then Grz = S4 + AGrz is the well-known Grzegorczyk’s logic , determined by the class of all finite partial orders [3].

Definition 4.1 Let GrzU be Grzegorczyk’s logic with the universal modality. It is defined as the logic with modal operators □, ∀, and the following postulates:

(1) postulates of Grz for □;

(2) postulates of S5 for ∀ ;

(3) ∀p ⊃ □p.

Theorem 4.2 GrzU has the f.m.p (and therefore is K-complete).

PROOF. Take a generated submodel M = (W, R_{1}, R_{2}, φ) of the canonical model refuting a given formula A. Due to the axioms (2) and (3), the relation R_{2} is universal. Then we extract a finite submodel of M refuting A by a standrad filtration argument in the same way as it is done for Grz. ⊣

To show that GrzU is S-N-incomplete we use the well-known K. Fines frame F F from [4]. The whole argument is close to Sec. 2 of [7], so we do not give it in full detail here.

Definition 4.3 By induction we define the formulas β_{n}, γ_{n} :

β_{0} = □p, γ_{0} = □¬p, β_{1} = ¬p ∧ ◇β_{0} ∧ ¬◇γ_{0}, γ_{1} = p ∧ ¬◇β_{0} ∧ ◇γ_{0},

β_{n+1} = ◇β_{n} ∧ ◇γ_{n−1} ∧ ¬◇γ_{n}, β_{n+1} = ◇γ_{n} ∧ ◇β_{n−1} ∧ ¬◇β_{n} (for n ≥ 1).

Let α_{n} = ◇β_{n+1} ∧ ◇γ_{n+1} ∧ ¬◇γ_{n+2} ∧ ¬◇β_{n+2}, ϵ_{n} = ◇α_{n} ∧ ◇β_{n+2},

lprθ_{n} = ϵ_{n+1} ∧ ¬◇α_{n}, δ_{n} = ϵ_{n} ⊃ ◇θ_{n}.

Let S = {ϵ_{0}} ∪ {∀δ_{n} | n ∈ ω}.

Definition 4.4 Let F F = (W, ≤), where W = ⋃_{n}{a_{n}, b_{n}, c_{n}, d_{n}}, ≤ is the least partial order in W, such that

b_{n+1} ≤ b_{n}, c_{n−1}; c_{n+1} ≤ c_{n}, b_{n−1}; a_{n} ≤ b_{n+1}, c_{n+1}; d_{n} ≤ a_{n}, d_{n+1}.

Let F F_{n} be the restriction of F F to the set V_{n} = W − {d_{m} | m > n}.

Lemma 4.5 The set S is GrzU-consistent.

PROOF. We will show that every set S_{n} = {ϵ_{0}} ∪ {∀δ_{m} | m ≤ n} is GrzUconsistent. Since every ascending chain in F F_{n} is finite, the logic GrzU is valid in F F_{n} with ∀ interpreted as the universal truth. So it is sufficient to show that S_{n} is satisfied in some Kripke model over F F_{n}. Take the valuation φ in V_{n}, such that φ(p) = {b_{0}, c_{1}}. Then by induction on k it follows that φ(β_{k}) = {b_{k}}, φ(γ_{k}) = {c_{k}}. This implies φ(α_{k}) = {a_{k}}, and thus d_{0} ∈ φ(ϵ_{0}). Also φ(δ_{m}) = V_{n}. For, x ∈ φ(ϵ_{m}) implies x ≤ a_{m}, x ≤ b_{m+2}, and thus x ≤ d_{m}. But d_{m+1} ≤ a_{m+1}, b_{m+3}, c_{m+3}; d_{m+1} ≰ a_{m}; therefore d_{m+1} ∈ φ(θ_{m}), x ∈ φ(◇θ_{m}). So we obtain that the formulas ∀δ_{m} are true in (F F_{n}, φ) whenever m ≤ n, and thus (F F_{n}, φ), d_{0} ⊧ S_{n}. ⊣

Lemma 4.6 S is not satisfied in any neghbourhood frame validating GrzU.

PROOF. Suppose the contrary, and let X be a neighbourhood GrzU-frame satisfying S. Due to the postulates (2), (3) of GrzU, X is isomorphic to a disjoint union of topological spaces X_{i} , such that □ is interpreted in X_{i} as the interior operator, and ∀ as the universal truth. So without any loss of generality, we may assume that X is one of those X_{i} .

Then φ(ϵ_{0}) ≠ ∅, φ(∀δ_{n}) = X, for some valuation φ in X. Let X_{0} = φ(ϵ_{0}), X_{n} = φ(θ_{n}) for n > 0. Then X_{n} ⊆ φ(ϵ_{n+1}) ⊆ ◇W_{n+1} (since by our assumption φ(δ_{n+1}) = X). Also X_{n} ∩ X_{n+1} = ∅, since X_{n} ⊆ φ(ϵ_{n+1}) ⊆ φ(◇α_{n+1}), X_{n+1} ⊆ φ(ϵ_{n+1}) − φ(◇α_{n+1}).

Now it follows that AGrz is refuted in X. In fact, let Y be a subspace of X on the set Y = ⋃_{n∈ω} X_{n}. For y ∈ Y, let μ(y) = min{n | y ∈ X_{n}}.

Let η(y) be μ(y) modulo 2. Then η is an interior mappping from Y onto the set {0, 1} with the weakest topology (i.e. onto the neighbourhood frame of a two-element cluster). To prove this, it is sufficient to show that the subsets Y_{0} = η^{−1}(0), Y_{1} = η^{−1}(1) are dense in Y. For the latter, we check by induction on n, that

∀n∀x ∈ Y (μ(x) = n ⇒ x ∈ ◇Y_{0} ∩ ◇Y_{1}).

In fact, assume this for every k < n, and let μ(x) = n; then x ∈ X_{n} ⊆ ◇X_{n+1}. Let V be any neighbourhood of x; take a point y ∈ X_{n+1} ∩ V. Assume that n is even. Then x ∈ Y_{0}, V ∩ Y_{0} ≠ ∅. Since X_{n} ∩ X_{n+1} = ∅, we have either μ(y) = n + 1 ( and thus, y ∈ Y_{1} ∩ V), or μ(y) = n + 1 (and thus y ∈ ◇Y_{1} by the inductive hypothesis, and again Y_{1} ∩ V ≠ ∅). The case when n is odd is quite similar. Since η is interior and the formula AGrz is refuted in the two-element cluster, it is refuted in Y. Therefore it is refuted also in X , because the validity of AGrz is preserved by any (not necessarily open) subspace. ⊣

Theorem 4.7 The logic GrzU is S-N-incomplete.

PROOF. From 4.4. and 4.5. ⊣

5 Conclusion

The results obtained in this paper show the crucial difference between the neighbourhood and Kripke semantics. In fact, it turns out that in neighbourhood semantics, modal logics enjoy the compactness property in numerous cases, and thus they acquire features of classical first order theories. On the other hand, in Kripke semantics modal logics are known to behave like second order theories, because such properties as compactness, Löwenheim – Skolem etc. fail too often.

Another important point is the difference between the transitive and the general case. Although the counterexample in Section 4 is bimodal, it is very likely to be reformulated as monomodal, by using Thomason’s translations [9], [10], [6]. But it in the transitive case such counterexamples are impossible, due to Theorem 3.1. This leads us again to an old question:

Does there exist a Thomason-style translation from polymodal logics (and consequently, from classical second-order logic[11]) to monomodal K4-logics?

A common opinion among modal logicians has been that this question has an answer ‘yes’. However the previous observations seem to point at the answer ‘no’.

References

[1] J. VAN BENTHEM. Exploring logical dynamics. CSLI publications, 1996.

[2] J. VAN BENTHEM. Modal logic and classical logic. Bibliopolis, 1983.

[3] A. CHAGROV, M.ZAKHARYASCHEV. Modal logic. Oxford University Press, 1996.

[4] K. FINE, An incomplete logic containing S4, Theoria,v.40 (1974), No.1, 23- 29.

[5] K. FINE. Normal forms in modal logic. Notre Dame Journ. of Formal Logic, 16:(2), pp. 229–237, 1975.

[6] M.KRACHT, F.WOLTER. Normal modal logics can simulate all others. Journal of Symbolic Logic, to appear.

[7] V.B.SHEHTMAN. Topological models of propositional logics. Semiotika i Informatika, 1980, No.15,74-98. (In Russian)

[8] V. SHEHTMAN. On strong neighbourhood completeness of modal and intermediate propositional logics (part I). In: Advances in Modal Logic 96. M.Kracht, M. de Rijke, H. Wansing, M. Zakharyaschev, eds. CSLI Publications, 1997, pp. 209-222.

[9] S.K.THOMASON. Reduction of tense logic to modal logic. I. Journal of Symbolic Logic, v. 39 (1974), 549–551.

[10] S.K.THOMASON. Reduction of tense logic to modal logic. II. Theoria, v. 41 (1975), 154–169.

[11] S.K.THOMASON. Reduction of second-order logic to modal logic. Zeitschrift f. math. Logik und Grundlagen der Mathematik, v. 21 (1975), 107–114.