Compactness (propositional logic)

The compactness theorem reduces the satisfiability of an infinite set of propositional formulas to the satisfiability of its finite subsets. This is reminiscent of a phenomenon in topology called compactness. In fact, it is the same phenomenon.

Theorem [Compactness theorem] Let $\Phi$ be an arbitrary set of propositional formulas. Then $\Phi$ is satisfiable if, and only if, every finite set $\Phi_0 \subseteq \Phi$ is satisfiable.

Corollary Let $\Phi$ be an arbitrary set of propositional formulas and $\psi$ any propositional formula. Then $\Phi \models \psi$ if, and only if, $\Phi_0 \models \psi$ for some finite set $\Phi_0 \subseteq \Phi$.

Proof

The direction from left to right in the theorem is trivial, because if a set of formulas is satisfiable, then so is every subset of it, in particular, every finite subset of it.

The difficult part is the other direction and when $\Phi$ is an infinite set. One way to prove it is to use a transfinite induction on the set of variables used. The idea is that a 1-assignment is constructed step-by-step.

For the special case where the variables are $X_0, X_1, \dots$ this is carried out in what follows.

Useful terminology

A partial assignment $\beta$ is said to be extensible for a finite set of formulas $\Phi_0$ if there exists a 1-assignment $\beta'$ for $\Phi_0$ such that $\beta \subseteq \beta'$ and $\beta' \mymodels \Phi_0$.

Example $\{X_0 \mapsto 0\}$ is extensible for $\{\neg X_0 \wedge X_1\}$, but $\{X_0 \mapsto 1\}$ is not.

Remark If $\beta$ is extensible for a finite set $\Phi_0$ and $\text{vars}(\Phi_0) \subseteq \text{dom}(\beta)$, then $\beta \mymodels \Phi_0$, that is, $\beta$ is a partial 1-assignment for $\Phi_0$.

This follows immediately from the coincidence lemma.

A partial variable assignment $\beta$ is said to be extensible for an infinite set $\Phi$ of propositional formulas if it is extensible for every finite set $\Phi_0 \subseteq \Phi$.

Proof itself

Let $\Phi$ be an infinite set of formulas such that every finite subset of it is satisfiable. By induction, we define a value $b_i$ for every $i \in \mathbf N$ such that for every $n$ the function $\beta_n \colon \{X_0, \dots, X_{n-1}\} \to \{0,1\}$ with $\beta_n(i) = b_i$ for every $i<n$ is extensible for $\Phi$.

This is sufficient, as is explained in what follows. Let $\beta^*$ be the variable assignment with $\beta^*(X_i) = b_i$ for every $i \in \mathbf N$. Claim: $\beta^* \mymodels \Phi$. To see this, assume $\varphi \in \Phi$. Let $n$ be such that $\text{vars}(\varphi) \subseteq \{X_0, \dots, X_{n-1}\}$. Then $\beta^* \vert_{\{X_0, \dots, X_{n-1}\}}$ is extensible for $\{\varphi\}$ and also a 1-assignment for $\varphi$ by the above remark. So, by the coincidence lemma, $\beta^*$ is a 1-assignment for $\varphi$.

The $b_i$'s are defined as follows. Assume $b_i$ has been defined for $i<n$ in such a way that $\beta_n$ (see above) is extensible for $\Phi$. By way of contradiction, assume neither $\beta_n \cup \{X_n \mapsto 0\}$ nor $\beta_n \cup \{X_n \mapsto 1\}$ is extensible for $\Phi$. Then there are finite sets $\Phi_0, \Phi_1 \subseteq \Phi$ such that $\beta_n \cup \{X_n \mapsto b\}$ is not extensible for $\Phi_b$ for every $b \in \{0,1\}$.

By the inductive assumption, $\beta_n$ is extensible for $\Phi_0 \cup \Phi_1$. So there exists a variable assignment $\beta'$ with $\beta_n \subseteq \beta'$ and $\beta \mymodels \Phi_0 \cup \Phi_1$. In other words, $\beta_n \cup \{X_n \mapsto \beta'(X_n)\}$ is extensible for $\Phi_0 \cup \Phi_1$, and hence for $\Phi_0$ and $\Phi_1$—a contradiction.

This concludes the proof (for a countable set of variables or formulas).

Applications

There are many applications of the above compactness theorem. For instance, it is used to prove that resolution is complete for every set of clauses.

Other applications are in modelling. For instance, it can be used to show that certain infinite systems of equations are solvable iff every finite subsystem is solvable, or that quadrant I can be tiled iff larger and larger squares can be tiled. In other words, it is a general tool to reduce existential questions about infinite objects to questions about finite "sub" objects.

Finally, the following theorem is an immediate consequence of the above.

Theorem

1. EnumSAT is the set of words $u$ where $u$ is an encoding of an enumerating Turing machine $T$ such that the set of propositional formulas enumerated by $T$ is satisfiable. EnumSAT is co recursively enumerable.
2. EnumEntail is the set of pairs $\langle u, \varphi\rangle$ where $u$ is an encoding of a an enumerating Turing machine $T$ and $\varphi$ is a formula which is entailed by the set of formulas enumerated by $T$. EnumEntail is recursively enumerable.

Here is an algorithm which recognizes the complement of EnumSAT (on the set of all enumerating Turing machines). It makes use of a procedure Sat which is any SAT test.

  EnumSat($u$)
  Precondition: $u$ is an encoding of an enumerating TM $T$
  let $i = 0$
  let $\varphi = \bot$
  loop forever
    let $\psi = T(i)$
    if $\psi$ is a propositional formula
      let $\varphi = \varphi \wedge \psi$
      if Sat($\varphi$) = $\bot$
        accept