Well, first, a Merry Christmas and a Happy New Year!
Let L be a bounded distributive lattice. Given any element u of L, and any element v of L such that u≰v, there is a (join-)prime filter containing u and that does not contain v. That is an easy application of Zorn’s Lemma. We consider the set Filt(L) of filters in L, ordered by inclusion. This is a dcpo, where directed suprema are computed as unions. The subset of those filters F ∈ Filt(L) such that u ∈ F and v ∉ F is closed under those directed suprema, hence has a maximal element (Zorn). Let us call that maximal element F. That F is prime is a standard exercise, using the fact that L is distributive in a crucial way. (Exercise!)
Can we ask more properties of that prime filter F? For example, can we ask it to be Scott-open?
Spatial frames
If L is a complete distributive lattice, then a prime, Scott-open filter is a completely prime filter, namely a point of F, or again, an element of the space pt(L) obtained through Stone duality from L. Proposition 8.1.17 of the book says that we can indeed require F to be Scott-open (and prime, containing u but not v) provided L is a spatial frame. In fact, when L is a frame, it is equivalent to require that all pairs of elements u≰v of L are separated by a prime, Scott-open filter F (u ∈ F and v ∉ F) and to require that L be spatial.
But what happens when L is not spatial, or when L is not even complete?
The Rasiowa-Sikorski Lemma
The Rasiowa-Sikorski Lemma [1] states that, if L is a Boolean algebra, then for every pair u≰v in L, one can find a prime filter F separating u and v and satisfying a local form of Scott-openness.
Hence, as promised, we no longer assume L to be complete. Requiring L to be a Boolean algebra is more demanding than being just a bounded distributive lattice, but we will see later that this is not required.
Here is what this local form of Scott-openness is. A sup situation is a family D of elements of L that has a supremum sup D in L. (In a Boolean algebra, we cannot assume that all families, even just directed families, have a supremum.) F respects the sup situation D if and only if (sup D ∈ F implies that some element of D is in F). Hence F is Scott-open if and only if it respects every directed sup situation. F is completely prime if and only if it respects every sup situation.
The Rasiowa-Sikorski Lemma states that, given any countable family of sup situations in a Boolean algebra L, we can require the prime filter F separating u and v to respect all the sup situations from that countable family. That is crucial in the applications to logic that Rasiowa and Sikorski were interested in, and I will say a brief word about it in the next section.
In the meantime, notice that this is yet another case where countability enters the stage in a surprising way.
The surprise should dwindle down once you realize that the Rasiowa-Sikorski Lemma is a consequence of the Baire property, as realized by R. Goldblatt [2]… and I will explain how this works.
First-order logic
Please allow me not to be overly explicit here. This is not a blog on logic, and I wish to shy away from the technical details unrelated to topology. I assume you all know what a formula is. The formulae of first-order logic are built from so-called atomic formulae P(t1,…,tn) (where P is a so-called predicate symbol of arity n, and t1,…,tn are so-called terms) using conjunction ⋀, disjunction ⋁, negation ¬, truth ⊤, falsity ⊥, universal quantification ∀ and existential quantification ∃. Terms are built from variables and applications f(t1,…,tn) (where f is a so-called function symbol of arity n, and t1,…,tn are terms, recursively). A sentence is a formulae whose variables are all quantified. For example, ∀x.∃y.P(x,y) is a sentence, and ∃y.P(x,y) is a formula that is not a sentence.
I will assume that there are at most countably many predicate symbols and function symbols. This entails that there are only countably many sentences.
Importantly, formulae have no meaning per se. They are just inert pieces of syntax. To give a meaning to formula, we need to define a semantics.
The semantics of first-order logic is given by so-called first-order structures. A structure S is the data of: (1) a non-empty set X, over which terms are interpreted, (2) for each predicate symbol P (of arity n), an n-ary relation over X, (3) for each function symbol (of arity n), a function from Xn to X. We can then define a satisfaction relation ⊨, so that S ⊨ F (for every formula F), if and only if F is true in S. For example, S ⊨ ∀x.∃y.P(x,y) if and only if for every value a (of x) in X, there is a b in X such that (a,b) is related by the relation associated with the symbol P by S.
Formulae are proved in a so-called proof system, given by deduction rules. There are plenty of proof systems available. All reasonable proof systems are sound: if you can prove F in this proof system, then S ⊨ F for every first-order structure S, namely, F is valid. The real question is completeness: is every valid sentence provable?
This question was solved first by Kurt Gödel [6] in 1930. That obviously depends on your proof system, but here is a generic completeness argument. By generic, I mean that it will apply to any proof system, provided it satisfies some assumptions which I will enumerate along the way.
We start by assuming that our proof system specifies an entailment relation, which I will write as ≤, and that entailment is a preordering. This induces an equivalence relation ≡ on sentences (F≡G if and only if F≤G and G≤F; known as logical equivalence). Let [F] be the equivalence class of F. The quotient of the set of all formulae by ≡ is a poset L, with (the trace of) ≤ as ordering. L is called the Lindenbaum algebra of the proof system.
We will assume that the proof system has enough deduction rules so that L is a Boolean algebra, with bottom element [⊥], top element [⊤], complement implemented by ¬ (i.e., the complement of [F] is [¬F]), binary infimum implemented by ∨ (i.e., the inf of [F] and [G] is [F ∨ G]), and binary supremum implemented by ∧. Explicitly, for the latter, we should have rules that allow us to show that F ∧ G entails F, that F ∧ G entails G, and that if H entails F and also entails G, then H entails F ∧ G. (The first two are the so-called elimination rules for conjunction, and the third one is the introduction rule for conjunction, in natural deduction.)
This is enough to deal with the propositional connectives ∧, ∨, ¬, ⊤, ⊥. In order to deal with the quantifiers, we will also assume that [∀x.F(x)] is the infimum of the family of elements [F(t)], where t ranges over the so-called closed terms (closed meaning without any variable, e.g., f(a,b), where a and b are constants, namely function symbols of arity 0), and that [∃x.F(x)] is the supremum of the family of elements [F(t)], where t ranges over the closed terms. (Technically, that requires one to add so-called Henkin constants to the language. This is a clever, but rather hackish trick. Please allow me not to say anything more about it.)
Because we have negation, we do not need to consider, say, the first constraint on universal quantifications, and we simply assume that [∀x.F(x)] = [¬∃x.¬F(x)], and that [∃x.F(x)] = sup {[F(t)] | t closed}, instead.
Now we are set. Imagine that F is an unprovable sentence. We need to find a first-order structure S such that S ⊨ F is wrong. The set X is simply the set of all closed terms (the so-called Herbrand universe). Instead of finding the relations associated with each predicate symbol P, we will directly define the family of all sentences T that are true in S. Here are our requirements on that family:
- T should not contain [F];
- T should be closed under entailment, namely: if [G] is in T and G≤H then [H] is in T;
- T should mimic the semantics: it should contain [⊤] but not [⊥] (not containing [⊥] is automatic from 1 and 2); it contains [G ∧ H] if and only if it contains [G] and [H] (hence T should be a filter), it contains [G ∨ H] if and only if it contains [G] or [H] (hence T should be a prime filter), it contains [¬G] if and only if it does not contain [G] (hence T is an ultrafilter—that is a useless requirement since, in a Boolean algebra, ultrafilters and prime filters coincide), and it contains [∃x.G(x)] if and only if it contains [G(t)] for some closed term t.
Note that, since I have assumed that [∀x.G(x)] = [¬∃x.¬G(x)], I do not need to assume the symmetric statement that T contains [∀x.G(x)] if and only if T contains [G(t)] for every closed term t.
If you look at it closely, you will realize that the requirement “T contains [∃x.G(x)] if and only if it contains [G(t)] for some closed term t” is equivalent to saying “T respects the sup situations {[G(t)] | t closed}, for every formula G(x) with at most one unquantified variable x“.
There are only countably many formulae, so there are only countably many such sup situations to respect. Recapitulating, we need to find a prime filter T that contains [⊤], does not contain [F], and which respects countably many sup situations {[G(t)] | t closed}. This is exactly what the Rasiowa-Sikorski lemma states the existence of. T describes a first-order structure S such that S ⊨ F is wrong. Hence our proof system is complete.
Oh, before I go on, you will almost never find this argument, in papers or books of logic. Completeness is usually proved by building the ultrafilter T by hand, directly, using the fact that L itself is countable. The process is rather ad hoc: essentially we initialize T to {¬F}, then we add new formulae to T as long as they do not contradict the current set of formulae in T. There are additional difficulties, notably all formulae must be dealt with eventually, and the quantifications present specific difficulties as well. That argument looks more like a hack, but it is elementary, and this is perhaps why it is preferred nowadays.
But we are interested in topology, right? The point here is that, as R. Goldblatt noticed [2], the Rasiowa-Sikorski lemma is a consequence of Stone duality and the Baire property.
The Görnemann-Rauszer-Sabalski Lemma
I will in fact explain a more general result than the Rasiowa-Sikorski result, and that is (half of) a result by Görnemann [3] and Rauszer and Sabalski [4]. My exposition is a variant on Goldblatt’s [2], as you may have guessed.
Here is the setting. We return to the case of a bounded distributive lattice L. A sup situation D in L is distributive if and only if, for every u in L, u ⋀ sup D = sup {u ⋀ v | v ∈ D}. (The theorem will not work without that extra assumption. But it will be automatic in Boolean algebras.) Then we have:
Theorem [3,4]. Let L be a bounded distributive lattice, and E be a countable family of distributive sup situations in L. For every pair u≰v in L, there is a prime filter F that contains u, does not contain v, and respects all the sup situations in E.
I said “half of” the Görnemann-Rauszer-Sabalski theorem. The authors of [3] and [4] also consider so-called distributive inf situations. An inf situation is a family A with a greatest lower bound inf A. It is distributive if and only if, for every u in L, u ⋁ inf A = inf {u ⋁ v | v ∈ A}. F respects an inf situation A if and only if (A ⊆ F implies inf A ∈ F). The full result is that we can find a prime filter F that contains u, does not contain v, and respects both the sup situations and the inf situations from two countable sets, one of distributive sup situations, the other one of distributive inf situations. I will not bother to consider inf situations here. The argument is similar.
The proof (1/5): Stone enters the stage
We now prove this. First, instead of looking for a (join-)prime filter, we will look for a (meet-)prime ideal. This is equivalent, in the sense that the complement of a meet-prime ideal is a join-prime filter. (Exercise!)
Now, what we are looking for, modulo that change of point of view, is a (meet-)prime ideal x that contains v, does not contain u, and respects all the sup situations D in L, in the sense that (D ⊆ x implies sup D ∈ x).
What is (meet-)prime ideal? That is an element of the space pt(I(L)), the Stone dual of I(L), if you follow Corollary 8.1.21 of the book. (This is why I wrote it as x above: this is really a point of a topological space.)
If you have a look at Exercise 9.5.12 in the book, you will see that I(L) is an algebraic fully arithmetic complete lattice, and Exercise 9.5.19 says (among other things) that pt(I(L)) is a spectral space. Goldblatt looks directly at its patch space, which is a Priestley space (see Theorem 9.5.24 in the book). We will make good use of that wealth of structure. Notably, pt(I(L))patch is compact Hausdorff.
The proof (2/5): the sets Oa
The open subsets of the topology on pt(I(L)) are the sets OI={x ∈ pt(I(L)) | I ⊊ x}, where I ranges over I(L), still following Corollary 8.1.21. Let me write Oa for O↓a, for every a in L. Then Oa is {x ∈ pt(I(L)) | a ∉ x}, and the sets Oa form a basis of the topology on pt(I(L)). Indeed, for every ideal I, OI is the union of the sets Oa where a ranges over the elements of I.
Those sets Oa are not just open. They are compact open. The short argument is as follows. The finite elements of the lattice of open sets O(Y) of any topological space Y are its compact open subsets. When Y=pt(I(L)), O(Y) is isomorphic to I(L), because O ⊣ pt is an equivalence (Exercise 9.5.5). Explicitly, I ↦ OI is an order isomorphism. But the finite elements of I(L) are the principal filters ↓a, a in L, and we are done.
The proof (3/5): translating the statement into topological terms
Now what does it mean for a prime ideal x to contain v? That means that x is not in Ov. And what does it mean to fail to contain u? That means that x is in Ou. Hence we are looking for an element x of pt(I(L)) in Ou–Ov, and which respects all the sup situations in the countable family E.
Note, for future reference, that since Ou is open and Ov is compact saturated, Ou–Ov is patch-open. Recall that a patch-open set is one that is open in the patch topology. We will freely use the names “patch-closed”, “patch-compact”, “patch-dense”, and so on as well.
Note also that Ou–Ov is non-empty. Otherwise, Ou would be included in Ov. Since I ↦ OI is an order isomorphism, that would imply ↓u ⊆ ↓v, hence u≤v, which would contradict our assumption that u≰v.
Finally, what does it mean for a prime ideal x to respect a sup situation D? This is the condition (D ⊆ x implies sup D ∈ x), or equivalently (if for every d in D, x is not in Od, then x is not in Osup D). By taking contrapositives, this means (if x is in Osup D then x is in Od for some d in D), or alternatively, (x is in UD imp VD), where UD is the open set Osup D and VD is the open set obtained as the union of the open sets Od, d in D. Recall the notation U imp V, meaning the set of points x such that (x is in U implies x is in V), and which we have introduced for so-called UCO sets in the post on countably presented locales.
We will reflect on the fact that UD imp VD is a UCO set later (and very briefly). For now, we remark that UD imp VD is the union of the open set VD, and of the complement of UD = Osup D. That last complement is the complement of a compact open set, hence it is open in the de Groot dual of pt(I(L)). It follows that both VD and the complement of UD are patch-open. Hence UD imp VD is also patch-open.
The proof (4/5): patch-density
UD imp VD is a UCO set, it is patch-open, good. It is also patch-dense, as we now claim. This is where we use that D is a distributive sup situation.
In order to see this, we consider a non-empty patch-open subset V of pt(I(L)), and we must show that it intersects UD imp VD. We use Theorem 9.5.24 of the book: the patch topology of pt(I(L)) has a base of sets of the form K–K’, where K and K’ range over the compact open subsets of pt(I(L)). We remember that the compact open sets are the sets Oa, a in L. Hence V is a union of sets of the form Oa–Ob, with a, b ∈ L. At least one of them must be non-empty. We pick one, Oa–Ob. It is non-empty, so there is a point x in Oa–Ob. We need to show that Oa–Ob intersects UD imp VD.
We imagine it does not. If that is the case, then (Oa–Ob) ∩ (UD imp VD) is empty. By distributing the union implicit in the imp operator with intersection, this means: (1) Oa–Ob ⊆ UD, and (2) Oa–Ob ∩ VD is empty. Equivalently: (1) Oa ⊆ Ob ∪ UD, and (2) Oa ∩VD ⊆ Ob.
We rewrite (2) as follows. VD is the union of the open sets Od, d in D, so (2) states that Oa ∩ Od ⊆ Ob for every d in D. Since I ↦ OI is an order isomorphism, Oa ∩ Od = O↓a ∩ O↓d = O↓a ∩ ↓d = O↓(a ⋀ d) is included in Ob if and only if a ⋀ d ≤ b. Hence (2) states that a ⋀ d ≤ b for every d in D.
Oh, but D is a distributive sup situation! so a ⋀ sup D = sup {a ⋀ d | d ∈ D}, and therefore a ⋀ sup D ≤ b.
We haven’t used (1) yet. Since x is in Oa, by (1) it is in Ob or in UD. We claim that x is in Ob. It suffices to show this if x is in UD = Osup D. If so, then x is in Oa ∩ Osup D = Oa ⋀ sup D. Since a ⋀ sup D ≤ b, Oa ⋀ sup D is included in Ob, so x is in Ob. All right, so x is in Ob, whichever case is true. But that is impossible, since we have taken x from Oa–Ob.
Hence UD imp VD is patch-dense, as we claimed.
The proof (5/5): invoking Baire
Let us repeat a few of the things we have already said. First, pt(I(L))patch is compact Hausdorff. Second, Ou–Ov is patch-open and non-empty. Third, UD imp VD is patch-open, and patch-dense for every distributive sup situation D. We are also given a countable family E of distributive sup situations.
Every compact Hausdorff space is Baire. In fact, every sober locally compact space is Choquet-complete, hence Baire (Theorem 8.3.24 in the book). Therefore pt(I(L))patch is Baire.
The intersection of the sets UD imp VD, where D ranges over E, is a countable intersection of dense subsets of pt(I(L))patch, hence it is dense, by the Baire property. Hence it intersects the non-empty open subset Ou–Ov of pt(I(L))patch.
Let x be a point in the intersection. It is in Ou–Ov, so u is not in x, and v is in x, as we have already argued. For every sup situation D in E, x is in UD imp VD, and we have already said that this means that x respects the sup situation D. This finishes the proof. ☐
The Rasiowa-Sikorski lemma as a corollary
In summary, we have shown: Let L be a bounded distributive lattice, and E be a countable family of distributive sup situations in L; for every pair u≰v in L, there is a prime filter F that contains u, does not contain v, and respects all the sup situations in E.
If L is a Boolean algebra, then L is, in particular, a bounded distributive lattice. In fact, all suprema that exist automatically distribute over ⋀. This is because every Boolean algebra is a Heyting algebra (see Exercise 9.5.22 in the book), with u ⇒ v defined as ¬u ⋁ v. Recall that residuation ⇒ is uniquely determined by the fact that for every d in L, u ⋀ d ≤ v if and only if d ≤ u ⇒ v. In other words, u ⋀ _ is left adjoint to u ⇒ _. And left adjoints preserve all colimits (all suprema, here). Explicitly, imagine that D is a family with a supremum sup D, and let u be any element of L. Then u ⋀ sup D is an upper bound of {u ⋀ d | d ∈ D}. Given any other upper bound v of {u ⋀ d | d ∈ D}, we have u ⋀ d ≤ v for every d in D, hence d ≤ u ⇒ v for every d in D, namely sup D ≤ u ⇒ v, and therefore u ⋀ sup D ≤ v.
It follows that, if L is a Boolean algebra, then all sup situations are distributive. We obtain the Rasiowa-Sikorski lemma:
Corollary [1]. Let L be a Boolean algebra, and E be a countable family of sup situations in L. For every pair u≰v in L, there is a prime filter F that contains u, does not contain v, and respects all the sup situations in E.
And beyond…
Let us look back at the proof of the (“half of”) Görnemann-Rauszer-Sabalski theorem. We have built a subset Y of pt(I(L)) as the intersection of the sets UD imp VD, where D ranges over a given countable set of distributive sup situations E. We have seen that Y is patch-dense, and that was the key to the proof.
Y is also a Π02 subset of pt(I(L)). Indeed, recall that sets of the form UD imp VD are UCO (union of closed and open subset), and that Π02 subsets are countable intersections of UCO subsets by definition.
pt(I(L)) is a spectral space, hence is in particular sober and locally compact. If L is countable (as in the case of the Lindenbaum algebra of first-order logic), then the base of open sets Oa of pt(I(L)) is countable, hence pt(I(L)) is second countable. Every second countable, sober locally compact space is quasi-Polish, and every Π02 subset of a quasi-Polish space is quasi-Polish [5]. That is extra structure that allows one to prove some more completeness results, especially on probabilistic logics. A remarkable paper in that respect is [7], which uses a variant of this (and other things…) in a crucial way.
- Helena Rasiowa and Roman Sikorski, The Mathematics of Metamathematics. PWN–PolishScientific Publishers, Warsaw, 1963.
- Robert Goldblatt. 2012. Topological Proofs of some Rasiowa-Sikorski Lemmas. Studia Logica, 100, 1–18.
- Sabine Görnemann. 1971. A Logic Stronger than Intuitionism. Journal of Symbolic Logic, 36(2), 249–261.
- Cecylia Rauszer and Bogdan Sabalski. 1975. Notes on the Rasiowa-Sikorski Lemma. Studia Logica, 34(3), 265–268.
- Matthew de Brecht. Quasi-Polish spaces. Annals of Pure and Applied Logic, Volume 164, Issue 3, March 2013, pages 356-381.
- Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik (in German). Volume 37, Issue 1, 1930, 349–360.
- Dexter Kozen, Kim G. Larsen, Radu Mardare, and Prakash Panangaden. Stone duality for Markov processes. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 2013, 321–330.
— Jean Goubault-Larrecq (December 23rd, 2019)