A topological space related to SAT: is it compact?

The Satisfiability problem is, of course, a fundamental problem in theoretical CS. I was playing with one version of the problem with infinitely many variables. $\newcommand{\sat}{\mathrm{sat}} \newcommand{\unsat}{\mathrm{unsat}}$

Basic Setup. Let $X$ be a nonempty and possibly infinite set of variables. A literal is either a variable $x \in X$ or its negation $\neg x$. A clause $c$ is a disjunction of finite number of literals. Finally, we define a formula $F$ as a set of clauses.

An assignment of $X$ is a function $\sigma : X \to \{0,1\}$. I will not explicitly define the condition for when an assignment $\sigma$ satisfies a clause; it is slightly cumbersome, and is the same as in standard SAT. Finally, an assignment satisfies a formula if it satisfies every constituent clause. Let $\sat(F)$ be the set of satisfying assignments for $F$, and let $\unsat(F)$ be the complement of $\sat(F)$.

A topological space.

Our goal is to endow the space of all assignments of $X$, call this $\Sigma$, with a topological structure. Our closed sets are of the form $\sat(F)$ where $F$ is a formula. We can verify that this is indeed a topology:

• The empty formula $\emptyset$ containing no clauses is satisfied by all assignments; so $\Sigma$ is closed.
• The formula $\{ x, \neg x \}$ for any $x \in X$ is a contradiction. So $\emptyset$ is closed.
• Closure under arbitrary intersection. Suppose $F_{i}$ is a formula for each $i \in I$. Then $\sat \left(\bigcup_{i \in I} F_i\right) = \bigcap_{i \in I} \sat(F_i)$.
• Closure under finite union. Suppose $F$ and $G$ are two formulas, and define $$F \vee G := \{ c \vee d \,:\, c \in F, d \in G \}.$$ Then $\sat(F \vee G) = \sat(F) \cup \sat(G)$.This needs an argument, but I'll skip this.

Call this topology $\mathcal T$, the "satisfiability topology"(!) on $\Sigma$. Of course, the opens sets of this topology are of the form $\unsat(F)$. Moreover, I observed that the collection of open sets $$\{ \unsat(c) \,:\, c \text{ is a clause} \}$$ forms a basis for $\mathcal T$. (Exercise!)

Compact? I feel that this is an interesting, if not terribly useful, way to look at things. I want to understand whether this topological space possesses traditional interesting properties like compactness, connectedness etc. In this post, we will restrict ourselves to compactness:

Let $X$ be a countably infinite collection of variables.1 Is $\Sigma$ compact under $\mathcal T$?

One can prove the following

Proposition. $\mathcal T$ is compact if and only for all unsatisfiable formulas $F$, there exists a finite unsatisfiable subformula $\{ c_1, c_2, \ldots, c_m \} \subseteq F$.

(Not-so-hard exercise!) After several days of thinking, I do not have much progress in answering this question. I also do not have strong evidence for or against compactness. Can you suggest some approach?

Finally, as a bonus question:

Has such a structure been studied before?

1The restriction to countable $X$ is just for simplicity; it also feels like the next natural step from finite number of variables.

• (1.) Based on the wiki summary of the topology tag, this tag isn't that relevant here. Nevertheless I included it since the question explicitly connects to point-set topology. (2.) I wasn't sure if this question is more suited for Math.SE or here; I decided to post it here. (3.) Sorry about the length of the question. Since I presume not everyone will be familiar with a topological space, I explained that stuff a little more elaborately. Sep 5, 2011 at 16:47
• I submitted a tag improvement request to broaden the definition of the topology tag. Sep 5, 2011 at 17:46
• Small remark: given a formula F (which is in CNF form), one can convert it to DNF form, negate it and use De Morgan to create a formula F' in CNF form such that sat(F)=unsat(F') and unsat(F)=sat(F'). Thereby, any set is closed iff it is open in your topology. Sep 5, 2011 at 17:58
• Isn't your proposition just a special case of the compactness theorem (en.wikipedia.org/wiki/Compactness_theorem) for propositional logic? Sep 5, 2011 at 18:16
• @Travis It could be, I am not sure. My background in logic is quite deficient, so I cannot see these things very clearly. :) Sep 6, 2011 at 0:27

What you are doing is deriving a topological representation of a Boolean algebra. The study of representations of Boolean algebras goes back at least to Lindenbaum and Tarski who proved (in 1925, I think) that the complete, atomic Boolean algebras are isomorphic to powerset lattices.

There are however, Boolean algebras that are not complete and atomic. For example, the sequence $x_1, x_1 \land x_2, \ldots$, is a descending chain that has no limit in the Boolean algebra defined over formulas. The question of whether arbitrary Boolean algebras, such as the one you mention, also had set-based representations was solved by Marshall Stone, who put forth the maxim "always topologize" (Marshall H. Stone. The representation of Boolean algebras, 1938).

Stone's Representation Theorem for Boolean Algebras Every Boolean algebra is isomorphic to the lattice of clopen subsets of a topological space.

The main idea is to consider what in your case are the satisfying assignments to a formula. In the general case, you consider homomorphisms from a Boolean algebra into the two element Boolean algebra (the truth values). The inverse of $\mathit{true}$ gives you the sets of satisfying assignments, or what are called ultrafilters of the Boolean algebra. From these, one can obtain a topology called the spectrum or Stone space of a Boolean algebra. Stone provide the answer to your question too.

The Stone space of a Boolean algebra is a compact, totally disconnected Hausdorff space.

There have been several results that extend and generalise Stone's representation in various directions. A natural question is to ask if other families of lattices have such representations. Stone's results also apply to distributive lattices. Topological representations for arbitrary lattices were given by Alasdair Urquhart in 1978. Distributive lattices enjoy greater diversity in structure, compared to Boolean algebras and are of great interest. A different representation for the distributive case was given by Hilary Priestley in 1970, using the idea of an ordered topological space. Instead of set-based representations, we can find poset-based representations and topologies.

The constructions in these papers have one remarkable property. Stone's construction maps not just Boolean algebras to topological spaces: structural relationships relating Boolean algebras translate into structural properties between the resulting topologies. It is a duality between categories. The entire gamut of such results is called Stone Duality. Informally, dualities give us precise translations between mathematical universes: the combinatorial world of sets, the algebraic world of lattices, the spatial world of topology and the deductive world of logic. Here are a few starting points that may help.

1. Chapter 11 of Introduction to Lattices and Order, by Davey and Priestley covers Stone's theorem.
2. Matthew Gwynne's slides cover the theorem and give a proof of compactness. Matthew (in the comments) also suggests Introduction to Boolean Algebras by Paul Halmos.
3. In moving from propositional logic to modal logic, the Boolean algebra is extended with a join-preserving operator and topology with an interior. Jónsson and Tarski's 1952 paper, Boolean Algebras with Operators is extremely readable and consistent with modern notation.
4. Chapter 5 of Modal Logic by Blackburn, de Rijke and Venema covers Stone's theorem and its extension to Boolean algebras with operators.
5. Stone Spaces by Peter Johnstone reviews such results for various other kinds of algebras.
• Stone Duality is more general. Johnstone and Vicker's books (see the references part of the Wikipedia article) are both quite nice, though the first one is quite advanced. Sep 5, 2011 at 22:43
• Yes, but I'm not sure if the OP wanted to know about Stone Duality in its full glory. Have added a few links per your comment. If one just wants the representation theorem, Davey and Priestley's presentation suffices. Sep 5, 2011 at 23:10
• @Kaveh: Appreciated. Am still getting used to identifying the desired detail-level of an answer, and reading the tone of comments. Not that my sounding like a grumpy old man helps. (smiley-face) Sep 6, 2011 at 1:07
• This would be a great stepping off point for a blog post on Stone Duality and connections to CS. Sep 6, 2011 at 4:45
• Paul Halmos' "Introduction to Boolean Algebras" also covers the representation theorem, as well as other duality theorems. Sep 6, 2011 at 6:13