Compactness and Effectiveness

Truth-table methods are finite: they decide implication for a finite set of premises by checking finitely many rows. Two results reach past the finite. Compactness transfers satisfiability from finite subsets to an infinite whole, and effectiveness fixes what it means for a property of formulas to be decidable by an algorithm — language the incompleteness theorems later depend on.¹

The compactness theorem

Call a set $Σ$ of wffs satisfiable iff one truth assignment satisfies every member, and finitely satisfiable iff every finite subset is satisfiable.

One direction is free: a satisfying assignment for $Σ$ satisfies every subset, so satisfiable implies finitely satisfiable. For finite $Σ$ the converse is trivial, since $Σ$ is a finite subset of itself. The content is that an infinite finitely satisfiable set is satisfiable — that no obstruction to satisfiability is spread across infinitely many formulas without already showing up in some finite piece.

The nontrivial half of compactness: if every finite subset of a possibly infinite set has a satisfying assignment, then one assignment satisfies the whole set at once.

Proof by maximal extension

The proof has two parts: enlarge $Σ$ to a set that decides every formula while staying finitely satisfiable, then read a truth assignment straight off it.

Part 1 — extend. Since the sentence symbols are countable, so are the wffs; fix an enumeration $α_{1}, α_{2}, \dots$ of all of them. Define a chain by recursion:

Δ_{0} = Σ, Δ_{n + 1} = {Δ_{n}; α_{n + 1} Δ_{n}; (\neg α_{n + 1}) if this is finitely satisfiable, otherwise,

where $Δ_{n}; α$ abbreviates $Δ_{n} \cup {α}$ . At each step at least one of the two choices keeps the set finitely satisfiable, so every $Δ_{n}$ is finitely satisfiable. Let $Δ = ⋃_{n} Δ_{n}$ . Then:

$Σ \subseteq Δ$ ;
for every wff $α$ , either $α \in Δ$ or $(\neg α) \in Δ$ (it was decided at stage $n + 1$ when $α = α_{n + 1}$ );
$Δ$ is finitely satisfiable — any finite subset lies inside some $Δ_{n}$ , which is finitely satisfiable.

The construction is a walk down a binary tree: at level $n$ it commits to including $α_{n}$ or its negation, always down a branch that stays finitely satisfiable. When there are uncountably many sentence symbols the enumeration is unavailable, and Zorn's lemma produces a maximal finitely satisfiable $Δ$ instead.

The extension as a branch through a binary tree of choices: at each formula the construction adds it or its negation, always taking a branch that stays finitely satisfiable, and the limit of the branch decides every formula.

Part 2 — read off an assignment. Define $v (A) = T$ iff $A \in Δ$ , for every sentence symbol $A$ . A structural induction on $φ$ shows that $v$ satisfies $φ$ iff $φ \in Δ$ : the atomic case is the definition, and the connective cases use that $Δ$ decides every formula and is finitely satisfiable. Since $Σ \subseteq Δ$ , $v$ satisfies every member of $Σ$ . $■$

Compactness for consequence

The satisfiability form has an implication form, using that $Σ ⊨ τ$ iff $Σ; (\neg τ)$ is unsatisfiable.

A tautological consequence of infinitely many premises already follows from finitely many of them. This corollary is in fact equivalent to compactness.

Coloring an infinite graph

Compactness turns an infinite combinatorial constraint into infinitely many finite ones. The four-color theorem colors any finite planar map with four colors; compactness extends it to infinite maps.

Worked example. A countably infinite planar map $C_{1}, C_{2}, \dots$ is four-colorable.²

For each country $C_{i}$ and color $c \in {r, g, b, y}$ take a sentence symbol $A_{i, c}$ reading country $C_{i}$ has color $c$ . Let $Σ$ collect:

for each $i$ , that $C_{i}$ gets exactly one color — the disjunction $(A_{i, r} \lor A_{i, g} \lor A_{i, b} \lor A_{i, y})$ and, for each pair of distinct colors $c \neq = c^{'}$ , the formula $(\neg (A_{i, c} \land A_{i, c^{'}}))$ ;
for each pair of adjacent countries $C_{i}, C_{j}$ and each color $c$ , the formula $(\neg (A_{i, c} \land A_{j, c}))$ .

A truth assignment satisfying $Σ$ is a proper four-coloring of the whole map. Any finite $Σ_{0} \subseteq Σ$ mentions finitely many countries, which form a finite planar map, four-colorable by the finite theorem, so $Σ_{0}$ is satisfiable. Thus $Σ$ is finitely satisfiable, and by compactness satisfiable — the infinite map is four-colorable.

Compactness lifts finite four-colorability to an infinite map: every finite portion is colorable by the finite theorem, and compactness assembles the finite colorings into one coloring of the whole.

Effectiveness and decidability

The truth-table method matters not only for what it computes but for the fact that a mechanical procedure computes it. An effective procedure is one with finite instructions, executable mechanically without insight, that for a decision problem halts on every input with yes or no after finitely many steps. No bound on running time or scratch space is imposed in advance; effectiveness is the limiting notion with all practical resource limits removed. The word stays informal here; a precise counterpart, recursive, arrives with the recursive functions. Positive claims — that some effective procedure exists — need only the informal notion: exhibit the procedure and its effectiveness is evident.

A counting argument bounds how much can be decidable. There are uncountably many ( $2^{ℵ_{0}}$ ) sets of expressions, but only countably many effective procedures, since each is fixed by a finite instruction text over a finite alphabet. Most sets of expressions are therefore undecidable; the interest is in which specific ones are decidable.

The parsing algorithm decides wffhood; the truth-table method decides implication for finite premise sets. As a corollary, the tautological consequences of a finite $Σ$ form a decidable set — in particular, the set of tautologies is decidable.

Tautologyhood is decidable: a formula enters, the procedure builds its truth table, and after finitely many rows it answers yes or no.

The gap between decidable and enumerable

Decidability is symmetric between yes and no; effective enumerability is only half of it. Two theorems place the boundary.

Enumerability equals semidecidability. A set is effectively enumerable iff it is semidecidable — listing the members and saying yes on members are interchangeable, by dovetailing tests across all expressions and increasing time budgets.
Kleene's complementation theorem. A set is decidable iff both it and its complement are effectively enumerable. Run two semidecision procedures in parallel — one for the set, one for its complement — and whichever halts first decides membership.

Class	Guarantee	Missing
Decidable	halts with yes or no on every input	—
Effectively enumerable	halts with yes on members	may never halt on non-members

For an infinite premise set the symmetry can break. If $Σ$ is merely decidable (or even just effectively enumerable), its set of tautological consequences is effectively enumerable but not necessarily decidable.

The search over finite subsets is what a proof would make explicit. Reading each line as a tautology, a premise, or a modus-ponens step gives a finite certificate of consequence.

Worked example. Give a deduction from $Σ = {(\neg S \lor R), (R \to P), S}$ ending in $P$ , where each line is a tautology, a member of $Σ$ , or follows from two earlier lines by modus ponens.

Line	Formula	Justification
1	$S$	member of $Σ$
2	$(\neg S \lor R)$	member of $Σ$
3	$((\neg S \lor R) \to (S \to R))$	tautology
4	$(S \to R)$	modus ponens, lines 2, 3
5	$R$	modus ponens, lines 1, 4
6	$(R \to P)$	member of $Σ$
7	$P$	modus ponens, lines 5, 6

Line 3 is a tautology because $(\neg S \lor R)$ tautologically implies $(S \to R)$ . Every line is a tautological consequence of $Σ$ , so $Σ ⊨ P$ ; the sequence is the finite certificate the search above would find.

Provability tends to be effectively enumerable — proofs can be searched — while the matching decidability can fail. The set of valid first-order sentences is effectively enumerable (by completeness) yet undecidable, and arithmetic truth is not even effectively enumerable.

Enderton, §1.7 — the compactness theorem, its proof by a maximal finitely satisfiable extension (with the Zorn's-lemma alternative), Corollary 17A, and the effectiveness notions: decidability, effective enumerability, Theorems 17B–17G. ↩
Enderton, §1.7, Exercise 4 — coloring a countable infinite planar map with four colors by applying compactness to the finite four-color theorem. ↩

The compactness theorem

Proof by maximal extension

Compactness for consequence

Coloring an infinite graph

Effectiveness and decidability

The gap between decidable and enumerable

Footnotes