128

Part II

Kripke semantics

Proceeding to the systematic study of superintuitionistic and modal logics, first of all we are interested in finding good semantic instruments. For the beginning, let us try to manage with what we already have, namely, Kripke frames and models. So the main questions we address in this part are whether logics in ExtInt and NExtK are characterized by suitable classes of Kripke frames and whether they are finitely approximable. We begin with generalizing the completeness proofs of Sections 2.6 and 3.6 and show that this approach works for a good many logics.

CANONICAL MODELS AND FILTRATION

In this chapter we consider two best known methods of obtaining completeness results. One of them—the method of canonical models—given a consistent logic L in ExtInt or NExtK, constructs a canonical Kripke model 𝔐_{L} = ⟨𝔉_{L}, 𝔙_{L}⟩ characterizing L. Sometimes the frame 𝔉_{L} turns out to be a frame for L, and then we can say at once that L is Kripke complete. Another method, known as filtration, is intended for establishing the finite approximability by means of extracting from the canonical models finite refutation frames.

5.1 The Henkin construction

Suppose L is a superintuitionistic or normal modal logic, and we want to find a class of Kripke models characterizing L. The proofs of Completeness Theorems for Int and K above provide us with a method of constructing models refuting formulas outside of L. However formulas in L need not be true in them. So let us try to modify this method in such a way that it would ensure not only completeness but also soundness.

Recall that the worlds in those models are tableaux t = (Γ, Δ) consistent in Int and K, with the truth-relation in them being chosen so that t ⊧ φ, for all φ ∈ Γ, and t |̸= ψ, for all ψ ∈ Δ. The condition guaranteeing in this situation that all formulas in L are true at all worlds is, of course, the inclusion L ⊆ Γ.

Now we restore this construction in all details. It is often called the Henkin construction in view of its conceptual closeness to the construction used by Henkin for proving the completeness of first order classical calculus.

So, let L be a consistent si-logic in the language L or a normal modal logic in the language ML. A tableau t = (Γ, Δ) in the language of L is said to be L-consistent if for no φ_{1}, …, φ_{n} in Δ do we have Γ ⊢_{L} φ_{1} ∨ … ∨ φ_{n}. t is called maximal if Γ∪Δ is the set of all formulas in the language of L. It should be clear that every maximal L-consistent tableau is saturated in Int or K (for details see the proof of Theorem 1.16).

The following two lemmas guarantee that if we succeed in constructing (according to our plan) a model whose points are all maximal L-consistent tableaux then all formulas in L will be true in this model, while all those outside of L will be refuted by it.

Lemma 5.1. (Lindenbaum’s Lemma) Every L-consistent tableau t = (Γ, Δ) can be extended to a maximal L-consistent tableau.

Proof Let φ_{1}, φ_{2}, … be some enumeration of all formulas in the language of L. Define a sequence of tableaux t_{0} = (Γ_{0}, Δ_{0}), t_{1} = (Γ_{1}, Δ_{1}), … by taking t_{0} = t and, for i ≥ 0,

t_{i+1} = \{ \begin{matrix}(Γ_{i}, Δ_{i} ∪ \{φ_{i}\}) & if (Γ_{i}, Δ_{i} ∪ \{φ_{i}\}) is L-consistent \\ (Γ_{i} ∪ \{φ_{i}\}, Δ_{i}) & otherwise. \end{matrix}

In exactly the same way as in the proof of Theorem 1.16 one can show that L-consistency of t_{i} entails the L-consistency of t_{i+1}. Thus all the constructed tableaux t_{0}, t_{1}, … prove to be L-consistent and for every formula φ there is i such that either φ ∈ Γ_{i} or φ ∈ Δ_{i}.

Let us consider now the tableau t^{∗} = (Γ^{∗}, Δ^{∗}) where

Γ^{∗} = ⋃_{i<ω} Γ_{i}, Δ^{∗} = ⋃_{i<ω} Δ_{i}.

It is clear that Γ^{∗} ∪ Δ^{∗} contains all the formulas in the language of L and so t^{∗} is maximal. To prove that it is L-consistent, suppose otherwise. Then for some φ_{1}, …, φ_{n} ∈ Δ^{∗}, there is a derivation of φ_{1} ∨ … ∨ φ_{n} from the set Γ^{∗} in L. Since this derivation uses only a finite number of assumptions in Γ^{∗}, there exists i such that φ_{1}, …, φ_{n} ∈ Δ_{i} and Γ_{i} ⊢_{L} φ_{1} ∨ … ∨ φ_{n}, contrary to t_{i} being L-consistent.

□

Lemma 5.2 Suppose Λ is a set of formulas and φ a formula in the language of L. Then Λ ⊢_{L} φ iff, for every maximal L-consistent tableau t = (Γ, Δ), φ ∈ Γ whenever Λ ⊆ Γ. In particular, φ ∈ L iff φ ∈ Γ for every maximal L-consistent tableau t = (Γ, Δ).

Proof (⇒) If Λ ⊆ Γ and φ ∉ Γ, for some maximal L-consistent tableau t = (Γ, Δ), then, by the maximality of t, φ ∈ Δ. Since Λ ⊢_{L} φ, it follows that t is not L-consistent, which is a contradiction.

(⇐) Suppose Λ ⊬_{L} φ. Then the tableau t = (Λ, {φ}) is L-consistent. By Lindenbaum’s Lemma, t is contained in a maximal L-consistent tableau, which is a contradiction. □

Remarks (1) When proving Lemmas 5.1 and 5.2, we did not use the rule of necessitation. So these lemmas hold for quasi-normal modal logics as well.

(2) It should be clear that with the help of transfinite induction the lemmas above can easily be extended to logics in uncountable languages. And certainly they hold for logics in finite languages.

Now we can construct the model we are after. First we form a frame 𝔉_{L} = ⟨W_{L}, R_{L}⟩ by taking W_{L} to be the set of all maximal L-consistent tableaux and, for every t_{1} = (Γ_{1}, Δ_{1}) and t_{2} = (Γ_{2}, Δ_{2}) in W_{L},

t_{1}R_{L}t_{2} iff Γ_{1} ⊆ Γ_{2} iff Δ_{1} ⊇ Δ_{2},

if L ∈ ExtInt and

t_{1}R_{L}t_{2} iff {φ : □φ ∈ Γ_{1}} ⊆ Γ_{2},

if L ∈ NExtK. The frame 𝔉_{L} is called the canonical frame for L.

Lemma 5.3 The canonical frame 𝔉_{L} for L is a Hintikka system in Int, if L ∈ ExtInt, and in K, if L ∈ NExtK.

Proof Follows from the proofs of Theorems 2.43 and 3.53 and Lindenbaum’s Lemma. □

Define a valuation 𝔙_{L} in 𝔉_{L} by taking, for every variable p,

𝔙_{L}(p) = {(Γ, Δ) : p ∈ Γ}.

The resulting model 𝔐_{L} = ⟨𝔉_{L}, 𝔙_{L}⟩ is called the canonical model for L.

Theorem 5.4. (Canonical Model) Let L be a consistent superintuitionistic or normal modal logic and 𝔐_{L} = ⟨𝔉_{L}, 𝔙_{L}⟩ its canonical model on the frame 𝔉_{L} = ⟨W_{L}, R_{L}⟩. Then for every formula φ and every tableau t = (Γ, Δ) in W_{L},

(i) φ ∈ Γ implies (𝔐_{L}, t) ⊧ φ,

(ii) φ ∈ Δ implies (𝔐_{L}, t) |̸= φ and so

(iii) (𝔐_{L}, t) ⊧ φ iff φ ∈ Γ.

Proof By Lemma 5.3, 𝔉_{L} is a Hintikka system. It remains to observe that the valuation 𝔙_{L} was defined in exactly the same way as in the proofs of Propositions 2.31 and 3.25, where the implications (i) and (ii) were established. □

Theorem 5.5 Suppose L is a consistent logic in ExtInt or NExtK. Then every L-consistent tableau is realized in 𝔐_{L}. In particular, Λ ⊢_{L} φ iff, for every point x in 𝔐_{L}, x ⊧ Λ implies x ⊧ φ, and φ ∈ L iff 𝔐_{L} ⊧ φ.

Proof Follows from Lemmas 5.1, 5.2 and Theorem 5.4. □

Of course, it seems unlikely that the completeness result of such generality can be used as a technical tool for deciding whether a given formula is in L. Indeed, the model 𝔐_{L} was defined via the derivability in L and so it is nothing more than a model-theoretic reformulation of L. The role of canonical models is different: they give us that starting point from which we can develop a model-theoretic approach to investigating the logics under consideration. In the next sections of this chapter we shall use canonical models to prove the Kripke completeness and finite approximability of many superintuitionistic and modal logics. But before that we observe some important properties of canonical models which will be required in the sequel.

A model 𝔐 = ⟨𝔉, 𝔙⟩ for Int or K is said to be differentiated if, for any two points x, y in 𝔉, x = y whenever exactly the same formulas are true at x and y. As a direct consequence of Canonical Model Theorem we obtain

Proposition 5.6 Every canonical model is differentiated.

A model 𝔐 = ⟨𝔉, 𝔙⟩ for Int on a frame 𝔉 = ⟨W, R⟩ is called tight if, for any x, y ∈ W, xRy whenever x ⊧ φ implies y ⊧ φ for every φ ∈ ForL. A model 𝔐 for K is tight if, for any x, y ∈ W, xRy whenever x ⊧ □φ implies y ⊧ φ for every φ ∈ ForML. It follows immediately from the definition of 𝔐_{L} that the following proposition holds

Proposition 5.7 Every canonical model is tight.

A model is called refined if it is both differentiated and tight. Notice that in the intuitionistic case differentiatedness follows from tightness.

Corollary 5.8 Every canonical model is refined.

In the modal case Propositions 5.6 and 5.7 can be generalized as follows.

Proposition 5.9 Suppose 𝔐_{L} = ⟨𝔉_{L}, 𝔙_{L}⟩ is the canonical model for a normal modal logic L. Then for any x, y ∈ W_{L} and any n ≥ 0, xR_{L}^{n}y iff x ⊧ □^{n}φ implies y ⊧ φ for every modal formula φ.

Proof (⇒) Follows from Proposition 3.2.1.

(⇐) is proved by induction on n. The case n = 0 means nothing else but that 𝔐_{L} is differentiated.

Suppose now that our proposition holds for n and let x ⊧ □^{n+1}φ implies y ⊧ φ for every φ ∈ ForML. We must prove is that there is z such that xR_{L}z and zR_{L}^{n}y. Consider the tableau t = (Γ, Δ) where

Γ = {φ : x ⊧ □φ}, Δ = {□^{n}ψ : y |̸= ψ}

and show that it is L-consistent. Suppose otherwise. Then

⊢_{L} φ_{1} ∧ … ∧ φ_{k} → □^{n}ψ_{1} ∨ … ∨ □^{n}ψ_{m},

for some φ_{1}, …, φ_{k} ∈ Γ and □^{n}ψ_{1}, …, □^{n}ψ_{m} ∈ Δ, whence, by Examples 3.49 and 3.50,

⊢_{L} □φ_{1} ∧ … ∧ □φ_{k} → □(□^{n}ψ_{1} ∨ … ∨ □^{n}ψ_{m}).

Therefore, x ⊧ □(□^{n}ψ_{1} ∨ … ∨ □^{n}ψ_{m}) and so x ⊧ □^{n+1}(ψ_{1} ∨ … ∨ ψ_{m}). But then y ⊧ ψ_{1} ∨ … ∨ ψ_{m}, whence y ⊧ ψ_{i} for some i, contrary to □^{n}ψ_{i} ∈ Δ.

By Lindenbaum’s Lemma, t is contained in some maximal L-consistent tableau t^{∗} = (Γ^{∗}, Δ^{∗}). By the definition of Γ, we must have xR_{L}t^{∗}. Furthermore, by the definition of Δ, t^{∗} ⊧ □^{n}φ implies y ⊧ φ, for every φ, and so, by the induction hypothesis, t^{∗}R_{L}^{n}y. □

Corollary 5.10 For every points x and y in the canonical model for a normal modal logic L and every n ≥ 0, xR_{L}^{n}y iff y ⊧ φ implies x ⊧ ◇^{n}φ, for all φ ∈ ForML.

A model 𝔐 is called compact if a tableau t is realizable in 𝔐 whenever every finite subtableau of t is realizable in 𝔐. For modal models 𝔐 this definition is clearly equivalent to the more familiar one: 𝔐 is compact if a set of formulas Σ is satisfied in 𝔐 whenever every finite subset of Σ is satisfied in 𝔐.

Proposition 5.11 Every canonical model is compact.

Proof Exercise. □

5.2 Completeness theorems

According to Theorem 5.5, all formulas that do not belong to a superintuitionistic or normal modal logic L are refuted in the canonical frame 𝔉_{L}. So if we prove that 𝔉_{L} is a frame for L, then the Kripke completeness of L will be established. Moreover, in this case L will be even strongly complete.

A logic L with 𝔉_{L} ⊧ L is called canonical. For example, Int and K are obviously canonical. Using this notion, the observation above can be formulated as follows.

Theorem 5.12 Every canonical superintuitionistic or normal modal logic is strongly Kripke complete.

In fact, sometimes we can derive a much more useful result than simply strong Kripke completeness. Suppose that we have already proved the soundness of L with respect to the class of frames satisfying some property P. If now we succeed in proving that 𝔉_{L} satisfies P, then we shall establish not only that L is canonical but also that it is characterized by the class of frames satisfying P.

For instance, Proposition 3.72 asserts that the calculus T or, which is the same, the logic L = K ⊕ □p → p is sound with respect to the class of reflexive frames. To prove the completeness of this logic, it suffices to establish the reflexivity of its canonical frame 𝔉_{L} = ⟨W_{L}, R_{L}⟩. Suppose otherwise. Then there is a tableau t = (Γ, Δ) ∈ W_{L} such that not tR_{L}t. By the definition of R_{L}, this is possible only if □φ ∈ Γ and φ ∈ Δ, for some formula φ. But then, by Lemmas 5.2 and 5.3, □φ → φ ∉ L, which is a contradiction.

Note by the way that in this argument we have used only that re belongs to L. So actually we have proved the following

Theorem 5.13 Suppose a logic L ∈ NExtK is consistent and contains re. Then the canonical frame 𝔉_{L} for L is reflexive.

Corollary 5.14 The calculus T is complete with respect to the class of reflexive frames.

If we recall that the logic T was defined as the logic characterized by the class of reflexive frames, then as a consequence of Proposition 3.72 and Corollary 5.14 we immediately derive

Corollary 5.15 (i) T = K ⊕ re.

(ii) T is canonical.

By the same scheme we can prove the canonicity of the logics in ExtInt and NExtK axiomatizable by the formulas which were supplied by first order equivalents in Chapters 2 and 3.

Theorem 5.16 Suppose L is a consistent superintuitionistic or normal modal logic and φ ∈ L, for some formula φ in the list da, wem, bd_{n}, bw_{n}, bc_{n}, btw_{n}, kp or, respectively, tra_{n}, sym, ser, ga_{klmn}, euc, den_{n}, sc, con, ga, dir, bw_{n}, bd_{n}, alt_{n}. Then the canonical frame 𝔉_{L} for L satisfies the condition corresponding to φ.

Proof We will consider only three formulas, leaving the others to the reader as an exercise.

(i) Let ◇^{k}□^{l}p → □^{m}◇^{n}p ∈ L, for some k, l, m, n ≥ 0, and show that the canonical frame 𝔉_{L} = ⟨W_{L}, R_{L}⟩ satisfies the condition

∀x, y, z (xR_{L}^{k}y ∧ xR_{L}^{m}z → ∃u (yR_{L}^{l}u ∧ zR_{L}^{n}u)).

Let t_{i} = (Γ_{i}, Δ_{i}), for i = 0, 1, 2, be some tableaux in W_{L} such that t_{0}R_{L}^{k}t_{1} and t_{0}R_{L}^{m}t_{2}. In order to show that there exists a tableau t = (Γ, Δ) for which t_{1}R_{L}^{l}t and t_{2}R_{L}^{n}t, we, by Lindenbaum’s Lemma, Proposition 5.9 and Corollary 5.10, should prove that the tableau

t′ = ({χ : □^{l}χ ∈ Γ_{1}}, {ψ : ◇^{n}ψ ∈ Δ_{2}})

is L-consistent. Suppose otherwise. Then χ → ψ ∈ L for some formulas □^{l}χ ∈ Γ_{1} and ◇^{n}ψ ∈ Δ_{2}. Applying the regularity rule l times, we obtain □^{l}χ → □^{l}ψ ∈ L, whence □^{l}ψ ∈ Γ_{1} and so ◇^{k}□^{l}ψ ∈ Γ_{0}. Since ◇^{k}□^{l}ψ → □^{m}◇^{n}ψ ∈ Γ_{0}, we have also □^{m}◇^{n}ψ ∈ Γ_{0}. But then ◇^{n}ψ ∈ Γ_{2}, contrary to t_{2} being L-consistent.

(The reader can find a more general result in Exercise 5.25, while the strongest generalization, known sa Sahlqvist’s Theorem, will be proved in Section 10.2.)

(ii) Suppose now that □(□^{+}p → q) ∨ □(□^{+}q → p) ∈ L and show that 𝔉_{L} is connected, i.e.,

∀x, y, z (xR_{L}y ∧ xR_{L}z ∧ y ≠ z → yR_{L}z ∨ zR_{L}y).

Suppose otherwise. Then we have three tableaux t_{i} = (Γ_{i}, Δ_{i}) in W_{L}, for i = 0, 1, 2, such that (a) t_{0}R_{L}t_{1}, (b) t_{0}R_{L}t_{2}, (c) t_{1} ≠ t_{2}, (d) not t_{1}R_{L}t_{2} and (e) not t_{2}R_{L}t_{1}. By (d), there is φ_{1} ∈ Δ_{2} such that □φ_{1} ∈ Γ_{1}, while by (c), we have some χ_{1} ∈ Γ_{1} ∩ Δ_{2}. Let φ = φ_{1} ∨ χ_{1}. Then □^{+}φ ∈ Γ_{1} and φ ∈ Δ_{2}. By using (e) and (c) in exactly the same way, we can find ψ ∈ Δ_{1} such that □^{+}ψ ∈ Γ_{2}. Therefore, □(□^{+}φ → ψ) ∨ □(□^{+}ψ → φ) ∈ Δ_{0}, which is a contradiction.

(iii) Finally, we consider a si-logic L containing the Kreisel–Putnam Formula

kp = (¬p → q ∨ r) → (¬p → q) ∨ (¬p → r)

and prove that

∀x, y, z (xRy ∧ xRz ∧ ¬yRz ∧ ¬zRy → ∃u(xRu ∧ uRy ∧ uRz ∧
∀v(uRv → ∃w(vRw ∧ (yRw ∨ zRw))))).

Suppose t_{1} = (Γ_{1}, Δ_{1}), t_{2} = (Γ_{2}, Δ_{2}), t_{3} = (Γ_{3}, Δ_{3}) are points in W_{L} such that t_{1}R_{L}t_{2}, t_{1}R_{L}t_{3} and ¬t_{2}R_{L}t_{3}, ¬t_{3}R_{L}t_{2}. Form a tableau t = (Γ, Δ) by taking

Γ = Γ_{1} ∪ {¬φ : ¬φ ∈ Γ_{2} ∩ Γ_{3}},
Δ = Δ_{2} ∪ Δ_{3}

and show that t is L-consistent. Indeed, if this is not the case then (using the first de Morgan Law which belongs to Int) we would have

Γ_{1} ⊢_{L} ¬φ → ψ ∨ χ,

for some ¬φ ∈ Γ_{2} ∩ Γ_{3}, ψ ∈ Δ_{2}, χ ∈ Δ_{3}, and so, by kp,

Γ_{1} ⊢_{L} (¬φ → ψ) ∨ (¬φ → χ).

Therefore, either ¬φ → ψ ∈ Γ_{1} or ¬φ → χ ∈ Γ_{1}. In the former case we would then have ψ ∈ Γ_{2} and in the latter χ ∈ Γ_{3}, contrary to the L-consistency of t_{2} and t_{3}.

Thus, t is L-consistent and, by Lindenbaum’s Lemma, it can be extended to a maximal L-consistent tableau, say, t_{4} = (Γ_{4}, Δ_{4}). By the definition, t_{1}R_{L}t_{4}, t_{4}R_{L}t_{2} and t_{4}R_{L}t_{3}. It remains to show that every successor of t_{4} has a common successor with t_{2} or t_{3}. Suppose otherwise, i.e., some successor t′ = (Γ′, Δ′) of t_{4} has no common successors with t_{2} and t_{3}. Then there are formulas ¬φ_{2} ∈ Γ_{2} and ¬φ_{3} ∈ Γ_{3} such that φ_{2}, φ_{3} ∈ Γ′. Indeed, the tableau (Γ_{2} ∪ Γ′, ∅) is L-inconsistent (for otherwise t_{2} and t′ would have a common successor) and so φ, φ_{2} ⊢_{L} ⊥, for some φ ∈ Γ_{2}, φ_{2} ∈ Γ′, from which φ ⊢_{L} ¬φ_{2} and hence ¬φ_{2} ∈ Γ_{2}.

Therefore, ¬φ_{2} ∨ ¬φ_{3} and so ¬(φ_{2} ∧ φ_{3}) are in Γ_{2} ∩ Γ_{3}. But the, since t_{4}R_{L}t′, we have ¬(φ_{2} ∧ φ_{3}) ∈ Γ′. On the other hand φ_{2} ∧ φ_{3} ∈ Γ′, contrary to the L-consistency of t′. □

As a consequence of Theorem 5.16 we immediately obtain

Theorem 5.17 Every logic L in ExtInt and NExtK axiomatizable by some of the formulas mentioned in Theorem 5.16 is canonical, with the canonical frame 𝔉_{L} satisfying the first order conditions corresponding to the axioms of L.

In particular we have the following completeness results Corollary 5.18 (i) The calculus K4 is characterized by the class of transitive frames.

(ii) S4 is characterized by the class of quasi-ordered frames.

(iii) S5 is characterized by the class of frames with universal alternativeness relations.

(iv) D is characterized by the class of serial frames.

(v) S4.3 is characterized by the class of connected quasi-orders and by the class of linear partial orders.

Proof (i), (ii), (iv) and the first part of (v) are immediate consequences of Theorem 5.17 and the soundness results in Section 3.8, (iii) follows from these and Generation Theorem. As to the completeness of S4.3 with respect to linear partial orders, suppose ⊬_{S4.3} φ. Then φ is refuted in a connected quasi-order and so, by Generation Theorem, in a frame which is a chain of clusters. By bulldozing this chain (see the proof of Theorem 3.20), we can construct a linear order which is reducible to it and so, by Reduction Theorem, also refutes φ. □

For S5 Theorem 5.17 yields even a better result.

Corollary 5.19 S5 is locally tabular and characterized by the class of finite frames with universal alternativeness relations.

Proof For n > 0 let ML_{n} be a modal language with n variables. By Theorem 5.17, the logic S5(n) = S5∩ForML_{n} is canonical and 𝔉_{S5(n)} is the disjoint union of clusters. Since 𝔐_{S5(n)} is differentiated and by Proposition 3.7, each of these clusters may contain at most 2^{n} points and so 𝔉_{S5(n)} is finite. Therefore, there are only finitely many pairwise non-equivalent formulas with n variables in S5 and each of them that is not in S5 is refuted in 𝔉_{S5(n)}. □

Unfortunately the method of establishing completeness using canonical models is far from being universal: there are normal modal and superintuitionistic logics which are Kripke complete but not canonical, witnesses GL, Grz, SL (see Section 6.2) and the McKinsey Logic

KM = K ⊕ □◇p → ◇□p.

It also turns out that the axioms of these logics do not correspond to any first order condition on their Kripke frames.

As to the McKinsey axiom ma, we saw in Section 3.5 that in the class of transitive frames it corresponds to the McKinsey condition. Moreover, we will show now that the canonical frame for every normal extension of

K4.1 = K4 ⊕ □◇p → ◇□p

satisfies it. To this end we require the following

Lemma 5.20 ◇ ⋀_{i=1}^{n}(◇φ_{i} → □φ_{i}) ∈ K4.1, for any formulas φ_{1}, …, φ_{n}.

Proof Observe first that since (□◇p → ◇□p) ↔ ◇(◇p → □p) ∈ K (see Table 3.1), ◇(◇φ → □φ) ∈ K4.1 for any φ. Let ψ_{i} = ◇φ_{i} → □φ_{i}, i = 1, …, n. Then ◇ψ_{1}, …, ◇ψ_{n} ∈ K4.1. By RN, □◇ψ_{1}, □◇ψ_{2} ∈ K4.1 and so ◇□ψ_{2} ∈ K4.1. By using twice □p ∧ ◇q → ◇(p ∧ q) in Table 3.1, we get ◇◇(ψ_{1} ∧ ψ_{2}) ∈ K4.1 and so ◇(ψ_{1} ∧ ψ_{2}) ∈ K4.1, since ◇◇p → ◇p is in K4. Now by applying the same argument to ◇(ψ_{1} ∧ ψ_{2}) and ◇ψ_{3}, we obtain ◇(ψ_{1} ∧ ψ_{2} ∧ ψ_{3}) ∈ K4.1 and so forth. Eventually we shall have ◇(ψ_{1} ∧ … ∧ ψ_{n}) ∈ K4.1. □

Theorem 5.21 Suppose L ∈ NExtK4 is consistent and contains ma. Then 𝔉_{L} = ⟨W_{L}, R_{L}⟩ satisfies the McKinsey condition

∀x∃y (xR_{L}y ∧ ∀z (yR_{L}z → y = z)).

Proof Let t_{0} = (Γ_{0}, Δ_{0}) be some tableau in W_{L}. Consider the tableau t′ = (Γ′, ∅) with

Γ′ = {φ : □φ ∈ Γ_{0}} ∪ {◇φ → □φ : φ ∈ ForML}

and show that it is L-consistent. Suppose otherwise. Then

φ, ◇φ_{1} → □φ_{1}, …, ◇φ_{n} → □φ_{n} ⊢_{L} ⊥,

for some □φ ∈ Γ_{0} and φ_{1}, … φ_{n} ∈ ForML. By Deduction Theorem and the regularity rule, it follows that

⊢_{L} □φ → □¬ ⋀_{i=1}^{n}(◇φ_{i} → □φ_{i}),

and so

¬◇ ⋀_{i=1}^{n}(◇φ_{i} → □φ_{i}) ∈ Γ_{0},

contrary to Lemma 5.20.

Now take a maximal L-consistent extension t_{1} = (Γ_{1}, Δ_{1}) of t′. Clearly t_{0}R_{L}t_{1}. We are going to show that either t_{1} itself or any t_{2} ∈ t_{1}↑ has no proper successors. Indeed, otherwise we have three distinct tableaux t_{i} = (Γ_{i}, Δ_{i}), for i = 1, 2, 3, such that t_{1}R_{L}t_{2}R_{L}t_{3}. But then there is a formula φ such that φ ∈ Γ_{2}, φ ∈ Δ_{3} and so, by the transitivity of R_{L}, ◇φ ∈ Γ_{1} and □φ ∈ Δ_{1}, whence ◇φ → □φ ∈ Δ_{1}, contrary to the t_{1} being L-consistent. □

As a consequence of this theorem and the results in Section 3.5 we derive

Corollary 5.22 (i) K4.1 = K4 ⊕ □◇p → ◇□p is canonical, with 𝔉_{K4.1} being transitive and satisfying the McKinsey condition.

(ii) S4.1 = S4 ⊕ □◇p → ◇□p is canonical, with 𝔉_{S4.1} being a quasi-order satisfying the McKinsey condition.

5.3 The filtration method

The canonical model for a consistent logic L refutes all the formulas which do not belong to L. It is very big (contains continuum many points, to be more exact) and complicated. On the other hand, the examples of Int and K show that each formula φ ∉ L may be separated from L by a finite frame. Provided that L is finitely axiomatizable, this immediately yields the decidability of L (for details consult Section 16.2).

The filtration method is intended to establish such kind of completeness results and sometimes it may succeed even if the method of canonical models fails to prove canonicity.

To establish the finite approximability of a logic L, we need to prove that for every formula φ there is a frame 𝔉 satisfying the following three conditions: (1) 𝔉 |̸= φ, (2) 𝔉 is finite, (3) 𝔉 ⊧ L. By Theorem 5.5, to ensure (1) it suffices to take the canonical frame 𝔉_{L} for L. It is somewhat more difficult to satisfy (2), but, as we saw in Sections 2.4 and 3.4, also possible. Since we are interested only in truthvalues of φ, all the formulas which are not subformulas of φ may be discarded from the tableaux in W_{L}. Or better we shall regard tableaux t_{1} = (Γ_{1}, Δ_{1}) and t_{2} = (Γ_{2}, Δ_{2}) in W_{L} as Subφ-equivalent if Γ_{1} ∩ Subφ = Γ_{2} ∩ Subφ. And then we see that modulo the Subφ-equivalence tableaux in W_{L} mostly duplicate each other. More exactly, there are at most 2^{|Subφ|} pairwise non-Subφ-equivalent tableaux in W_{L}. Is it possible to compose only of them some Hintikka system ℌ = ⟨T, S⟩? To do this it suffices to define an accessibility relation S so that the conditions (HS_{I}1) and (HS_{I}2), if L ∈ ExtInt, and (HS_{M}1) and (HS_{M}2), if L ∈ NExtK, are satisfied. The former of these two conditions can always be satisfied, for instance, by taking it as a necessary condition for S. To meet the latter, we can use the fact that 𝔉_{L} satisfies it and simply put t_{1}St_{2} if t′_{1}R_{L}t′_{2}, for some t′_{1}, t′_{2} ∈ W_{L} that are Subφ-equivalent to t_{1} and t_{2}, respectively. The restrictions thus obtained give in general a whole spectrum of suitable S. And this is very much to the point, since we still need to take care of the condition (3). Whether (3) can be met by a proper choice of S depends on the particular logic L. So let us first consider in more details the construction sketched above and then apply it for establishing the finite approximability of a few superintuitionistic and modal logics.

Suppose we have a model 𝔐 = ⟨𝔉, 𝔙⟩ of the language L or ML on a frame 𝔉 = ⟨W, R⟩ and let Σ be a set of (L- or ML-) formulas closed under subformulas, i.e., Subφ ⊆ Σ whenever φ ∈ Σ. We say points x, y ∈ W are Σ-equivalent in 𝔐 and write x ∼_{Σ} y if

(𝔐, x) ⊧ φ iff (𝔐, y) ⊧ φ, for every φ ∈ Σ.

Clearly ∼_{Σ} is an equivalence relation on W. Denote by [x]_{Σ} the equivalence class generated by x, i.e., put [x]_{Σ} = {y ∈ W : x ∼_{Σ} y}. As a rule we will drop the subscript Σ and write simply [x] and x ∼ y if this does not involve ambiguity.

A filtration of 𝔐 through Σ is any model 𝔑 = ⟨𝔊, 𝔘⟩ based on a frame 𝔊 = ⟨V, S⟩ such that

(i) V = {[x] : x ∈ W };

(ii) 𝔘(p) = {[x] : x ∈ 𝔙(p)}, for every variable p ∈ Σ;

(iii) xRy implies [x]S[y], for all x, y ∈ W;

(iv) if [x]S[y] then y ⊧ φ whenever x ⊧ □φ, for x, y ∈ W and □φ ∈ Σ,

in the modal case and

(iv′) if [x]S[y] then y ⊧ φ whenever x ⊧ φ, for all x, y ∈ W and φ ∈ Σ,

in the intuitionistic one.

Theorem 5.23. (Filtration) Let 𝔑 be a filtration of a model 𝔐 through a set of formulas Σ. Then for every point x in 𝔐 and every formula φ ∈ Σ,

(𝔐, x) ⊧ φ iff (𝔑, [x]) ⊧ φ.

Proof The proof proceeds by induction on the construction of φ. The basis of induction follows from (ii). Now let φ = □ψ ∈ Σ and x ⊧ φ. To prove [x] ⊧ φ, we need to show that [y] ⊧ ψ for every successor [y] of [x]. So suppose [x]S[y]. Then, by (iv), y ⊧ ψ and, by the induction hypothesis, [y] ⊧ ψ. Conversely, let [x] ⊧ □ψ. Take any y ∈ x↑. Then, by (iii), [x]S[y] and so [y] ⊧ ψ, whence, by the induction hypothesis, y ⊧ ψ. The induction step for φ = ψ ∧ χ, φ = ψ ∨ χ and φ = ψ → χ in the modal case follows immediately from the truth-definition and the induction hypothesis.

The intuitionistic case is considered analogously by using (iv′) instead of (iv). □

In general, the conditions (iii) and (iv) (or (iv′)) do not determine S uniquely. Actually, they allow us to choose any relation S in the interval \underline{S} ⊆ S ⊆ \overline{S}, where

\underline{S} = \{⟨[x], [y]⟩ : ∃x′, y′ ∈ W (x′ ∼ x ∧ y′ ∼ y ∧ x′Ry′)\},
\overline{S} = \{⟨[x], [y]⟩ : ∀□φ ∈ Σ (x ⊧ □φ → y ⊧ φ)\}

or, in the intuitionistic case,

\overline{S} = \{⟨[x], [y]⟩ : ∀φ ∈ Σ (x ⊧ φ → y ⊧ φ)\}.

Indeed, if [x]S[y] holds then, by (iv) and (iv′), [x]\overline{S}[y]. And if [x]\underline{S}[y] then x′Ry′, for some x′ ∈ [x], y′ ∈ [y], and so, by (iii), [x]S[y]. The fact that \underline{S} satisfies (iv) or (iv′) and \overline{S} satisfies (iii) follows directly from the truth-definition in modal and intuitionistic models.

For this reason the filtration on the frame \underline{𝔊} = ⟨V, \underline{S}⟩ is called the finest or the least filtration of 𝔐 through Σ, while the filtration on the frame \overline{𝔊} = ⟨V, \overline{S}⟩ is called the coarsest or the greatest.

It is to be noted that a relation S between \underline{S} and \overline{S} may be nontransitive even if the original R is transitive, in particular, not all S in this interval give rise to filtrations of intuitionistic models. To construct a transitive relation we can take the transitive closure ˆ \underline{S} of \underline{S}, i.e., put

ˆ\underline{S} = \{⟨[x], [y]⟩ : ∃n > 0 [x]\underline{S}^{n}[y]\}.

Clearly ˆ \underline{S} satisfies (iii). To prove (iv), suppose [x]ˆ\underline{S}[y] and x ⊧ □φ, for some x, y in 𝔐 and □φ in Σ. Then there is a finite sequence of points [u], …, [v] such that [x]\underline{S}[u]\underline{S} … \underline{S}[v]\underline{S}[y]. By the definition of \underline{S}, x′Ru′ for some x′ and u′ that are Σ-equivalent to x and u, respectively. Since R is transitive and by Proposition 3.6, we then have u′ ⊧ □^{+}φ and so u ⊧ □^{+}φ. Using the same argument for the sequence u, …, v, y, we shall eventually obtain y ⊧ □^{+}φ. The intuitionistic models are considered analogously. Observe that in this case ˆ \underline{S} as well as \overline{S} are partial orders.

Alternatively we can define a transitive filtration 𝔑 = ⟨𝔊, 𝔘⟩ of a transitive modal model 𝔐 through Σ by taking, for any x and y in 𝔐,

[x]S[y] iff y ⊧ □^{+}φ whenever x ⊧ □φ, for all □φ ∈ Σ.

It should be clear that the frame 𝔊 = ⟨V, S⟩ is transitive and that 𝔑 is a filtration of 𝔐. It is called the Lemmon filtration of 𝔐 through Σ.

A very important property of filtrations is that they are finite whenever the “filter” Σ is finite. Moreover, a filtration may be finite even if the filter Σ is infinite. Say that a set Σ is finitely based over a model 𝔐 if there is a finite set of formulas Δ, a finite base of Σ over 𝔐, such that

∀ψ ∈ Σ ∃χ ∈ Δ 𝔐 ⊧ ψ ↔ χ.

For example, since Cl is locally tabular (see Theorem 1.29, the Boolean closure, i.e., the closure under ∧, ∨, →, ⊥ of every finite set of modal formulas is finitely based over any model. (However, this is not so in the intuitionistic case.)

Proposition 5.24 Suppose 𝔑 is a filtration of a model 𝔐 through a set Σ which is finitely based over 𝔐 and Δ is a finite base of Σ. Then 𝔑 contains at most 2^{|Δ|} points.

Proof Clearly, two points are Σ-equivalent in 𝔐 iff they are Δ-equivalent. So the number of pairwise non-Σ-equivalent points in 𝔐 is not greater than the number of subsets in Δ. □

As a consequence of Theorem 5.23 and Proposition 5.24 we obtain

Corollary 5.25 Suppose 𝔐 is a countermodel for φ and Σ a finitely based over 𝔐 set of formulas closed under subformulas. Then every filtration of 𝔐 through Σ is a finite countermodel for φ.

Thus, to prove the finite approximability of a logic L, it suffices to show that for every formula φ ∉ L there is a filtration 𝔑 of some countermodel 𝔐 for φ through some finitely based (over 𝔐) filter Σ containing φ such that 𝔑 ⊧ L. If this is really the case then we say that L admits filtration.

Corollary 5.26 If a logic L admits filtration then L is finitely approximable.

The following two remarks are relevant here. First, if a logic L is sound with respect to the class of frames satisfying a property P, then to prove that L admits filtration it is sufficient to show that for every φ ∉ L there is a filtration 𝔑 = ⟨𝔊, 𝔘⟩ of 𝔐_{L} (or some other countermodel for φ) through some finitely based Σ containing φ such that 𝔊 satisfies P. Second, it turns out that when filtrating the canonical model 𝔐_{L}, we have no real choice for S. For the following proposition holds.

Proposition 5.27 Suppose 𝔑 = ⟨𝔊, 𝔘⟩ is a filtration of the canonical model 𝔐_{L} = ⟨𝔉_{L}, 𝔙_{L}⟩ through Σ such that 𝔑 ⊧ L. Then 𝔑 is the finest filtration of 𝔐_{L} through Σ.

Proof Suppose 𝔊 = ⟨V, S⟩. We need to show that S ⊆ \underline{S}, i.e., for any [x], [y] ∈ V such that [x]S[y], there are x′, y′ ∈ W_{L} for which x′ ∼ x, y′ ∼ y and x′R_{L}y′. Consider the tableaux t_{1} = (Γ_{1}, Δ_{1}) and t_{2} = (Γ_{2}, Δ_{2}) where

Γ_{1} = {φ : (𝔑, [x]) ⊧ φ}, Δ_{1} = {φ : (𝔑, [x]) |̸= φ},
Γ_{2} = {φ : (𝔑, [y]) ⊧ φ}, Δ_{2} = {φ : (𝔑, [y]) |̸= φ}.

Since 𝔑 ⊧ L, both t_{1} and t_{2} are L-consistent and so belong to W_{L}. And since [x]S[y], we must have t_{1}R_{L}t_{2}. □

We are in a position now to prove the finite approximability of a few modal and superintuitionistic logics using the filtration method.

First of all, since our basic logics Int and K are characterized by the class of all frames, they trivially admit filtration.

Next, let us observe that, by (iii), every filtration of a reflexive or serial model is reflexive or serial too. More generally, if the underlying frame of a model 𝔐 satisfies some condition expressed by first order formulas (with R and = as their only predicates), containing no occurrences of → and ⊥ — such formulas are called positive — then (iii) guarantees that the underlying frame of every filtration of 𝔐 also satisfies this condition, which can readily be proved by induction on the construction of the first order positive formulas. In fact, this is a consequence of the result in classical model theory according to which positive formulas are stable under homomorphisms (see (Chang and Keisler 1973), Theorem 3.2.4). Thus we have

Theorem 5.28 If a normal modal or superintuitionistic logic L is characterized by the class of frames satisfying some first order positive formulas in R and = then L admits filtration and so is finitely approximable.

Proof The detailed proof is left to the reader as an exercise. □

Corollary 5.29 The logics D, T and S5 are finitely approximable and decidable.

Proposition 5.30 The finest filtration of every symmetrical model is also symmetrical.

Proof Suppose 𝔑 = ⟨𝔊, 𝔘⟩ is the finest filtration of a model 𝔐 based on a symmetrical frame 𝔉 = ⟨W, R⟩ and [x]S[y], for some points [x], [y] in 𝔊. Then by the definition of S, there are x′ ∈ [x] and y′ ∈ [y] such that x′Ry′, from which y′Rx′ and so, by (iii), [y]S[x]. □

As a consequence of Proposition 5.30 and Theorem 5.17, according to which KB is characterized by symmetrical frames, we obtain

Corollary 5.31 KB admits filtration and so is finitely approximable and decidable.

Using the transitive closure of the finest filtration or the Lemmon filtration and the fact that K4, D4 and S4 are characterized by the classes of transitive frames, serial transitive frames and quasi-orders, respectively, we immediately obtain

Corollary 5.32 The logics K4, D4, S4 admit filtration and so are finitely approximable and decidable.

Also we have Theorem 5.33 The logics K4.2, K4.3, S4.2, S4.3, KC, LC admit filtration and so are finitely approximable and decidable.

Proof We show how to establish this result only for K4.2. The other logics are considered analogously.

By Theorem 5.17 and Generation Theorem, K4.2 is characterized by the class of rooted transitive directed frames. So it suffices to show that, for every model 𝔐 based on such a frame 𝔉 = ⟨W, R⟩ and a finite filter Σ, there is a filtration of 𝔐 through Σ which is also based on a transitive directed frame.

Take the transitive closure 𝔑 of the finest filtration of 𝔐 through Σ. Let S be the accessibility relation in 𝔑 and let [x]S[y] and [x]S[z], for some points [x], [y], [z] in 𝔑 such that [y] ≠ [z]. Then uRy′, vRz′, for some y′ ∼ y, z′ ∼ z, u and v. Clearly, y′ ≠ z′. Since 𝔉 is rooted and transitive, both y′ and z′ are seen from the root of 𝔉 and so, by the directedness condition, there is w such that y′Rw and z′Rw, from which [y]S[w] and [z]S[w]. □

Remark It is worth noting that although S4.3 is characterized by the class of linear partial orders, it is not characterized by the class of finite linear partial orders. For example, the Grzegorczyk formula is refuted by a proper cluster or an infinite ascending chain and so is not in S4.3. On the other hand, it is valid in every finite partial order. It follows in particular that by filtrating linear orders we may obtain chains with proper clusters.

Our next two results are a bit more complicated. They demonstrate situations when we have to filtrate models through sets which are bigger than the set of subformulas of the refuted formula.

Theorem 5.34 The logics K4.1 and S4.1 admit filtration and so are finitely approximable and decidable.

Proof We consider only K4.1, leaving S4.1 to the reader as an exercise. According to Corollary 5.22, K4.1 is characterized by the class of transitive frames satisfying the McKinsey condition. So, given a countermodel 𝔐 for φ on such a frame 𝔉, we must construct a transitive filtration 𝔑 of 𝔐 through some finite set Σ ⊇ Subφ such that every final cluster in 𝔑 is simple. Observe at once that, by (iii) and the McKinsey condition, no filtration of 𝔐 contains dead ends. Thus, our only problem is to avoid final proper clusters in 𝔑. We recommend the reader first to try filtrating 𝔐 through Subφ to understand that under such a filtration two final simple clusters in 𝔐 may be put into one proper cluster in 𝔑. To prevent this, we should take a smaller accessibility relation in our filtration which can be done by choosing a bigger filter Σ.

Define Σ as the closure under subformulas of the set

{□◇ψ, ◇□ψ : ψ ∈ Subφ}

and let 𝔑 be the transitive closure of the finest filtration of 𝔐 through Σ. Suppose [x] and [y] belong to a final cluster in 𝔑 and show that [x] = [y]. According to Filtration Theorem, it suffices to establish that [x] ∼ [y].

Take any formula ψ ∈ Σ. If ψ = □χ or ψ = ◇χ then, by Proposition 3.6, [x] ⊧ ψ iff [y] ⊧ ψ. So the only remaining case is ψ ∈ Subφ. Suppose [x] ⊧ ψ. Then ◇ψ is true in 𝔑 at every point in the cluster containing [x]; so [x] ⊧ □◇ψ and x ⊧ □◇ψ. Since 𝔐 is a model for K4.1, we must then have x ⊧ ◇□ψ and hence [x] ⊧ ◇□ψ. Therefore, there is a point [z] in the cluster under consideration such that [z] ⊧ □ψ and so [y] ⊧ ψ. □

Theorem 5.35 The logic K5 admits filtration and so is finitely approximable and decidable.

Proof By Theorem 5.17, K5 = K ⊕ ◇□p → □p is characterized by the class of euclidean frames. Let 𝔐 be a countermodel for a formula φ based on a euclidean frame. Again, a filtration of 𝔐 through Subφ need not be euclidean. So let us try a bigger filter, say,

Σ = Subφ ∪ {◇□ψ : □ψ ∈ Subφ}.

Let 𝔑 be the coarsest filtration of 𝔐 through Σ. We show that its underlying frame 𝔊 = ⟨V, S⟩ is euclidean.

Suppose [x]S[y] and [x]S[z], for some [x], [y], [z] ∈ V, and prove that [y]S[z]. By the definition of S, we need to show that [y] ⊧ □ψ implies [z] ⊧ ψ, for every □ψ ∈ Σ. So let □ψ ∈ Σ and [y] ⊧ □ψ. Then [x] ⊧ ◇□ψ and, by Filtration Theorem, x ⊧ ◇□ψ, from which x ⊧ □ψ, since 𝔐 is a model for K5. Therefore,

[x] ⊧ □ψ and [z] ⊧ ψ. □

Remark Since K5 has only finitely many distinct modalities (see Exercise 5.11), the modal closure, i.e., the closure under prefixing □ and ◇, of every finite set of formulas is finitely based over any model for K5. So instead of Σ in the proof above we might use the modal closure of Subφ.

5.4 Diego’s Theorem The bigger the filter, the more properties of the initial model will be inherited by its filtration and the more chances that the filtration will be a model for the logic under consideration. In this section we show that the closure of every finite set of intuitionistic formulas under ∧, → and ⊥ (or ¬) is finitely based over any intuitionistic model and so can be exploited as a filter for establishing the finite approximability of superintuitionistic logics. This very useful result is an immediate consequence of the following

Theorem 5.36. (Diego’s Theorem) For every n ≥ 0, the set Ξ_{n} of L-formulas, constructed from the variables p_{1}, …, p_{n} using ∧, → and ⊥, contains only finitely many pairwise non-equivalent in Int formulas.

Proof The proof proceeds via a number of lemmas and requires some auxiliary definitions.

To begin with, we form the coarsest filtration 𝔐 = ⟨𝔉, 𝔙⟩ of the canonical model for Int through Ξ_{n}. We will regard points t in 𝔉 = ⟨W, R⟩ as tableaux t = (Γ, Δ) such that

Γ = {φ ∈ Ξ_{n} : (𝔐, t) ⊧ φ}, Δ = {φ ∈ Ξ_{n} : (𝔐, t) |̸= φ}.

For an atomic p ∈ Ξ_{n}, call such a tableau t = (Γ, Δ) p-prime (relative to Ξ_{n}) if p ∈ Δ and, for every φ ∈ Ξ_{n}, either φ ∈ Γ or φ → p ∈ Γ.

Lemma 5.37 For any atomic p ∈ Ξ_{n}, any t = (Γ, Δ) ∈ W and any φ ∈ Ξ_{n}, if φ → p ∈ Δ then there is a p-prime successor t^{∗} = (Γ^{∗}, Δ^{∗}) of t in 𝔉 such that φ ∈ Γ^{∗}.

Proof Since φ → p ∈ Δ, there must be a point t_{1} = (Γ_{1}, Δ_{1}) accessible from t in 𝔉 for which φ ∈ Γ_{1}, p ∈ Δ_{1}. Let X be a maximal chain of points in 𝔉 refuting p and such that t_{1} ∈ X. Put Γ^{∗} = ⋃_{(Γ′,Δ′)∈X} Γ′, Δ^{∗} = Ξ_{n} − Γ^{∗} and t^{∗} = (Γ^{∗}, Δ^{∗}). The tableau t^{∗} is Int-consistent, for otherwise φ_{1} ∧ … ∧ φ_{k} → ψ_{1} ∨ … ∨ ψ_{l} ∈ Int, for some φ_{1}, …, φ_{k} ∈ Γ^{∗}, ψ_{1}, …, ψ_{l} ∈ Δ^{∗}. But then, since X is linearly ordered and by (HS_{I}1), there exists t′ = (Γ′, Δ′) ∈ X such that φ_{1}, …, φ_{k} ∈ Γ′, ψ_{1}, …, ψ_{l} ∈ Δ′, contrary to the Int-consistency of t′. Therefore, by Lindenbaum’s Lemma, t^{∗} is a point in 𝔉. In fact, it is the final point in X. Besides, we clearly have φ ∈ Γ^{∗} and tRt^{∗}. It remains to observe that t^{∗} is pprime. Indeed, by the definition, p ∈ Δ^{∗} and if ψ and ψ → p are in Δ^{∗} then there is a successor t′ of t^{∗} such that t′ ⊧ ψ, t′ |̸= p, from which t′ = t^{∗}, for otherwise we can extend the chain X by adding t′ to it, contrary to its maximality. □

Let V be the set of all p-prime tableaux in W, for all atomic p ∈ Ξ_{n}, S the restriction of R to V and 𝔊 = ⟨V, S⟩.

Lemma 5.38 For any t = (Γ, Δ) ∈ W and any φ ∈ Δ, there is a tableau t^{∗} = (Γ^{∗}, Δ^{∗}) in V such that tRt^{∗} and φ ∈ Δ^{∗}.

Proof Observe first that, by the intuitionistic equivalences,

p ↔ ((⊥ → ⊥) → p), (p → (q → r)) ↔ (p ∧ q → r)

and

(p → q ∧ r) ↔ (p → q) ∧ (p → r),

φ is equivalent in Int to a formula of the form ⋀_{i}(ψ_{i} → p_{i}), for some atomic p_{i} ∈ Ξ_{n} and ψ_{i} ∈ Ξ_{n}. Therefore, ψ_{i} → p_{i} ∈ Δ, for some i, and so, by Lemma 5.37, there is a p_{i}-prime tableau t^{∗} = (Γ^{∗}, Δ^{∗}) accessible from t and such that ψ_{i} ∈ Γ^{∗}. It follows immediately that φ ∈ Δ^{∗}. □

As a consequence we readily derive that 𝔊 = ⟨V, S⟩ is a Hintikka system characterizing Ξ_{n} in the sense that, for every φ ∈ Ξ_{n}, φ is in Int iff φ ∈ Γ, for all (Γ, Δ) in V.

Our goal now is to show that 𝔊 is finite. Lemma 5.39 If t = (Γ, Δ) is a p-prime tableau and t′ = (Γ′, Δ′) is any successor of t in 𝔊 different from t, then p ∈ Γ′.

Proof Since t ≠ t′ and tSt′, there must be some φ ∈ Γ′ − Γ. And since t is p-prime, φ → p ∈ Γ. Therefore, φ → p ∈ Γ′ and so p ∈ Γ′. □

Suppose t = (Γ, Δ) is a p-prime tableau in 𝔊, for some p ≠ p_{n}, and p_{n} ∈ Γ. Form a tableau t′ = (Γ′, Δ′) by taking

Γ′ = {φ ∈ Γ : p_{n} ∉ Subφ}, Δ′ = {φ ∈ Δ : p_{n} ∉ Subφ}.

Clearly t′ is a p-prime tableau relative to Ξ_{n−1}. It turns out that t is uniquely determined by t′ and p_{n} in the following sense. Lemma 5.40 Γ = {φ ∈ Ξ_{n} : Γ′, p_{n} ⊢_{Int} φ}.

Proof It suffices to show that Γ′, p_{n} ⊢_{Int} φ, for every φ ∈ Γ. So let φ be an arbitrary formula in Γ and φ′ = φ{⊤/p_{n}}. By Strong Completeness Theorem for Int, we have p_{n} ⊢_{Int} φ′ ↔ φ. It follows that φ′ ∈ Γ. Hence φ′ ∈ Γ′ and so Γ′, p_{n} ⊢_{Int} φ. □

We are in a position now to prove the crucial Lemma 5.41 𝔊 is finite.

Proof The proof proceeds by induction on n. If n = 0 then, according to Corollary 2.27, 𝔊 contains only one point.

Suppose now that n > 0. By the induction hypothesis and Lemma 5.40, there are finitely many tableaux (Γ, Δ) in 𝔊 such that p ∈ Γ, for some atomic p ∈ Ξ_{n}. (The variables may be renamed to use Lemma 5.40.) So it is sufficient to show that there is a finite number of tableaux t = (Γ, Δ) in 𝔊 containing all p_{1}, …, p_{n} in Δ. By Lemma 5.39, every such point t has no predecessors in 𝔊. And by Generation Theorem and the fact that all p_{i} are in Δ, t is uniquely determined by the set of its proper successors in 𝔊. Since, as we have already established, only a finite number of such sets exists, there are only finitely many distinct t = (Γ, Δ) with p_{1}, …, p_{n} ∈ Δ. □

It is not difficult now to complete the proof of Diego’s Theorem. Since 𝔊 characterizes Ξ_{n}, for any φ, ψ ∈ Ξ_{n} we have φ ↔ ψ ∈ Int iff for every (Γ, Δ) in 𝔊, φ and ψ simultaneously belong either to Γ or to Δ. Ergo the number of pairwise non-equivalent in Int disjunction free formulas built from ⊥, p_{1}, …, p_{n} is not greater than the number of subsets in V, that is 2^{|V |}. □

As a direct consequence of Diego’s Theorem we obtain Corollary 5.42 Suppose Σ is a finite set of intuitionistic formulas. Then the closure of Σ under ∧, → and ⊥ contains finitely many pairwise non-equivalent in Int formulas and so is finitely based over any intuitionistic model.

We take advantage of this result to establish the finite approximability of the Kreisel–Putnam logic KP. In Section 7.3 we shall use it to prove the finite approximability of an infinite family of si-logics.

Theorem 5.43 The Kreisel–Putnam logic

KP = Int + (¬p → q ∨ r) → (¬p → q) ∨ (¬p → r)

admits filtration and so is finitely approximable and decidable.

Proof Suppose φ ∉ KP and 𝔐 is a model for KP refuting φ. Let Σ be the closure of Subφ under →, ∧ and ⊥ and Δ a finite base of Σ over 𝔐. Construct the coarsest filtration 𝔑 = ⟨𝔊, 𝔘⟩ of 𝔐 through Σ. By Proposition 5.24, Corollary 5.42 and Filtration Theorem, 𝔑 is a finite countermodel for φ.

To prove that 𝔊 = ⟨V, S⟩ is a frame for KP, we show that it satisfies the firstorder condition corresponding to kp in Exercise 2.8. Suppose otherwise. Since 𝔊 is finite, we then have points [x], [y], [z] ∈ V such that [x]S[y], [x]S[z], [y] and [z] do not see each other and every successor [u] of [x], seeing both [y] and [z] (in particular [x] itself), sees a final point [w] in 𝔊, which is not accessible from [y] and [z]. Let [w_{1}], …, [w_{n}] be all the final points in 𝔊 that are seen from [x] and are not seen from [y] and [z]. According to our assumption, n > 0.

For a point [v] ∈ V, denote by γ_{v} the conjunction of all the formulas in Δ that are true at [v] and by δ_{v} the disjunction of those formulas in Δ that are false at [v] in 𝔑. Put γ = ⋁_{i=1}^{n} γ_{w_{i}} and consider the following substitution instance of kp:

κ = (¬γ → δ_{y} ∨ δ_{z}) → (¬γ → δ_{y}) ∨ (¬γ → δ_{z}).

Since 𝔐 ⊧ KP, we have (𝔐, x) ⊧ κ. Also we must have x |̸= ¬γ → δ_{y} and x |̸= ¬γ → δ_{z}. Indeed, if for instance x ⊧ ¬γ → ⋁_{i} ψ_{i} where ψ_{i} are the formulas in Δ that are false at [y], then by using kp a sufficient number of times we obtain that x ⊧ ⋁_{i}(¬γ → ψ_{i}) and so x ⊧ ¬γ → ψ_{i}, for some i. And since ¬γ is equivalent in Int to ⋀_{i=1}^{n} ¬γ_{w_{i}} ∈ Σ, we conclude by Filtration Theorem that [x] ⊧ ¬γ → ψ_{i}. On the other hand, we have [y] ⊧ ¬γ, for otherwise there is a point [v] accessible from [y] and such that [v] ⊧ γ_{w_{i}}, for some i, and so [w_{i}]S[v], which is possible only when [w_{i}] = [v], since [w_{i}] is final in 𝔊. It follows that [y] ⊧ ψ_{i}, which is a contradiction.

Therefore, x |̸= ¬γ → δ_{y} ∨ δ_{z} and so there is u ∈ x↑ such that u ⊧ ¬γ and u |̸= δ_{y} ∨ δ_{z}. Then [x]S[u], [u] ⊧ ¬γ and [u] |̸= δ_{y} ∨ δ_{z}, from which [u]S[y] and [u]S[z], since 𝔑 is the coarsest filtration of 𝔐,. Take a point [w_{i}] ∈ [u]↑. Clearly [w_{i}] ⊧ γ_{w_{i}} and so [u] |̸= ¬γ_{w_{i}}, contrary to [u] ⊧ ⋀_{i=1}^{n} ¬γ_{w_{i}}. □

Remark In Section 19.2 we shall show that there are formulas φ ∉ KP whose smallest refutation frames validating KP contain at least 2^{2^{|Subφ|}} points. This means that by filtrating 𝔐 through Subφ we could not establish the finite approximability of KP.

5.5 Selective filtration

If we want to use the filtration method for establishing the finite approximability of a logic L without knowing any non-trivial completeness results for it, we have no other choice but to filtrate the canonical model 𝔐_{L} through some set of formulas Σ. However, this may yield no result no matter what Σ we choose, even if L is really finitely approximable. For example, as we shall see below, GL is characterized by the class of finite strict orders, but the canonical frame 𝔉_{GL} contains a reflexive point, and so by (iii) in Section 5.3, every filtration of 𝔐_{GL} has a reflexive point as well.

When filtrating a model or better a Hintikka system ℌ through Σ, we divide the tableaux in ℌ into Σ-equivalence classes, identify the tableaux in each class and try to project the accessibility relation in ℌ to the resulting finite set of tableaux so that we again could obtain a Hintikka system. Yet there is another way of constructing finite Hintikka systems starting from ℌ: instead of factorizing ℌ we may try to extract a finite subsystem of ℌ by selecting some suitable points in the Σ-equivalence classes in accordance with the rules for constructing Hintikka systems. This method is known as selective filtration. We use it here to establish the finite approximability of GL, Grz and T_{n}. (By the way, none of these logics, except T_{1}, is canonical.)

A general scheme of selective filtration, which will be enough for our purposes, may be described as follows. Suppose L is a modal or superintuitionistic logic and φ ∉ L. Then there is a model 𝔐 = ⟨𝔉, 𝔙⟩ separating φ from L, i.e., 𝔐 |̸= φ and 𝔐 ⊧ L. Suppose also that Σ is a finitely based over 𝔐 set of formulas containing φ and closed under subformulas. We may think of 𝔉 as the Hintikka system 𝔉 = ⟨W, R⟩, with points t ∈ W being the tableaux t = (Γ, Δ) where

Γ = {ψ ∈ Σ : (𝔐, t) ⊧ ψ}, Δ = {ψ ∈ Σ : (𝔐, t) |̸= ψ}.

We start our selective filtration of 𝔐 through Σ with selecting a tableau t = (Γ, Δ) in W such that φ ∈ Δ. The tableau t will be the root of the finite Hintikka system we are going to extract from 𝔐. It may turn out that the pair ℌ = ⟨T, S⟩, where T = {t} and S is the restriction of R to T, is already a Hintikka system. In this situation we are done. Otherwise there are formulas □ψ ∈ Δ (ψ → χ ∈ Δ, in the intuitionistic case) such that either ψ ∉ Δ or not tSt (respectively, ψ ∉ Γ). Denote by Θ_{t} the set of all formulas of that sort. Now, at the second step for each □ψ ∈ Θ_{t} (respectively, ψ → χ ∈ Θ_{t}), we select a tableau t′ = (Γ′, Δ′) in W such that tRt′ and ψ ∈ Δ′ (respectively, ψ ∈ Γ′ and χ ∈ Δ′). Denote by T_{t} the set of all selected successors of t. Then we add T_{t} to T, thus obtaining a set T′, take the restriction S′ of R to T′ and check whether ℌ′ = ⟨T′, S′⟩ is a Hintikka system. If this is not the case then, for each t′ ∈ T_{t}, we consider formulas in Θ_{t′}, select a set T_{t′} of suitable successors of t′, add it to T′, and so on till we reach tableaux t^{∗} with Θ_{t^{∗}} = ∅. If we succeed then the resulting Hintikka system ℌ^{∗} = ⟨T^{∗}, S^{∗}⟩ will certainly refute φ.

Two points are essential in this construction. First, we must ensure somehow that the process will eventually terminate. For example, we may try to select successors t′ of each tableau t in such a way that Θ_{t′} contains less formulas than Θ_{t}. And second, to separate φ from L, ℌ^{∗} must be a frame for L. In that respect the definition of the accessibility relation in ℌ^{∗} as the restriction of R to T^{∗} may be too severe. For in fact, to obtain a Hintikka system, it is sufficient to define on T^{∗} any relation S in the interval S_{∗} ⊆ S ⊆ S^{∗}, where tS_{∗}t′ iff either t = t′ and tRt′ or t′ ∈ T_{t} (of course, in the intuitionistic case S must be a partial order).

We apply now this scheme to prove the finite approximability of

GL = K4 ⊕ □(□p → p) → □p.

Using the selective filtration, we will extract from the canonical model 𝔐_{GL} a finite submodel that refutes φ ∉ GL and contains only irreflexive points, which, by Proposition 3.47, is enough to ensure that the model validates the Löb axiom la.

The following observation is the key to the filtration. Lemma 5.44 Suppose x |̸= □ψ for some point x in a model 𝔐 for GL. Then there is an (irreflexive) point y ∈ x↑ such that y |̸= ψ and y ⊧ □ψ.

Proof Since every substitution instance of la is true in 𝔐, we have x ⊧ □(□ψ → ψ) → □ψ. Therefore, x |̸= □(□ψ → ψ) and so there is y ∈ x↑ such that y ⊧ □ψ and y |̸= ψ. Clearly, y is irreflexive. □

Theorem 5.45 GL is characterized by the class of finite strict orders.

Proof It suffices to show that every formula φ ∉ GL is refuted by some finite strict order 𝔊 = ⟨V, S⟩. We construct it according to the scheme above by filtrating 𝔐_{GL} through Σ = Subφ.

Observe first that there is an irreflexive point x_{0} in 𝔐_{GL} such that x_{0} |̸= φ. For there must be x in 𝔐_{GL} refuting φ, and if x is reflexive then x |̸= □φ and we can use Lemma 5.44.

We define 𝔊 by induction. Put V_{0} = {x_{0}} and Θ_{x_{0}} = {□ψ ∈ Σ : x_{0} |̸= □ψ}. Suppose now that V_{n} = {x_{1}, …, x_{m}} has been already constructed. If Θ_{x_{i}} = ∅ for all i = 1, …, m, then let V = ⋃_{j=0}^{n} V_{j} and S be the restriction of R_{GL} to V. Otherwise, for each x_{i} with Θ_{x_{i}} ≠ ∅ and each □ψ ∈ Θ_{x_{i}}, we select according to Lemma 5.44 an irreflexive point y ∈ x_{i}↑ such that y |̸= ψ and y ⊧ □ψ. Let V_{n+1} be the set of the selected points y.

Since |Θ_{y}| < |Θ_{x_{i}}| (because 𝔉_{GL} is transitive) and Σ is finite, we must eventually reach a set V_{n} whose points validate all the boxed formulas in Σ, i.e., Θ_{x} = ∅ for every x ∈ V_{n}. By the construction, 𝔊 is a strict order and 𝔊 |̸= φ. □

Corollary 5.46 (i) GL is characterized by the class of Noetherian strict orders. (ii) GL is characterized by the class of finite strictly ordered trees.

Proof Follows from Theorem 5.45, Proposition 3.47, Exercise 3.18 and Reduction Theorem. □

It is somewhat more difficult to prove the finite approximability of the Grzegorczyk logic

Grz = K ⊕ □(□(p → □p) → p) → p.

First we observe that the canonical frame for Grz satisfies two good properties:

Proposition 5.47 𝔉_{Grz} is reflexive and transitive.

Proof Suppose there is x in 𝔉_{Grz} such that x ∉ x ↑. By the definition of canonical model, this means that x ⊧ □φ and x |̸= φ, for some formula φ. But then x |̸= □(□(φ → □φ) → φ) → φ, contrary to 𝔐_{Grz} ⊧ Grz. Thus, 𝔐_{Grz} is reflexive.

Now let us prove that □p → □□p ∈ Grz. By Theorem 5.16, it will follow that 𝔉_{Grz} is transitive. Suppose otherwise. Then x |̸= □p → □□p and so x |̸= φ = (p∧ ¬□p) ∨ □□p, for some x in 𝔐_{Grz}. We will show that x ⊧ □(□(φ → □φ) → φ).

Suppose this is not the case. Then there exists y ∈ x↑ such that y ⊧ □(φ → □φ), y ⊧ □p and y |̸= □□p (for if y |̸= p then x |̸= □p, which is a contradiction). Besides, there is z ∈ y↑ for which z ⊧ φ → □φ, z ⊧ p and z |̸= □p. Therefore, z ⊧ φ and z ⊧ □φ. Now we have u ∈ z ↑ such that u ⊧ (p ∧ ¬□p) ∨ □□p and u |̸= p. By the reflexivity, u |̸= □□p and hence u ⊧ p ∧ ¬□p, which is a contradiction.

Thus x |̸= □(□(φ → □φ) → φ) → φ, contrary to 𝔐_{Grz} being a model for Grz. □

Corollary 5.48 Grz = K4 ⊕ grz = S4 ⊕ grz.

According to Proposition 3.48, to establish the finite approximability of Grz, given a formula φ ∉ Grz, we need to extract from 𝔐_{Grz} a finite partially ordered countermodel for φ. The following lemma shows in particular that when filtrating 𝔐_{Grz} through Σ = Subφ we may choose successors of a point x in clusters different from C(x). And if two or more successors appear in the same non-degenerate cluster, we simply shall not take into account the accessibility relation between them.

Lemma 5.49 Suppose □ψ ∈ Σ, x ⊧ ψ and x |̸= □ψ, for some point x in 𝔐_{Grz}. Then there is a point y ∈ x↑ such that y |̸= ψ and z ∼_{Σ} x for no z ∈ y↑.

Proof Suppose otherwise. Then for every y ∈ x↑ such that y |̸= ψ, there is a point z ∈ y↑ which is Σ-equivalent to x and so z ⊧ ψ and z |̸= □ψ. It follows that x ⊧ □(□(ψ → □ψ) → ψ).

Since x |̸= □ψ, there is y ∈ x↑ such that y |̸= ψ, and since 𝔉_{Grz} is transitive, y ⊧ □(□(ψ → □ψ) → ψ), contrary to 𝔐_{Grz} ⊧ Grz. □

We are in a position now to prove

Theorem 5.50 Grz is determined by the class of finite partial orders.

Proof Given a formula φ ∉ Grz, take Σ = Subφ and use the selective filtration through Σ to extract from 𝔐_{Grz} a finite partially ordered frame 𝔊 = ⟨V, S⟩ refuting φ. We construct 𝔊 by induction.

To begin with, we take some point x in 𝔐_{Grz} such that x |̸= φ and put 𝔊_{0} = ⟨V_{0}, S_{0}⟩, where V_{0} = {x}, S_{0} = {⟨x, x⟩}, and Θ_{x} = {□ψ ∈ Σ : x |̸= □ψ and x ⊧ ψ}. Suppose now that we have already constructed a partially ordered frame 𝔊_{n} = ⟨V_{n}, S_{n}⟩ with V_{n} ⊆ W_{Grz}, S_{n} ⊆ R_{Grz}. Let X_{n} be the set of final points x in 𝔊_{n} such that Θ_{x} ≠ ∅. If X_{n} = ∅ then put 𝔊 = 𝔊_{n}. Otherwise for each x ∈ X_{n} and each □ψ ∈ Θ_{x}, fix a point y(x, □ψ) ∈ x ↑ such that y(x, □ψ) |̸= ψ and ¬∃z ∈ y(x, □ψ)↑ z ∼_{Σ} x (that such a point exists is guaranteed by Lemma 5.49). Put

V_{n+1} = V_{n} ∪ {y(x, □ψ) : x ∈ X_{n} and □ψ ∈ Θ_{x}},

define S_{n+1} as the reflexive and transitive closure of the relation

S_{n} ∪ {⟨x, y(x, □ψ)⟩ : x ∈ X_{n} and □ψ ∈ Θ_{n}}

and let 𝔊_{n+1} = ⟨V_{n+1}, S_{n+1}⟩. It should be clear that S_{n+1} ⊆ R_{Grz} (but S_{n+1} is not in general the restriction of R_{Grz} to V_{n+1}).

Notice that 𝔊_{n+1} is a partial order. Indeed, otherwise we would have a cluster in 𝔊_{n+1} containing both x and y(x, □ψ), for some x ∈ X_{n} and □ψ ∈ Θ_{x}. But then y(x, □ψ)R_{Grz}x, contrary to our choice of y(x, □ψ).

Since no chain in 𝔊_{n+1} contains distinct Σ-equivalent points and since Σ is finite, at some step m we shall have X_{m} = ∅, and so our selection process will terminate. If we regard points x in 𝔊 as the tableaux t_{x} = (Γ_{x}, Δ_{x}) with Γ_{x} = {ψ ∈ Σ : (𝔐_{Grz}, x) ⊧ ψ} and Δ_{x} = {ψ ∈ Σ : (𝔐_{Grz}, x) |̸= ψ}, then 𝔊 will clearly be a Hintikka system. Therefore, 𝔊 |̸= φ. □

Corollary 5.51 (i) Grz is characterized by the class of Noetherian partial orders.

(ii) Grz is characterized by the class of finite partially ordered trees.

Proof Follows from Theorems 5.50, 2.19 and Proposition 3.48. □

Let us consider now the si-logics

T_{n} = Int + ⋀_{i=0}^{n}((p_{i} → ⋁_{i≠j} p_{j}) → ⋁_{i≠j} p_{j}) → ⋁_{i=0}^{n} p_{i}, for n ≥ 1,

and prove that all of them are finitely approximable. By Proposition 2.41, T_{n} is sound with respect to the class of finite frames of branching ≤ n. We shall use the selective filtration to show that T_{n} is also complete with respect to this class.

Theorem 5.52 T_{n} is characterized by the class of finite frames of branching ≤ n.

Proof Suppose φ ∉ T_{n} and 𝔐 = ⟨𝔉, 𝔙⟩ is a model for T_{n} refuting φ. By Theorem 2.19 and Reduction Theorem, without loss of generality we may assume that 𝔉 = ⟨W, R⟩ is a tree. Let Σ = Subφ and Γ_{x} = {ψ ∈ Σ : x ⊧ ψ}, for every point x in 𝔉.

Given x in 𝔉, put rg(x) = {[y] : y ∈ x↑} and say that x is of minimal range if rg(x) = rg(y) for every y ∈ [x] ∩ x↑. Since there are only finitely many distinct Σ-equivalent classes in 𝔐, every y ∈ [x] sees a point z ∈ [x] of minimal range.

We are in a position now to extract from 𝔐 a finite refutation frame 𝔊 = ⟨V, S⟩ for φ of branching ≤ n. To begin with, we select some point x of minimal range at which φ is refuted and put V_{0} = {x}.

Suppose now that V_{k} has already been defined. If |rg(x)| = 1 for every x ∈ V_{k}, then we put 𝔊 = ⟨V, S⟩ where V = ⋃_{i=0}^{k} V_{k} and S is the restriction of R to V. Otherwise, for each x ∈ V_{k} with |rg(x)| > 1 and each [y] ∈ rg(x) different from [x] and such that Γ_{z} ⊂ Γ_{y} for no [z] ∈ rg(x) − {[x]}, we select a point u ∈ [y] ∩ x↑ of minimal range. Let U_{x} be the set of all the selected points for x and V_{k+1} = ⋃_{x} U_{x}. It should be clear that Γ_{x} ⊂ Γ_{u} (and rg(x) ⊃ rg(u)), for every u ∈ U_{x}, and so the inductive process must terminate. Using the standard tableau argument one can readily show also that 𝔊 |̸= φ.

It remains to establish that 𝔊 ⊧ T_{n}, i.e., 𝔊 is of branching ≤ n. Suppose otherwise. Then there is a point x in 𝔊 with at least n + 1 immediate successors x_{0}, …, x_{n}, which are evidently in U_{x} because 𝔊 is a tree. We are going to construct a substitution instance of T_{n}’s axiom bb_{n} which is refuted at x in 𝔐.

Denote by χ_{i} the conjunction of the formulas in Γ_{x_{i}}. Since all of them are true at x_{i} in 𝔐, we have x_{i} ⊧ χ_{i}; and since Γ_{i} ⊆ Γ_{j} for no distinct i and j, we have x_{j} |̸= χ_{i} if i ≠ j. Let us consider now the truth-value of the formula ψ = bb_{n}{χ_{0}/p_{0}, …, χ_{n}/p_{n}} at x in 𝔐.

Since xRx_{i} for every i = 0, …, n, we have x |̸= ⋁_{i=0}^{n} χ_{i}. Suppose that x |̸= ⋀_{i=0}^{n}((χ_{i} → ⋁_{i≠j} χ_{j}) → ⋁_{i≠j} χ_{j}). Then y ⊧ χ_{i} → ⋁_{i≠j} χ_{j} and y |̸= ⋁_{i≠j} χ_{j}, for some y ∈ x↑ and some i ∈ {0, …, n}, and hence y |̸= χ_{i}. Since x_{i} ⊧ χ_{i} and x_{i} |̸= ⋁_{i≠j} χ_{j}, y sees no points in [x_{i}] and so y ≁_{Σ} x (for otherwise x would not be of minimal range). Therefore, Γ_{x_{j}} ⊆ Γ_{y} for some j ∈ {0, …, n}, and then y ⊧ χ_{j}, which is a contradiction.

It follows that x ⊧ ⋀_{i=0}^{n}((χ_{i} → ⋁_{i≠j} χ_{j}) → ⋁_{i≠j} χ_{j}), from which x |̸= ψ, contrary to 𝔐 being a model for bb_{n}. □

As a consequence of Theorem 5.52 we obtain the following completeness result justifying, by the way, the name T_{n} of the logics under consideration.

Corollary 5.53 T_{n} is characterized by the class of finite n-ary trees.

Proof Exercise (use Reduction Theorem and Exercise 2.5). □

5.6 Kripke semantics for quasi-normal logics The Kripke semantics for modal logics we have dealt with so far is suitable only for normal extensions of K. Now we use the concept of canonical model to introduce in a rather natural way a Kripke semantics for all logics in ExtK, including quasi-normal ones.

Suppose L is a consistent quasi-normal logic. Then the set of formulas

M = {φ ∈ ForML : ∀n ≥ 0 □^{n}φ ∈ L}

is clearly a normal logic, the greatest one among all normal logics contained in L, to be more exact. We call M the kernel of L and denote it by ker L.

Let 𝔐_{M} = ⟨𝔉_{M}, 𝔙_{M}⟩ be the canonical model for M. Each maximal Lconsistent tableau t is also a maximal M-consistent tableau, and so t is a point in 𝔉_{M}. Denote by D_{L} the set of all maximal L-consistent tableaux. Then by Lemma 5.2 which, as we observed, holds for quasi-normal logics as well, we have

Λ ⊢_{L} φ iff for every (Γ, Δ) ∈ D_{L}, Λ ⊆ Γ implies φ ∈ Γ.

Therefore, by Theorem 5.4, for any Λ and φ,

Λ ⊢_{L} φ iff for every t ∈ D_{L}, (𝔐_{M}, t) ⊧ Λ implies (𝔐_{M}, t) ⊧ φ.

Of course, instead of M we can take any other normal logic contained in L.

This result can be interpreted as follows. We distinguish in 𝔐_{M} a set of points, namely D_{L}, and regard them as the only “actual worlds” in 𝔐_{M}. A formula φ is then assumed to be true in 𝔐_{M} if it is true at all the actual worlds.

Thus we arrive at the following Kripke semantics for quasi-normal logics. A Kripke frame with distinguished points is a pair ⟨𝔉, D⟩ where 𝔉 = ⟨W, R⟩ is

a Kripke frame and D ⊆ W. The points in D are called the distinguished points or the actual worlds in 𝔉. A model with distinguished points (based on ⟨𝔉, D⟩) is a pair ⟨𝔐, D⟩ where 𝔐 = ⟨𝔉, 𝔙⟩ is an ordinary Kripke model based on 𝔉. A formula φ is said to be true in ⟨𝔐, D⟩ (notation: ⟨𝔐, D⟩ ⊧ φ) if (𝔐, x) ⊧ φ for all x ∈ D. φ is valid in ⟨𝔉, D⟩ (notation: ⟨𝔉, D⟩ ⊧ φ) if φ is true in all models based on ⟨𝔉, D⟩.

Clearly, 𝔉 ⊧ φ iff ⟨𝔉, W ⟩ ⊧ φ, so a frame 𝔉 may be identified with ⟨𝔉, W ⟩. As to the other extreme case, it follows from the definition that all formulas, even ⊥, are valid in ⟨𝔉, ∅⟩.

The model ⟨𝔐_{ker L}, D_{L}⟩ and the frame ⟨𝔉_{ker L}, D_{L}⟩, constructed at the beginning of this section, are called the canonical model and the canonical frame (with distinguished points) for L, respectively.

What we have established so far can be summarized as the following

Theorem 5.54 Each consistent quasi-normal logic L is strongly characterized by its canonical model ⟨𝔐_{ker L}, D_{L}⟩, i.e., for every Λ and φ,

Λ ⊢_{L} φ iff ∀x ∈ D_{L} x ⊧ Λ → x ⊧ φ,

[figure: ∘; ∘; ∘; 1; ∘; 𝔉; 0; (a); ∘; •; •; •; ⋮; (b); 0; 1; 2; ω; 𝔊] Fig. 5.1.

in particular,

φ ∈ L iff ⟨𝔐_{ker L}, D_{L}⟩ ⊧ φ.

It is worth noting that a formula φ is true in ⟨𝔐, D⟩ iff φ is true in every model in the class {⟨𝔐, {d}⟩ : d ∈ D}. So we obtain

Theorem 5.55 Every consistent quasi-normal logic is strongly characterized by a class of models having a single distinguished point.

Given a class C of frames with distinguished points, denote by LogC the set of modal formulas that are valid in all frames in C; if C = {⟨𝔉, D⟩} then we write simply Log⟨𝔉, D⟩. As an easy exercise we offer the reader to prove the following

Proposition 5.56 For every class C of frames with distinguished points, LogC is a quasi-normal logic.

To illustrate the introduced semantics for quasi-normal logics we give some examples.

Example 5.57 The first known quasi-normal, but not normal extension of S4 was

S4.1′ = S4 + □◇p → ◇□p.

To understand why S4.1′ is not normal, let us consider the frame 𝔉 shown in Fig. 5.1 (a) with actual world 0. Since 𝔉 does not satisfy the McKinsey condition, it refutes ma and so (𝔉, 0) |̸= □ma. However, ⟨𝔉, {0}⟩ ⊧ ma, for otherwise we would have (under some valuation) 1 |̸= ma, which is impossible. Therefore, S4.1′ ⊆ Log ⟨𝔉, {0}⟩. On the other hand, □ma ∉ Log ⟨𝔉, {0}⟩, which means that S4.1′ is not closed under necessitation.

Theorem 5.58. (Scroggs’ Theorem) All logics in ExtS5 are normal.

Proof It is enough to show that every extension L of S5(n) in the language with n variables is normal. According to Theorem 5.54, L is characterized by ⟨𝔐_{S5(n)}, D_{L}⟩, which in view of Corollary 5.19 is finite. By Exercise 5.4, L is then characterized by the frame ⟨𝔉_{S5(n)}, D_{L}⟩. Let 𝔉 be the subframe of 𝔉_{S5(n)} generated by D_{L}. Then L = Log ⟨𝔉, D_{L}⟩ and so, as is easy to see, L = Log𝔉. □ Example 5.59 As we observed in Section 3.8, there is no Kripke frame validating all formulas in Solovay’s logic

S = (K4 ⊕ □(□p → p) → □p) + □p → p.

It follows in particular that S has no consistent normal extensions. By the same reason no Kripke frame with distinguished points can validate S. Logics with this property may be called Kripke inconsistent. All consistent extensions of S, if any, are clearly Kripke inconsistent.

Moreover, there is no (normal) Kripke model for S. For by Lemma 5.44, every model 𝔐 for GL contains a final irreflexive point x. (Indeed, if y is not a dead end in 𝔐 then y |̸= □⊥ and so x ⊧ □⊥ for some x ∈ y↑.) But then x |̸= □⊥ → ⊥.

We construct now a model with a distinguished point for S, which shows by the way that S is consistent. Let 𝔊 = ⟨V, S⟩ be the (transitive) frame depicted in Fig. 5.1 (b), or formally

𝔊 = ⟨{i : i ≤ ω}, {⟨ω, ω⟩ , ⟨j, i⟩ : 0 ≤ i < j ≤ ω}⟩ .

Define a valuation 𝔘 in 𝔊 by taking 𝔘(p) = V, for every variable p. Observe first that all substitution instances of the Löb axiom are true in the (normal) model 𝔐 = ⟨𝔊, 𝔘⟩. Indeed, all of them are clearly true at all irreflexive points in 𝔐. As to ω, one can readily prove by induction on the construction of φ that if ω ⊧ φ (or ω |̸= φ) then there is some n < ω such that m ⊧ φ (respectively, m |̸= φ), for all m ∈ {n, n + 1, …, ω}. So if a substitution instance of the Löb axiom is false at ω then it is also false at some irreflexive point n which, as we know, is impossible.

Thus, 𝔐 ⊧ GL. Now, let us observe that (𝔐, ω) ⊧ □φ → φ, for every formula φ, simply because ω is reflexive. So if we distinguish ω as the only actual world in 𝔐 then we obtain that ⟨𝔐, {ω}⟩ ⊧ S.

We use this observation to prove the following

Theorem 5.60 For every modal formula φ,

φ ∈ S iff ⋀_{□ψ∈Subφ} (□ψ → ψ) → φ ∈ GL.

Proof The part (⇐) is evident. To prove (⇒), suppose

⋀_{□ψ∈Subφ} (□ψ → ψ) → φ ∉ GL.

Since GL is finitely approximable, this formula is refuted at the root x of some finite frame 𝔉 = ⟨W, R⟩ for GL under some valuation. Construct a new frame 𝔊 by adding to 𝔉 the infinite chain depicted in Fig. 5.1 (b) so that it could see all points in 𝔉 and define a valuation in 𝔊 in such a way that the truth-value of each variable remains the same at all points in 𝔉 and at points in the added chain it coincides with that at x. By induction on the construction of χ ∈ Subφ and using the fact that x ⊧ ⋀_{□ψ∈Subφ} (□ψ → ψ) one can show that y ⊧ χ iff x ⊧ χ. Since the root of 𝔊 is reflexive, it follows that ⋀_{□ψ∈Subφ} (□ψ → ψ) → φ is false at it. And that la is true there is checked in the same way as in Example 5.59. □

5.7 Exercises Exercise 5.1 Prove that every variable free formula is equivalent in D either to ⊤ or to ⊥.

Exercise 5.2 Show that K ⊕ ma = D ⊕ ma.

Exercise 5.3 Construct modal and intuitionistic models that are not differentiated (tight, compact).

Exercise 5.4 Show that if 𝔐 = ⟨𝔉, 𝔙⟩ is differentiated finite model for a logic L then 𝔉 is a frame for L.

Exercise 5.5 Show that GL.3 = GL ⊕ con is characterized by the class of finite linear strict orders and by the frame ⟨ω, >⟩.

Exercise 5.6 Show that K4Z = K4 ⊕ z is characterized by the class consisting of finite irreflexive frames and balloons.

Exercise 5.7 Show that D4Z.3 = D4 ⊕ z ⊕ con is characterized by the frame ⟨ω, <⟩.

Exercise 5.8 Show that Dum = S4 ⊕ dum is characterized by the class consisting of finite partial orders and reflexive balloons.

Exercise 5.9 Show that Grz.3 = Grz⊕sc is characterized by the frame ⟨ω, ≥⟩.

Exercise 5.10 Show that Dum.3 = Dum ⊕ sc is characterized by the frame ⟨ω, ≤⟩.

Exercise 5.11 (i) Show that frames for K5 are 3–transitive.

(ii) Prove that there are finitely many pairwise non-equivalent modalities in K5.

(iii) Prove that all logics in NExtK5 are locally tabular and finitely axiomatizable.

Exercise 5.12 Show that D4G_{1} is finitely approximable.

Exercise 5.13 Show that both S4.1 and S4.2 have exactly 10 pairwise nonequivalent modalities.

Exercise 5.14 Show that Int = ⋂_{i≥1} T_{n} and that

Int ⊂ … ⊂ T_{n} ⊂ … ⊂ T_{2} ⊂ T_{1}.

Exercise 5.15 Prove that each T_{n}, for n ≥ 2, has the disjunction property.

Exercise 5.16 Prove that all logics in NExtAlt_{1} are finitely approximable. Exercise 5.17 Prove that there are at most 2^{n} pairwise nonequivalent in Int disjunction free formulas of variables p_{1}, …, p_{n}. Exercise 5.18 Show that Log⟨𝔉, D⟩ = ⋂_{x∈D} Log ⟨𝔉, {x}⟩. Exercise 5.19 Show that K4 = ⋂_{n≥1} K4B_{n}. Exercise 5.20 Prove that Alt_{3} ⊕ re ⊕ sym has infinitely many non-equivalent modalities. (Segerberg (1971) conjectures that no proper normal extension of Alt_{3} ⊕ re ⊕ sym has this property.) Exercise 5.21 Show that K4H = K4 ⊕ p → □(◇p → p) is canonical, with its canonical frame satisfying the condition

xRy ∧ yRz → x = y ∨ y = z.

Prove that every L ∈ NExtK4H is finitely approximable. Exercise 5.22 Show that S4 ⊕ □◇p → (p → □p) is characterized by the class of quasi-orders satisfying the condition

x ≠ z ∧ xRz ∧ xRy → yRz.

Exercise 5.23 Show that S4 ⊕ □(□p → q) ∨ (◇□q → p) is characterized by the class of quasi-orders satisfying the condition

xRz ∧ ¬zRx ∧ xRy → yRz.

Exercise 5.24 Show that □(p → q) → (□p → ◇q) ∈ D. Exercise 5.25 Prove that if a normal modal logic L contains the formula hin of Exercise 3.15 then 𝔉_{L} satisfies the first order condition in Exercise 3.15. Exercise 5.26 Show that no distinct modalities are equivalent in T and K ⊕ ◇p → □p. Derive from this that there are at least two maximal logics in NExtK in which no distinct modalities are equivalent. Exercise 5.27 Show that the logic S4 + ◇grz is not normal. Exercise 5.28 Prove that (i) NExtS4.3 = ExtS4.3,

(ii) NExt(S4.2 ⊕ bd_{3}) = Ext(S4.2 ⊕ bd_{3}) and (iii) NExt(S4 ⊕ bd_{2}) ≠ Ext(S4 ⊕ bd_{2}).

Exercise 5.29 Show that the reflexive point in the frame considered in Example 5.59 can be replaced by an irreflexive one. Exercise 5.30 Show that ker L in Theorem 5.54 can be replaced with any normal logic L′ ⊆ L (for instance, K). Exercise 5.31 Show that KP ⊆ ML.

5.8 Notes The construction of the canonical models is conceptually close to that used in the Henkin–style completeness proofs for classical first and second order calculi (see (Church 1956) and (Chang and Keisler 1990)) and to the Tarski–Lindenbaum algebras (see Chapter 7). The method of canonical models was introduced by Lemmon and Scott (1977)^{7} and Makinson (1966); cf. also (Cresswell 1967) and (Schütte 1968). The canonical model of (Lemmon and Scott 1977) seems to have its roots in the relational representation of Boolean algebras with modal operators (in particular, the Tarski–Lindenbaum algebras for modal logics), studied by Lemmon (1966a, 1966b). The canonical model of (Makinson 1966) is an “improvement” of the tableau construction of (Kripke 1963). Perhaps these different sources explain why Lemmon and Scott (1977) introduce the filtration method, while the construction of the canonical model in (Makinson 1966) is combined with selecting (using a sort of selective filtration) from it a countable submodel, which gives an analog of Löwenheim–Skolem’s Theorem (see Theorem 6.29). Approximately at the same time the canonical model for intuitionistic (predicate) logic was constructed by Aczel (1968), Fitting (1969) and Thomason (1969).

The method of canonical models turned out to be a powerful tool in nonclassical logic. It was applied systematically to prove completeness theorems for a good many normal modal logics by Lemmon and Scott (1977), who obtained in particular Corollary 5.22 and the result of Exercise 5.25, and by Segerberg (1971). Routley (1970) extended the ideas of Makinson (1966) to wide classes of weak modal systems. Rennie (1970) noticed that the method of canonical models works for multi-modal logics too. Smorinski (1973) used it for si-logics. Later the method was applied to a great many other types of logics; see for instance (Goldblatt 1982) and (Segerberg 1994).

The filtration method was introduced simultaneously with the canonical models by Lemmon and Scott (1977); Filtration Theorem is due to Segerberg (1968). However, the algebraic variant of filtration goes back to McKinsey (1941) and Lemmon (1966a, 1966b). In modal logic various forms of filtration were widely used by Bull (1967), Segerberg (1968, 1971), Gabbay (1970b, 1972, 1976) who developed selective filtrations, Nagle and Thomason (1985), Shehtman (1990) and many others. Smorinski (1973), Gabbay (1970a), Ono (1972), Gabbay and de Jongh (1974), Ferrari and Miglioli (1993) and others applied it to si-logics. The results and proofs concerning the finite approximability, presented in this chapter, were taken from the cited papers and books. Diego’s Theorem was first proved in (Diego 1966); the proof above is due to Urquhart (1974). Sobolev (1977b) somewhat generalized Diego’s Theorem and used it to establish the finite approximability of a wide class of si-logics. Unfortunately, even the formulation of this result is too complicated to be presented here. A consequence of Sobolev’s Theorem—that all si-logics with extra axioms in one variable are finitely approximable—will be proved by another method in Section 11.6. An interesting result was obtained by Drugush (1984): using a variant of selective

7This book was written in 1966.

filtration of (Gabbay and de Jongh 1974) he proved that every si-logic characterized by a class of trees is finitely approximable. Note also that according to Drugush (1982) the union of si-logics characterized by finite trees is determined by finite trees too, i.e., the family of such logics is a sublattice of ExtInt.

The semantics for quasi-normal modal logics was developed by Segerberg (1971). Scroggs’s Theorem appeared in (Scroggs 1951) and Theorem 5.60 was first proved by Solovay (1976).

Quite recently Shehtman has proved that every Kripke complete si-logic and every logic in NExtS4 characterized by partially ordered Kripke frames is strongly complete with respect to the neighborhood semantics.