Ming Xu

Some Normal Extensions of K4.3

Abstract. This paper proves the finite model property and the finite axiomatizability of a class of normal modal logics extending K4.3. The frames for these logics are those for K4.3, in each of which every point has a bounded number of irreflexive successors if it is after an infinite ascending chain of (not necessarily distinct) points. Keywords: Modal logic, Normal extensions of K4.3, Finite model property, Finite axiomatizability.

1.

Introduction

We present a class of normal extensions of K4.3, which have the finite model property and are finitely axiomatizable. For each n  0, let Irrf n and Zn be the following formulas:  Irrf n = 0in (q1 ∧ · · · ∧ qi ∧ qi+1 → qi+1 ) Zn = (p → p) → (3(p ∧ ∼Irrf n ) → p) and let Ln be the smallest normal extension of K4.3 containing Zn . Each modal logic of which we are to prove the finite model property and finite axiomatizability is a normal extension of an Ln with n  0. In this paper, we only deal with normal modal logics and their normal extensions, and thus for convenience, we will drop the words “normal” and “modal”, and speak of logics and their extensions. Consider the following formula Z: Z = (p → p) → (3p → p) which is discussed in [11] and [7]. The syntactical resemblance between Z and Zn is obvious, and so is the resemblance between the (Kripke) frames for Z and those for Zn . It is easy to verify that a transitive frame validates Z if for each point x in the frame, x generates an infinite ascending chain of (not necessarily distinct) points only if each successor of x has a successor

Presented by Robert Goldblatt; Received November 4, 2011

Studia Logica (2013) 101: 583–599 DOI: 10.1007/s11225-012-9398-7

c Springer Science+Business Media B.V. 2012 

584

M. Xu

in the chain. Similarly, such a frame validates Zn if for each point x in the frame, x generates an infinite ascending chain only if each successor of x either has a successor in the chain or has at most n irreflexive successors (see Proposition 2.1).1 Because in this paper we deal only with extensions of K4.3 whose rooted frames are “chains” (i.e., transitive and connected), Fine’s theorem ([6]) allows us to consider only Noetherian frames for K4.3. In accordance with what we said above, a Noetherian chain validates Z if nothing is after a nondegenerate cluster in the chain (if any), while such a chain validates Zn if each point after such a cluster (if any) has at most n irreflexive successors. It is of some interest to compare the condition on Noetherian chains for Zn just mentioned and that on the frame F∗ = W ∗ , R∗ , where W ∗ = {ω} ∪ ω and R∗ = {n, k : k, n ∈ ω and n > k} ∪ {ω, x : x ∈ W ∗ }. It is easy to see that F∗ is a Noetherian chain, but its generating point is reflexive and has infinitely many irreflexive successors, which is just the opposite of the condition that a Noetherian chain for Zn must satisfy. Not all extensions of K4.3 have the finite model property, nor are they all finitely axiomatizable. The logic of F∗ is a typical example of an extension of K4.3 without the finite model property or the finite axiomatizability.2 Among extensions of K4.3, however, some logics are shown in the literature whose extensions all have the finite model property and are all finitely axiomatizable. For example, S5 ([10]), S4.3 ([2] and [5]), K45 and K4.3 plus axioms of finite depth ([11] and [3]), G.3 (K4.3 plus (p → p) → p, [8] and [12]) and K4.3 plus Z above ([9]) etc.3 What we show here generalizes all these results, for it is easy to verify in terms of provability or frame properties that each logic mentioned above is an extension of an Ln with n  0. For example, G.3 extends L0 because Z0 is obviously provable in G.3, and S4.3 extends L0 as well because frames for S4.3 contain no irreflexive points. Section 2 provides basic notions and some preliminary work, and Sect. 3 proves the finite model property of extensions of Ln with n  0. The basic 1

It is also easy to verify that a frame validates Irrf n at a world iff the world has at most n irreflexive successors. 2 See, e.g., the discussions in p. 161 of [4] and in pp. 440–441 of [8]. 3 Although [11] does not show the finite axiomatizability of all extensions of K4.3 of finite depth, it does show their decidability. In fact, by applying a well known technique of lists, one can easily show the finite axiomatizability of all transitive logics of finite depth and finite width (see, e.g., [13]). [9] is an unpublished manuscript, which shows the finite model property and the finite axiomatizability of all normal extensions of K4.3 plus Z, and provides a syntactical characterization of these logics.

Some Normal Extensions of K4.3

585

strategy of our proof in Sect. 3 is to apply Fine’s technique of eliminating points developed in [6], combined with some ideas from [12]. In Sect. 4, we prove the finite axiomatizability of extensions of Ln with n  0, where we divide reflexive points in finite frames for Ln into finitely many segments, using irreflexive points as dividers, and repeatedly apply a well known technique of lists. In the final section, we make a few remarks about our main theorems.

2.

Preliminaries

In this paper, (modal) formulas are built from propositional variables p, q, r etc., using truth-functional connectives and . As usual, 3φ is introduced as an abbreviation of ∼∼φ. Let F = W, R be any frame. F is transitive if for all x, y, z ∈ W , Rxy and Ryz only if Rxz. F is connected if for all x, y ∈ W , either Rxy or x = y or Ryx. Let x, y ∈ W . We call y a successor of x if Rxy, and call y a proper successor of x if Rxy but not Ryx. A point x is reflexive if Rxx, and irreflexive otherwise. F is (ir -) reflexive if it contains only (ir-) reflexive points. We will speak of transitive models or connected models etc., with the understanding that their underlying frames are transitive or connected etc. Let us first show the frame condition of Zn w.r.t. transitive frames. Proposition 2.1. Let F be a transitive frame and let n  0. Then F  Zn iff for each infinite ascending R-chain x0 , x1 , . . ., and for each z such that Rx0 z, either z has at most n irreflexive successors or Rzxk for some k  1. In particular, if F is connected, F  Zn only if each proper successor of a reflexive point has at most n irreflexive successors. proof. Let x0 , x1 , . . . (not necessarily distinct) be an infinite ascending Rchain in F = W, R, and let Rx0 z. Suppose that y1 , . . . , yn+1 are distinct irreflexive successors of z, and that Rzxk for no k  1. Let M = F, V  where V is such a valuation on F that V (p) = W − {xk : k  1}, and V (qi ) = {z ∈ W : z = yi } for each i = 1, . . . , n + 1. Because Rzxk for no k  1, M, z  p. For each i = 1, . . . , n+1, M, yi  q1 ∧· · ·∧qi−1 ∧qi ∧∼qi , and then M, z  (q1 ∧ · · · ∧ qi−1 ∧ qi → qi ). It follows that M, z  p ∧ ∼Irrf n , and then M, x0  3(p ∧ ∼Irrf n ). It is routine to verify that M, x0  (p → p) ∧ ∼p, and hence M, x0  Zn . Let M be any model on F and let x0 ∈ W . Suppose that M, x0  Zn . Then M, x0  (p → p) ∧ ∼p and M, x0  3(p ∧ ∼Irrf n ). The former implies the existence of an infinite ascending chain x0 , x1 , x2 , . . . such that

586

M. Xu

M, xk  p for all k  1, while the latter implies the existence of a successor z of x0 such that M, z  p ∧ ∼Irrf n . Since M, z  p, Rzxk for no k  1, and, since M, z  ∼Irrf n , M, z  3(q1 ∧ · · · ∧ qi−1 ∧ qi ∧ ∼qi ) for every i = 1, . . . , n + 1, from which it follows that z has at least n + 1 irreflexive successors. We assume the reader’s familiarity with weak canonical models in the sense of [6]. For each nonempty set Γ of propositional variables, we use FLΓ for the set of all formulas constructed from members of Γ, using  and truth-functional connectives. The Γ-canonical model for a logic L is the weak canonical model W, R, V  for L, where W is the set of all maximal consistent sets w.r.t. L and restricted to FLΓ . We also assume the reader’s familiarity with the notions of rooted frames (models), (point-) generated subframes (submodels) and p-morphisms. Let F = W, R and F = W  , R  be frames, and let M = F, V  and  M = F , V   be models. F is a subframe of F if W  ⊆ W and R = RW  , where RW  = R ∩ (W  × W  ). M is a submodel of M if F is a subframe of F, and V  (p) = V (p) ∩ W  for every propositional variable p. If M (F ) is a submodel (subframe) of M (F), we call M (F ) the restriction of M (F) to W  . For each x ∈ W , we use W |x for the smallest subset of W that contains x and is closed under R, and use M|x for the restriction of M to W |x — the submodel of M generated by x. If M is a submodel of M that in turn is a submodel of M, we then say that M is intermediate between M of M. Let Λ be any set of formulas closed under subformulas. M is a submodel of M modulo Λ if it is a submodel of M and for each φ ∈ Λ and each x ∈ W  , M, x  φ only if M, y  φ for some y ∈ W  such that Rxy. The following is easily verifiable by a straightforward induction. Proposition 2.2. Let M = W  , R , V   be any submodel of M = W, R, V  modulo a set Λ of formulas closed under subformulas. Then for each φ ∈ Λ and each x ∈ W  , M , x  φ iff M, x  φ. For each transitive model M = W, R, V , each x ∈ W and each formula ψ, x is a final point for ψ (is final for ψ) in M if M, x  ψ and M, y  ψ for every y ∈ W such that Rxy and not Ryx. That is to say, x is final for ψ in M iff ψ is true in M at x but not at any proper successor of x. When no confusion will arise, we may drop the phrase “in M”, and simply say “x is final for ψ”. Final points for formulas are in fact the same as Fine’s noneliminable points in [6], but in the current work, associating these points with particular formulas makes it easier to distinguish certain such points from the others.

Some Normal Extensions of K4.3

587

Let Λ be any set of formulas. Λ is closed under ±-pairs of subformulas if it is closed under subformulas and contains ∼φ for every φ ∈ Λ that is not itself a negation. Each set Λ of formulas clearly has an extension that is closed under ±-pairs of subformulas, and thus we define ±Λ, the ±-closure of Λ, to be the intersection of all such extensions of Λ. It is easy to see that ±Λ is finite whenever Λ is. Let M = W, R, V  be any transitive model. M is reducible w.r.t. Λ if Λ = ∅, and for each φ ∈ ±Λ and each x ∈ W , M, x  φ only if there is a final point for φ in M|x . Clearly, M is reducible w.r.t. Λ only if it is so w.r.t. each nonempty subset of Λ. Fine’s proof has established the following.4 Proposition 2.3. Let M be any generated submodel of a weak canonical model for an extension of K4. Then M is reducible w.r.t. the set of all formulas. Provided that M is reducible w.r.t. Λ, we use WΛ for {x ∈ W : for some φ ∈ ±Λ, x is final for φ in M}, MΛ for the restriction of M to WΛ , and FΛ for the frame underlying MΛ . Proposition 2.4. Let M = W, R, V  be a transitive model reducible w.r.t. Λ, and let M = W  , R , V   be any model intermediate between MΛ and M. Then M is a submodel of M modulo ±Λ. proof. Let φ ∈ ±Λ and x ∈ W  , and suppose that M, x  φ. By hypothesis there is a y ∈ W |x that is final for ∼φ in M, and then there is a z ∈ W such that Ryz and M, z  φ. By hypothesis again, there is a z  ∈ W |z that is final for ∼φ in M, from which it follows that Rxz  , M, z   φ and z  ∈ WΛ ⊆ W  . Let M = W, R, V  be any transitive model. M is reduced if for each x ∈ W , there is a formula φ such that x is final for φ in M. For each set Λ of formulas w.r.t. which M is reducible, we call MΛ the reduced submodel of M w.r.t. Λ. When Λ is the set of all formulas, we drop the phrase “w.r.t. Λ”, and simply call MΛ the reduced submodel of M. Note that reduced submodels w.r.t. sets of formulas are indeed reduced models, as formulated below, which does not follow directly from the definitions, but is a consequence of Propositions 2.2 and 2.4. Proposition 2.5. For each transitive model M and each set Λ of formulas, M is reducible w.r.t. Λ only if MΛ is reduced. 4

See the proof of Lemma 1 in §5 of [6].

588

M. Xu

A frame F = W, R (or a model on F) is Noetherian if it is transitive and contains no infinite ascending R-chain of distinct points in W . We assume the readers’ familiarity with the notion of clusters in transitive frames. Proposition 2.6. Let M be any Noetherian model, and let Λ be any nonempty set of formulas. Then M is reducible w.r.t. Λ, and furthermore, if M is connected, then Λ is finite only if MΛ is.5 proof. The first part is straightforward. For the second part, it suffices to note that if M is connected, final points in M for the same formula must be in the same cluster, and, since M is Noetherian, each cluster contains only finitely many points. Note that by Proposition 2.6, MΛ is well defined for each Noetherian model M and each nonempty set Λ of formulas. Note also that by Proposition 2.3, the reduced submodel of M in the following theorem is well defined. Proposition 2.7. Let M be any point-generated submodel of the Γ-canonical model for an extension L of Ln , where n  0 and Γ contains at least n + 2 variables, and let M = W, R, V  be the reduced submodel of M . Then (i) if Γ is finite, W, R is a Noetherian and connected frame for L; (ii) each proper successor of a reflexive point in M has at most n irreflexive successors. proof. (i) follows directly from Fine’s theorems.6 We prove (ii) as follows. Let x be any reflexive point in M, and let z be any proper successor of x. Assume that x is final for a formula φ in M. It is then easy to verify that 3φ ∧ (∼φ → ∼φ) ∈ x and ∼φ ∈ z.

(1)

Suppose for reductio that there are distinct irreflexive successors y0 , . . . , yn of z. Then, since they are irreflexive, there are ψ0 , . . . , ψn such that ψi ∧ ∼ψi ∈ yi for all i  n, and, since they are distinct, there are χ0 , . . . , χn such that for all i, j  n with i = j, χi ∈ yi and ∼χi ∈ yj . For each i  n, let φi = ψi ∨ ∼χi . Consider any i  n. φi ∈ yi since ψi ∈ yi , and ∼φi ∈ yi since ∼ψi ∧ χi ∈ yi , and if i > 0, then for each k < i, ∼χk ∈ yi , and hence φk ∈ yi , from which it follows that φ0 ∧ · · · ∧ φi−1 ∧ φi ∧ ∼φi ∈ yi . Hence 3(φ0 ∧ · · · ∧ φi−1 ∧ φi ∧ ∼φi ) ∈ z for all i  n, and then ∼Irrf n (φ0 /q1 , . . . , φn /qn+1 ) ∈ z. Applying the second conjunct of 5 6

The conclusion still holds if we replace connectedness by the condition of finite width. See Theorem 2 in §4 and Theorem 3 in §6 of [6].

Some Normal Extensions of K4.3

589

(1), we have ∼φ ∧ ∼Irrf n (φ0 /q1 , . . . , φn /qn+1 ) ∈ z, and hence 3(∼φ ∧ ∼Irrf n (φ0 /q1 , . . . , φn /qn+1 )) ∈ x, and thus by the first conjunct of (1), Zn (∼φ/p, φ0 /q1 , . . . , φn /qn+1 ) ∈ / x, contrary to the fact that L is closed under substitution and M is a model for L.

3.

Finite Model Property

Irreflexive points in a transitive frame are of two kinds, the first of which contains those that are successors of reflexive points, and the second of which contains those that are not. Connected frames for Ln contain only finitely many irreflexive points of the first kind, but may contain infinitely many of the second. In our proof of the finite model property of extensions of Ln , we need a subframe of a connected frame F for Ln , which contains all irreflexive points in F of the first kind, and “eliminates” most, if not all, of the second kind if there are infinitely many of them. Let us deal with the second kind first. Let F = W, R be any transitive and connected frame. A segment of F is a subset X of W such that for all x, y, z ∈ W , if x, z ∈ X, and if Rxy and Ryz, then y ∈ X. An initial segment of F is a segment of F that is closed under the converse of R, and a final segment of F is a segment of F that is closed under R. A segment of F is (ir-) reflexive if it contains only (ir-) reflexive points. An (ir-) reflexive segment X of F is maximal if no proper extension of X in W is an (ir-) reflexive segment of F. We will also speak of segments of a transitive and connected model with the understanding that they are segments of the frame underlying the model. Let M be a transitive and connected model that is reducible w.r.t. Λ, and let X be the maximal irreflexive initial segment of M. An extension of MΛ w.r.t. X is the restriction of M to WΛ∗ = WΛ ∪ X. It is easy to see that such an extension of MΛ is unique, and is intermediate between MΛ and M. We will fix M∗Λ for this model, and fix F∗Λ for its underlying frame. A cluster in a transitive frame F (or a model on F) is degenerate if it contains a single irreflexive point, and nondegenerate otherwise. For all clusters c and c in a transitive frame F = W, R, c c iff Rxy for some x ∈ c and y ∈ c , and c precedes c (c ≺ c ) iff c c and c = c, and c immediately precedes c iff c ≺ c but c ≺ d ≺ c for no cluster d in F. We will use c(x) for the cluster to which x belongs. Note that each Noetherian and connected frame F has its last cluster, i.e., a cluster c such that c ≺ c for every different cluster c in F.

590

M. Xu

Lemma 3.1. Let M = W, R, V  be any Noetherian and connected model, and let Λ be any nonempty set of formulas. Then (i) both MΛ and M∗Λ are Noetherian and connected, (ii) both MΛ and M∗Λ are submodels of M modulo ±Λ, (iii) both MΛ and M∗Λ contain all points in the last cluster in M, (iv) if Λ is finite, FΛ is isomorphic to a generated subframe of F∗Λ . proof. (i) is obvious and (ii) is by Proposition 2.4. As for (iii), let c be the last cluster in M. It is easy to see that for each φ and each x ∈ c, x is final either for φ or for ∼φ, and hence, since ±Λ contains a formula and its negation, x is final for a formula in ±Λ, and hence x ∈ WΛ . We prove (iv) as follows. Let Λ be finite. Then WΛ is finite by Proposition 2.6, and hence there is a root y of MΛ . Let X be the maximal irreflexive initial segment of M, and assume that {x ∈ X : x ∈ / WΛ } = ∅ (or else there is nothing more to show). If y ∈ / X, then MΛ is a submodel of M∗Λ generated by y since Rxy for all x ∈ X. Suppose that y ∈ X. Let Y = X ∩ WΛ . Since WΛ is finite, Y is finite and nonempty. Assume that |Y | = k + 1, where |Y | is the cardinality of Y . Because Y ⊆ X ⊆ WΛ∗ , it is easy to verify by (i) that there is a final segment {x0 , . . . , xk } of X, RX  with Rxi xi+1 for all i < k. Letting W  , R  be the subframe of F∗Λ generated by x0 , we know that FΛ is isomorphic to W  , R . When we show the finite model property of an extension L of some Ln with n  0, we will construct a subframe F of a connected frame F for L, and show by way of a p-morphism that F is a frame for L. To that end, we need F to contain all irreflexive successors of some reflexive points in F, as well as some reflexive points in F immediately preceding those irreflexive ones. Let M = W, R, V  be any Noetherian, connected and reduced model, and let W0 be the set of all irreflexive successors of some reflexive points in M. Selecting a formula φx for each x ∈ W0 in such a way that x is final for φx in M, we let Λ0 = {φx : x ∈ W0 }. Clearly, W0 is finite only if Λ0 is. A cluster in M is pre-degenerate if it is nondegenerate and immediately precedes a degenerate cluster. Since M is Noetherian, it is easy to verify that W0 = ∅ iff there are pre-degenerate clusters in M. Select a point xc ∈ c for each pre-degenerate cluster c, and a formula ψy for each y ∈ W1 = {xc : c is pre-degenerate} such that y is final for ψy in M, and let Λ1 = {ψy : y ∈ W1 }. Finally, we call W0 ∪ W1 a selection of auxiliary points and call Λ0 ∪ Λ1 a selection of auxiliary formulas w.r.t. M. It is easy to see that if W0 is finite,

Some Normal Extensions of K4.3

591

so are W0 ∪ W1 and Λ0 ∪ Λ1 . Surely auxiliary points and auxiliary formulas are not uniquely determined by M because they depend on how we select them, but for our purpose, any such selection is good enough, and is as good as any other. Lemma 3.2. Let M = W, R, V  be any Noetherian, connected and reduced model, in which each reflexive point has finitely many irreflexive successors, and let Λ be any finite and nonempty set of formulas extending a selection of auxiliary formulas w.r.t. M. Then for each reflexive point x ∈ W − WΛ , there is a z ∈ WΛ such that Rxz and Rzz, and Rxy only if Rzy for all y ∈ WΛ . proof. Consider any reflexive point x ∈ W − WΛ . By Lemma 3.1, WΛ contains a point in the last cluster in M, and hence Rxy0 for some y0 ∈ WΛ . Since Λ is finite, there are by Proposition 2.6 only finitely many points y ∈ WΛ such that Rxy, and hence there must a z ∈ WΛ such that Rxz and for each y ∈ WΛ , Rxy only if either Rzy or z = y.

(2)

It then suffices to show that z is reflexive. Suppose that it is not. Then c(z) is degenerate. By hypothesis, WΛ contains all irreflexive successors of x, and then by (2), c(z) is immediately preceded by a pre-degenerate cluster c, and hence by hypothesis again, WΛ contains a reflexive point z  ∈ c. Clearly, z  = z, Rz  z and not Rzz  .

(3)

Since x ∈ / WΛ , either Rxz  or Rz  x by the connectedness of R. If Rxz  , one of (2) and (3) must fail, from which it follows that Rz  x but not Rxz  , and hence c ≺ c(x) ≺ c(z) , contrary to c immediately preceding c(z) . Let M = W, R, V  and Λ be as described in the hypothesis of Lemma 3.2. For each reflexive x ∈ W − WΛ and each z ∈ WΛ , z is closest to x if they are related as in the conclusion of Lemma 3.2, i.e., if Rxz and Rzz, and for each y ∈ WΛ , Rxy only if Rzy. Recall the extension M∗Λ (the restriction of M to WΛ∗ ) of MΛ , and its underlying frame F∗Λ , w.r.t. the maximal irreflexive initial segment of M. A function f from W to WΛ∗ is suitable if f (x) = x for all x ∈ WΛ∗ , and f assigns to each x ∈ W − WΛ∗ a z ∈ WΛ that is closest to x. It is easy to verify that each x ∈ W − WΛ∗ is reflexive, and then by Lemma 3.2, each such x has a successor in WΛ that is closest to it, and hence suitable functions from W to WΛ∗ do exist. We need to show that all such functions are p-morphisms from W, R to F∗Λ . Lemma 3.3. Let M = W, R, V  and Λ be as described in the hypothesis of Lemma 3.2, and let f be any suitable function from W to WΛ∗ . Then f is a p-morphism from W, R to F∗Λ .

592

M. Xu

proof. Let x, y ∈ W such that Rxy. Suppose that x ∈ WΛ∗ . Clearly, if y ∈ WΛ∗ , Rf (x)f (y); and if y ∈ / WΛ∗ , f (y) is closest to y, and then Ryf (y), and hence Rf (x)f (y) by the transitivity of R. Suppose that x ∈ / WΛ∗ . Then Rxf (x). If y ∈ WΛ∗ , Rf (x)y by the closest-ness of f (x) to x, and hence Rf (x)f (y) since f (y) = y. If y ∈ / WΛ∗ , then f (y) ∈ WΛ and Ryf (y), and thus Rxf (y) by the transitivity of R, and hence Rf (x)f (y) because f (x) is closest to x. Let x ∈ W and y ∈ WΛ∗ such that Rf (x)y. Clearly, x ∈ WΛ∗ only if f (x) = x, and x ∈ / WΛ∗ only if f (x) is closest to x, which implies that Rxf (x) and Rf (x)y, and hence Rxy in both cases. Theorem 3.4. Each extension of Ln with n  0 has the finite model property. proof. Let L be any extension of Ln with n  0, let φ ∈ / L, and let Γ be a finite set of propositional variables containing at least n + 2 such variables and those occurring in φ. Consider the Γ-canonical model MΓ for L. We know that ∼φ is satisfied at a root of a generated submodel of MΓ , and thus by Proposition 2.3, it is satisfied at a final point x for ∼φ in that submodel. Let M be the submodel of MΓ generated by x, and let M = W, R, V  be the reduced submodel of M . Since x is final for ∼φ in M , x ∈ W , and then by Propositions 2.2 and 2.4, M, x  φ, and, by Proposition 2.7, W, R is a Noetherian and connected frame for L. Make a selection Δ of auxiliary formulas w.r.t. M, and let Λ = {φ} ∪ Δ. We know that ±Λ is finite and by Lemma 3.1, MΛ is a submodel of M modulo ±Λ, and hence by Proposition 2.2, MΛ  φ since x is in MΛ and φ ∈ ±Λ. Furthermore, MΛ is finite by Proposition 2.6. It then suffices to show that the frame FΛ underlying MΛ is a frame for L. By Lemma 3.3, the frame F∗Λ underlying M∗Λ is a frame for L, and by Lemma 3.1, FΛ is isomorphic to a generated subframe of F∗Λ , and hence FΛ is a frame for L.

4.

Finite Axiomatizability

Consider any extension L of Ln , where n  0, and any rooted frame F for L. Because by Proposition 2.1 there are at most n irreflexive successors of a proper successor of a reflexive point, it then follows that there are at most n + 1 irreflexive successors of reflexive points in F. Let us for the moment call each such irreflexive point an “irreflexive unit”. There may also be a (nonempty) maximal irreflexive initial segment of F, which we also treat as a single “irreflexive unit”. Reflexive points in F may then be divided into at

Some Normal Extensions of K4.3

593

most n + 2 maximal “reflexive segments”, using “irreflexive units” as their dividers. Each “reflexive segment”, if not empty, is just like a frame for S4.3, from which arises our strategy to prove the finite axiomatizability of L using a standard reductio: it is just like how Fine proves the finite axiomatizability of extensions of S4.3,7 except we may have to repeat his procedure n + 2 times. For all transitive frames F = W, R and F = W  , R  that are disjoint (i.e., W ∩ W  = ∅), let F ∗ F be the sum of F and F , i.e., the frame F = W  , R , where W  = W ∪ W  and R = R ∪ R ∪ (W × W  ). For all m ∈ ω, and all pairwise disjoint transitive frames F0 , . . . , Fm+1 , let F0 ∗ · · · ∗ Fm+1 be the frame (F0 ∗ · · · ∗ Fm ) ∗ Fm+1 . It is routine to verify the following. Lemma 4.1. Let F0 , . . . , Fm and F0 , . . . , Fm be any sequences of pairwise from disjoint transitive  frames, and for each k  m, let fk be a p-morphism   Fk to Fk . Then km fk is a p-morphism from F0 ∗ · · · ∗ Fm to F0 ∗ · · · ∗ Fm . Let F be any finite, transitive and connected frame. An (initial ) segment subframe of F is a subframe X, R of F such that X is a nonempty (initial) segment of F. A segment subframe X, R of F is a (maximal ) reflexive (irreflexive) segment subframe of F if X is a (maximal) reflexive (irreflexive) segment of F. It is easy to see that there are finitely many pairwise disjoint segment subframes F0 , . . . , Fm of F such that • F = F0 ∗ · · · ∗ Fm ; • F0 is either a maximal reflexive segment subframe of F or the maximal irreflexive initial segment subframe of F; • for each i with 0 < i  m, Fi is either a maximal reflexive segment subframe of F or the restriction of F to a degenerate cluster in F. It is also easy to see that such a representation of F is unique. We will call F0 , . . . , Fm the designated components of F, or simply, the components of F. Note that each such component is either a reflexive frame or an irreflexive one, and when it is irreflexive, it is either a singleton frame or the maximal irreflexive initial segment subframe of F. Note also that if F is a frame for Ln for some n  0, there are at most n + 2 irreflexive components of F, as we said at the beginning of this section. Because there is at most one reflexive component immediately after each irreflexive component of F, it then follows that there are at most 2(n + 2) components of F. 7

See, e.g., §§3–4 of [5], or §4.9 of [1].

594

M. Xu

A list of members of a set A is a function from I to A with I to be a nonempty and finite subset of ω. We will write (ai )i∈I for such a function, where ai ∈ A, the value of the function at i ∈ I. A sublist of a list (ai )i∈I is a list (ai )i∈J for some J ⊆ I. For each list (ai )i∈I , we use length((ai )i∈I ) for the length of (ai )i∈I , i.e., length((ai )i∈I ) = |I|. When |I| = 1, we use (ai ) for (ai )i∈I , and use s, t etc. to range over lists of natural numbers. We will call (0), (0, 0), . . . 0-lists, and call lists of positive integers positive lists. Let F be a finite frame that is transitive and connected, and let c0 , . . . , ck be all the clusters in F such that for each i < k, ci immediately precedes ci+1 . For each i  k, let  |ci | if ci is nondegenerate, #(ci ) = 0 otherwise. We will call (#(ci ))ik the list associated with F. A division list is a list (si )im of lists of natural numbers satisfying the following conditions: • for each i  m, si is either a positive list or a 0-list; • for each i < m, at least one of si and si+1 is a 0-list; • for each i  m, si is a 0-list and length(si ) > 1 only if i = 0; • if m > 0 and s0 is a 0-list, then s1 is a positive list. We will use s, t etc. to range over division lists. Let F be a finite frame that is transitive and connected, let F0 , . . . , Fm be the designated components of F, and for each i  m, let si be the list associated with Fi . It is easy to verify that (si )im is a division list, and we will call it the division list associated with F. As we said earlier, if F is a frame for Ln with n  0, there are at most 2(n + 2) designated components of F, and hence, if in addition s is the division list associated with F, length(s)  2(n + 2). Let s = (ai )ik and t = (bj )jn be positive lists. t contains s iff k = n and ai  bi for all i  k. t covers s (written s  t) iff a sublist of t contains s and ak  bn . We will apply the following lemma in our upcoming discussions, which is proved in [5].8 Lemma 4.2. Let F and F be any finite, reflexive, transitive and connected frames, and let s and t be the lists associated with F and F such that s  t. Then there is a p-morphism from F to F. 8

See Lemma 6 in §4 of [5].

Some Normal Extensions of K4.3

595

Let s = (si )ik and t = (ti )in be division lists. t covers s (written s  t) iff k = n and the following hold: • either both s0 and t0 are 0-lists and length(s0 )  length(t0 ), or both are positive lists and s0  t0 ; • for each i with 0 < i  k, either si = ti = (0), or both si and ti are positive lists and si  ti . Lemma 4.3. Let F and F be any finite and connected frames for Ln , where n  0, and let s and t be the division lists associated with F and F such that s  t. Then there is a p-morphism from a generated subframe of F to F. proof. Let F = F0 ∗ · · · ∗ Fm and F = F0 ∗ · · · ∗ Fm , where F0 , . . . , Fm and F0 , . . . , Fm are the designated components of F and F respectively, and assume that s = (si )im and t = (ti )im . Let k0 , . . . , kl be all the numbers between 0 and m (inclusive) such that both ski and tki with i  l are positive lists. Clearly Fk0 , . . . , Fkl and Fk0 , . . . , Fkl are all the maximal reflexive segment subframes of F and F respectively. Then for each i  l, since ski  tki , there is by Lemma 4.2 a p-morphism fki from Fki to Fki . Consider any i  n that is distinct from all 0, k0 , . . . , kl . It is easy to see that each of Fi and Fi consists of a single irreflexive point, and thus we let fi be the function that maps the point in Fi to the one  in Fi . If both s0 and t0 are positive lists, we know by Lemma 4.1 that im fi is a p-morphism from F to F. Now suppose that both s0 and t0 are 0-lists. Then length(s0 )  length(t0 ), and it is easy to see that F0 is isomorphic to a generated subframe F0 of F0 , and thus we let f0 be the isomorphism from F0 to F0 . By Lemma 4.1,     im fi is a p-morphism from F0 ∗ F1 ∗ · · · ∗ Fm to F, and it is easy to see that F0 ∗ F1 ∗ · · · ∗ Fm is a generated subframe of F . Where I ⊆ ω, a sequence (sk )k∈I of positive lists is a -chain if for all i, j ∈ I, i < j only if si  sj , and similarly, a sequence (sk )k∈I of division lists is a -chain if for all i, j ∈ I, i < j only if si  sj . In our proof below, we will apply the following well known theorem.9 Theorem 4.4. Each countably infinite sequence of positive lists contains a countably infinite subsequence that is a -chain. Lemma 4.5. Let (sk )k∈ω be any countably infinite sequence of division lists, and let m be a fixed natural number such that length(sk )  m for all k ∈ ω. Then (sk )k∈ω contains a countably infinite subsequence that is a -chain. 9

See the corollary after Theorem 5 in §3 of [5], or Theorem 4.99 in [1].

596

M. Xu

proof. Assume that length(sk ) = m for all k ∈ ω, for otherwise there must be an infinite subsequence of (sk )k∈ω whose members are all of the same length, and we may treat (sk )k∈ω to be such a subsequence. Our proof is by induction on m. Case m = 1. Consider (sk )k∈ω where each sk is the only member of sk . There is an infinite subsequence (sk )k∈I of (sk )k∈ω such that either each sk with k ∈ I is a positive list, or each is a 0-list. In the latter case, (sk )k∈I contains an infinite subsequence (sk )k∈J such that length(sk )  length(sk ) for all k, k  ∈ J with k < k  . In the former case, (sk )k∈I contains by Theorem 4.4 an infinite subsequence that is a -chain. Hence in both cases, (sk )k∈ω contains an infinite subsequence that is a chain. Case m = n + 1. For each sk = (sk,0 , . . . , sk,n ), where sk,i is the (i + 1)-th member of sk , let tk = (sk,0 , . . . , sk,n−1 ). By induction hypothesis, (tk )k∈ω contains an infinite subsequence (tk )k∈I that is a -chain. It is easy to see that there is an infinite subsequence (sk,n )k∈J of (sk,n )k∈I such that either each sk,n with k ∈ J is a positive list, or each such sk,n is a 0-list with length(sk,n ) = 1. In the latter case, (sk )k∈J is clearly a -chain (note that each sk is tk ∗ (sk,n ), the concatenation of tk and (sk,n )). In the former case, we apply Theorem 4.4 to obtain an infinite subsequence (sk )k∈J  of (sk )k∈J , which is a -chain, and hence we obtain that (sk )k∈J  is a -chain. Applying a standard reductio, we show below the finite axiomatizability of all extensions of Ln with n  0. Theorem 4.6. Each extension of Ln with n  0 is finitely axiomatizable, and hence is decidable. proof. Suppose for reductio that an extension L of Ln with n  0 is not finitely axiomatizable. Then there is an infinite ascending ⊂-chain S0 , S1 , . . . of logics extending Ln . We know by Theorem 3.4 that all Sk with k  0 have the finite model property, and hence there is an infinite sequence F0 , F1 , . . . of finite frames such that for each k  0, Fk is a transitive and connected frame for Sk , but not for any Sm with m > k. For each k  0, let tk be the division list associated with Fk . Then (tk )k∈ω is an infinite sequence of division lists such that length(tk )  2(n + 2) for all k ∈ ω, and hence by Lemma 4.5, ti  tj for some i, j ∈ ω such that i < j. It follows from Lemma 4.3 that there is a p-morphism from a generated subframe of Fj to Fi , which makes Fi a frame for Sj , a contradiction.

Some Normal Extensions of K4.3

5.

597

Some Remarks

Let C be the class of all finite frames that are transitive and connected, and for each  n  0, let Cn be the class of all finite rooted frames for Ln . Clearly C = n0 Cn , for each frame in C contains only finitely many irreflexive points, and thus finitely many irreflexive successors of reflexive points, and hence must be a member of some Ck with k  0. Because K4.3 has the finite model property, it is then characterized by C . But it is easy to verify that the intersection of all Ln with n  0 is characterized by C as well, from which the proposition below follows.  Proposition 5.1. n0 Ln = K4.3. In light of this fact and our discussion in the introduction about some boundary results of K4.3 logics in the literature, a combination of Theorem 3.4 and Theorem 4.6 seems quite general. However, many proper extensions of K4.3 with finite model property and finite axiomatizability are not extensions of any of Ln with n  0. Let K4.3D be K4.3 plus D (i.e., 3), and let K4.3Q be K4.3 plus Q (i.e., ⊥ ∨ 3⊥), both of which have the finite model property. It is easy to verify, in terms of frame conditions, that neither K4.3D nor K4.3Q is an extension of any Ln with n  0. Another example is K4.3 plus G ∨ q ∨ (q → G) (where G = (p → p) → p), which is easily verifiable to have the finite model property but is not an extension of Ln for any n  0.10 In fact, there are uncountably many extensions of K4.3Q that have the finite model property but are not extensions of any Ln with n  0. We sketch a proof as follows. For each n  0, let Fn = Wn , Rn , where Wn = {0, . . . , n, ω} and Rn xy iff either x > y or x = y = ω.11 Note that each Fn contains a dead-end and exactly n + 1 irreflexive successors of its reflexive root, and hence it is a frame for Q and the logic of it is an extension of Ln . For each n  0, 10 Let G0 = G ∨ q ∨ (q → G). It is easy to verify that a Noetherian chain is a frame for G0 iff either it is irreflexive or it starts with a reflexive point followed by a (possibly empty) irreflexive chain. In order to see that K4.3 plus G0 has the finite model property, it suffices to note that all subframes of a Noetherian chain for the logic are frames for it. A similar example is K4.3Q plus G0 , or K4.3 plus G1 = G ∨ q ∨ ((q → G) ∧ 3⊥). One can similarly verify that a Noetherian chain is a frame for G1 iff either it is irreflexive or it starts with a reflexive point followed by a nonempty irreflexive chain. 11 These frames and related logics are briefly discussed in [8]. It is easy to see that all these frames are frames for G1 , and hence for G0 , in note 10. Thus each LI defined below is an extension of K4.3 plus G1 (G0 ).

598

M. Xu

let αn = n+1 ⊥ ∧ 3n , βn = G ∨ 3αn and γn = 3αn ∧ q → q, and let φ0 = β1 and φn = βn+1 ∨ γn−1 with n > 0. It is routine to verify the following. Proposition 5.2. For each n  0, the following hold: (i) Fn  βm for all m  n, and Fn  βk for all k > n; (ii) Fn  γm for all m  n, and Fn  γk for all k < n; (iii) Fn  φn but Fm  φn for all m ∈ ω with m = n. For each nonempty I ⊆ ω, let LI be the logic of {Fi : i ∈ I}. It is easy to verify the following by applying the proposition above. Proposition 5.3. For all nonempty I, J ⊆ ω, I = J only if LI = LJ . Thus {LI : ∅ = I ⊆ ω} is a continuum of extensions of K4.3Q. Because each such LI clearly has the finite model property, and because only countably many logics are finitely axiomatizable, we then have the following by Theorems 3.4 and 4.6. Proposition 5.4. There is a continuum of extensions of K4.3Q, each of which has the finite model property, and none of which is an extension of any of Ln with n  0. Acknowledgments. I would like to give thanks to an anonymous referee for catching some errors in an early draft of this paper and making useful suggestions to improve it. References [1] Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge Univerity Press, Cambridge, 2001. [2] Bull, R. A., That all normal extensions of S4.3 have the finite model property, Zeitschrift f¨ ur Mathematische Logik und Grundlagen der Mathematik 12:341–344, 1966. [3] Bull, R. A., and K. Segerberg, Basic modal logic, in D. Gabbay, and F. Guenthner (eds.), Handbook of Philosophical Logic, vol. 2, D. Reidel Publishing Company, Dordrecht, 1984, pp. 1–88. [4] Chagrov, A., and M. Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, Oxford, 1997. [5] Fine, K., The logics containing S4.3, Zeitschrift f¨ ur Mathematische Logik und Grundlagen der Mathematik 17:371–376, 1971. [6] Fine, K., Logics containing K4, Part I, The Journal of Symbolic Logic 39:31–42, 1974.

Some Normal Extensions of K4.3

599

[7] Goldblatt, R., Logics of Time and Computation, vol. 7 of CSLI Lecture Notes, Center for the Study of Language and Information, Stanford University, 1987. [8] Kracht, M., Tools and techniques in modal logic, vol. 142 of Studies in Logic and the Foundations of Mathematics, Elsevier Science B. V., Amsterdam, Lausanne, New York, Oxford, Shannon, Singapore and Tokyo, 1999. [9] Li, K., Normal extensions of K4.3Z, Manuscript, August 2011, Department of Philosophy, Wuhan University 2011. [10] Scroggs, S. J., Extensions of the Lewis system S5, The Journal of Symbolic Logic 16:112–120, 1951. [11] Segerberg, K., An essay in classical modal logic, Philosophical Studies published by the Philosophical Society and the Department of Philosophy, University of Uppsala, Uppsala, 1971. [12] Xu, M., Normal extensions of G.3, Theoria 68(2):170–176, 2002. [13] Xu, M., A note on the finite axiomatizability of transitive logics of finite depth and finite width, (2011). Manuscript, May 2011, Department of Philosophy, Wuhan University.

Ming Xu Department of Philosophy Wuhan University Wuhan 430072 Hubei People’s Republic of China [email protected]