This is an old revision of the document!

Compactness Theorem for Propositional Logic

Among the application of compactness theorem is showing that certain theorem proving methods are “complete in the limit”.

Notation:

${\cal B} = \{ \mbox{false},\mbox{true} \}$
$V$ is the countably infinite set of all propositional variables of interest
interpretation $I : V \to {\cal B}$ maps propositional variables $V$ to truth values ${\cal B}$
if $F$ is a propositional formula, $I \models F$ means that $F$ is true when the variables are interpreted according to $I$
if $S$ is a set of formulas, $I \models S$ means: for each $F \in S$ , $I \models F$

Theorem (Compactness Theorem for Propositional Logic): Let $S$ be a (possibly infinite) set of propositional formulas. Then $S$ is satisfiable if and only if every finite subset of $S$ is satisfiable.

Equivalent statement of compactness: If a set $S$ is not satisfiable, then some finite subset of $S$ is not satisfiable.

If we allow infinite disjunctions in formulas, compactness fails. Note that we do not consider formulas with infinite connectives as propositional formulas (such formulas are usually called 'infinitary'), and from that reason the compactness theorem does not apply to this example.

Example. $S = \{ D, p_1, p_2, p_3, \ldots \}$ where $D = \bigvee\limits_{i=1}^{\infty} \lnot p_i$ , that is, $D$ is equivalent to $\exists i \ge 0. \lnot p_i$ . In this example, every finite subset of $S$ is satisfiable, but $S$ itself is not.

Proof of the compactness theorem: One direction is trivial: if $S$ is satisfiable then there exists $I$ such that $I \models S$ . Then for every finite subset $T \subseteq S$ we have $I \models T$ , so $T$ is satisfiable. We need to show the converse.

Intuition: A finitely satisfiable set has “all finite pieces” satisfiable (using potentially different interpretations). The question is whether we can somehow assemble interpretations for all finite pieces $T$ into one large interpretation for the entire infinite set $S$ . We will define such interpretation by extending it variable by variable, while preserving finite satisfiability for interepretations that begin with values for propositional variables chosen so far.

Let $S$ be finitely satisfiable. Let $V = \{ p_1,p_2,\ldots \}$ be the sequence of all propositional variables for formulas in $S$ (this set is countable by our assumption on Propositional Logic Syntax, but can be infinite).

Given a sequence of boolean values $u_1,u_2,\ldots,u_n \in {\cal B}$ of length $n \ge 0$ , by an $u_1,u_2,\ldots,u_n$ -interpretation we mean an interpretation $I : V \to {\cal B}$ such that $I(p_1)=u_1,\ldots,I(p_n)=u_n$ .

We will define interpretation $I^*(p_k) = v_k$ where the sequence of values $v_1,v_2,\ldots$ is given as follows: \[

  v_{k+1} = \left\{\begin{array}{l}

{\it false}, \mbox{ if for every finite } T \subseteq S, \mbox{ there exists a } v_1,\ldots,v_k,{\it false}-\mbox{interpretation } I \mbox{ such that } I \models T
{\it true}, \mbox{otherwise} \] We next show by induction the following.

Claim: For every non-negative integer $k$ , every finite subset $T \subseteq S$ has a $v_1,\ldots,v_k$ -interpretation $I$ such that $I \models T$ .

Base case: For $k=0$ the statement reduces to claim that every finite subset of $S$ is satisfiable, which is an assumption of the theorem.

Inductive step: Assume the claim for $k$ : every finite subset $T \subseteq S$ has a $v_1,\ldots,v_k$ -interpretation $I$ such that $I \models T$ , we show that the statement holds for $k+1$ . If $v_{k+1}={\it false}$ , the inductive statement holds by definition of $v_{k+1}$ . Let $v_{k+1}={\it true}$ . Then by definition of $v_{k+1}$ , there exists a finite set $A \subseteq S$ that has no $v_1,\ldots,v_k,{\it false}$ interpretation. We wish to show that every finite set $B \subseteq T$ has a $v_1,\ldots,v_k,{\it true}$ interpretation such that $I \models B$ . Take any such set $B$ . Consider the set $A \cup B$ . This is a finite set, so by inductive hypothesis, it has a $v_1,\ldots,v_k$ -interpretation $I$ . Because $I \models A$ which has no $v_1,\ldots,v_k,{\it false}$ -interpretation, we have $I(p_{k+1})={\it true}$ . Therefore, $I$ is a $v_1,\ldots,v_k,{\it true}$ -interpretation for $A \cup B$ , and therefore for $B$ . This completes the inductive proof.

We finally show that $I^* \models S$ . Let $F \in S$ . Let $FV(F) = \{p_{i_1},\ldots,p_{i_k} \}$ and $M = \max(i_1,\ldots,i_k)$ . Then $FV(F) \subseteq \{p_1,\ldots,p_M\}$ . The set $\{F\}$ is finite, so, by the Claim, it has a $v_1,\ldots,v_M$ -interpretation $I$ such that $I \models F$ . Because $I^*$ is also a $v_1,\ldots,v_M$ -interpretation, we have $I^* \models F$ .

End of Proof.