- English only
Lab for Automated Reasoning and Analysis LARA
Compactness Theorem for Propositional Logic
Among the application of compactness theorem is showing that certain theorem proving methods are “complete in the limit”.
- is the countably infinite set of all propositional variables of interest
- interpretation maps propositional variables to truth values
- if is a propositional formula, means that is true when the variables are interpreted according to
- if is a set of formulas, means: for each ,
Theorem (Compactness Theorem for Propositional Logic): Let be a (possibly infinite) set of propositional formulas. Then is satisfiable if and only if every finite subset of is satisfiable.
Equivalent statement of compactness: If a set is not satisfiable, then some finite subset of 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. where , that is, is equivalent to . In this example, every finite subset of is satisfiable, but itself is not.
Proof of the compactness theorem: One direction is trivial: if is satisfiable then there exists such that . Then for every finite subset we have , so 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 into one large interpretation for the entire infinite set . 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 be finitely satisfiable. Let be the sequence of all propositional variables for formulas in (this set is countable by our assumption on Propositional Logic Syntax, but can be infinite).
Given a sequence of boolean values of length , by an -interpretation we mean an interpretation such that .
We will define interpretation where the sequence of values is given as follows:
We next show by induction the following.
Claim: For every non-negative integer , every finite subset has a -interpretation such that .
Base case: For the statement reduces to claim that every finite subset of is satisfiable, which is an assumption of the theorem.
Inductive step: Assume the claim for : every finite subset has a -interpretation such that , we show that the statement holds for . If , the inductive statement holds by definition of . Let . Then by definition of , there exists a finite set that has no interpretation. We wish to show that every finite set has a interpretation such that . Take any such set . Consider the set . This is a finite set, so by inductive hypothesis, it has a -interpretation . Because which has no -interpretation, we have . Therefore, is a -interpretation for , and therefore for . This completes the inductive proof.
SECOND PART. We finally show that . Let . Let and . Then . The set is finite, so, by the Claim, it has a -interpretation such that . Because is also a -interpretation, and it agrees on all variables in , we have .
End of Proof.
How does this proof break if we allow infinite disjunctions? Consider the above example where . The inductively proved claim still holds, and the sequence defined must be . Here is why the claim holds for every . Let be arbitrary and be finite. Define
Then consider interpretation that assigns to true all for and sets the rest to false. Such interpretation makes true, so if it is in the set , then interpretation makes it true. Moreover, all other formulas in are propositional variables set to true, so the interpretation makes true. Thus, we see that the inductively proved statement holds even in this case. What the infinite formula breaks is the second part, which, from the existence of interpretations that agree on an arbitrarily long finite prefix we can derive an interpretation for infinitely many variables. Indeed, this part of the proof explicitly refers to a finite number of variables in the formula.