A topological space related to SAT: is it compact?

Question

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.¹ 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?

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

Answer 1

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.