The compactness theorem for propositional logic

Here is a topological proof of the compactness theorem for propositional logic. The advantage of this proof over the purely logical, inductive proof is that it works when there are uncountably many propositional variables (which may be relevant when dealing with uncountable objects, e.g. a graph with vertex set V = \mathbb{R}). Thanks to Linus Richter and Malcolm Jones for their input.


Fix a cardinal \kappa, and let \mathcal{P} = \{ P_i : i \in \kappa \} be a set of propositional variables indexed by \kappa . Let \mathcal{V} = \big\{ v: \mathcal{P} \rightarrow \{ 0, 1 \} \big\} be the set of all valuation maps on \mathcal{P} , with valuations extended to arbitrary propositional formulae \varphi in the standard way.

We define a topology on \mathcal{V} by declaring the basic open sets to be O_\varphi = \{ v \in \mathcal{V} : v(\varphi) = 1 \} for each propositional formula \varphi . Clearly, the O_\varphi cover \mathcal{V} , since for any v \in \mathcal{V} and any i \in \kappa , v \in O_{P_i} or v \in O_{(\neg P_i)} depending on whether v(P_i)=1 or v(P_i)=0 . Furthermore, the O_\varphi are closed under finite intersections, since O_{\varphi_1} \cap \cdots \cap O_{\varphi_n} = O_{(\varphi_1 \wedge \cdots \wedge \varphi_n)}. Thus, the O_\varphi form a base for a topology on \mathcal{V} .

The compactness theorem is then equivalent to the following statement:

Theorem: \mathcal{V} , with the topology defined above, is a compact space.

To see that this implies logical compactness, fix some unsatisfiable set of propositional formulae \mathcal{F} . We consider its negation \neg \mathcal{F} = \{ \neg \varphi : \varphi \in \mathcal{F} \} . Since \mathcal{F} is unsatisfiable, \neg \mathcal{F} has the property that for every valuation map v: \mathcal{P} \rightarrow \{ 0, 1 \} , there is some \varphi \in \neg \mathcal{F} such that v(\varphi) = 1 . Therefore, \mathcal{O} = \{ O_\varphi : \varphi \in \neg \mathcal{F} \} is an open cover of \mathcal{V} .

Since \mathcal{V} is compact, \mathcal{O} has a finite subcover \mathcal{O}' = \{ O_{\varphi_1}, \cdots, O_{\varphi_n} \} . But, this means the set \neg \mathcal{F}' = \{ \varphi_1, \cdots, \varphi_n \} has the aforementioned property of \neg \mathcal{F} . Thus, \mathcal{F}' = \{ \varphi : \neg \varphi \in \neg \mathcal{F}' \} is a finite, unsatisfiable subset of \mathcal{F} .


It remains to see that \mathcal{V} is actually compact. Consider the “generalised Cantor space” 2^\kappa = \{ 0,1 \}^\kappa , i.e. \kappa -many copies of the discrete space \{ 0, 1 \} , endowed with the product topology. An appeal to Tychonoff’s theorem shows this is a compact space. There is an obvious mapping f: 2^\kappa \to \mathcal{V} by defining f[(a_i)_{i \in \kappa }] = v \iff v(P_i) = a_i for all i \in \kappa .

f is continuous (in fact, a homeomorphism): any propositional formula \varphi contains only finitely many propositional variables P_{i_1}, \ldots, P_{i_n} , so we can consider the set of all assignments of P_{i_1}, \ldots, P_{i_n} such that \varphi is true, i.e.

K = \bigg\{ \mathbf{b} = (b_1, \ldots, b_n) \in \{ 0,1 \}^n : \forall v \in \mathcal{V}\ \Big( \big( \forall k \leq n: v(P_{i_k}) = b_k \Big) \Longrightarrow v(\varphi) = 1 \Big) \bigg\}

Each n-tuple \mathbf{b} \in K defines an open subset of 2^\kappa by setting U_\mathbf{b} = \{ (a_i)_{i \in \kappa } \in 2^\kappa : a_{i_k} = b_k\ \forall k \leq n \} . Then:

f^{-1}(O_\varphi) = \{ (a_i)_{i \in \kappa } \in 2^\kappa : f[(a_i)_{i \in \kappa }] \in O_\varphi \} \\ \hspace{3.9em} = \{ (a_i)_{i \in \kappa } \in 2^\kappa : f[(a_i)_{i \in \kappa }](\varphi) = 1 \} \\ \hspace{3.9em} = \{ (a_i)_{i \in \kappa } \in 2^\kappa : \exists \mathbf{b} \in K\ \forall k \leq n\ f[(a_i)_{i \in \kappa }] (P_{i_k}) = b_k \} \\ \hspace{3.9em} = \{ (a_i)_{i \in \kappa } \in 2^\kappa : \exists \mathbf{b} \in K\ \forall k \leq n\ a_{i_k} = b_k \} \\ \hspace{3.9em} = \bigcup_{ \mathbf{b} \in K } U_\mathbf{b}

Since 2^\kappa is compact and f is continuous and surjective, we have that f( 2^\kappa ) = \mathcal{V} is compact, as required.