---
title: Compactness and Effectiveness
module: Sentential Logic
moduleNumber: 2
lessonNumber: 7
order: 207
summary: >
  The compactness theorem reduces satisfiability of an infinite set of formulas to
  its finite subsets, proved by extension to a maximal finitely satisfiable set and
  applied to color infinite graphs. Effectiveness fixes what "decidable" and
  "effectively enumerable" mean and settles the decidability of tautologyhood.
topics: [Sentential Logic]
sources:
  - book: Enderton
    ref: "Ch. 1 — Sentential Logic; §1.7 Compactness and Effectiveness"
draft: false
---

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.[^enderton-compact]

## The compactness theorem

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

> **Theorem (Compactness).** A set of wffs is satisfiable iff it is finitely
> satisfiable.

One direction is free: a satisfying assignment for $\Sigma$ satisfies every
subset, so satisfiable implies finitely satisfiable. For finite $\Sigma$ the
converse is trivial, since $\Sigma$ 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.

$$
% caption: 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.
\begin{tikzpicture}[font=\footnotesize,
  fin/.style={draw, minimum width=17mm, minimum height=8mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[black, fill=acc!5] (0,0) ellipse (3.0 and 2.4);
  \node[font=\footnotesize, anchor=south] at (0,2.5) {unbounded set of formulas};
  \node[fin] at (-1.2,0.7) {small\\subset: sat};
  \node[fin] at (1.1,0.9) {small\\subset: sat};
  \node[fin] at (-0.9,-0.9) {small\\subset: sat};
  \node[fin] at (1.2,-0.8) {small\\subset: sat};
  \draw[->, draw=acc, thick] (3.3,0) -- (5.0,0);
  \node[fin, draw=acc, text=acc, minimum width=24mm] at (6.6,0) {one satisfying\\assignment};
\end{tikzpicture}
$$

### Proof by maximal extension

The proof has two parts: enlarge $\Sigma$ 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 $\alpha_1, \alpha_2, \dots$ of all of them. Define a chain by
recursion:

$$
\Delta_0 = \Sigma, \qquad
\Delta_{n+1} = \begin{cases}
\Delta_n; \alpha_{n+1} & \text{if this is finitely satisfiable},\\
\Delta_n; (\neg \alpha_{n+1}) & \text{otherwise},
\end{cases}
$$

where $\Delta_n; \alpha$ abbreviates $\Delta_n \cup \{\alpha\}$. At each step at
least one of the two choices keeps the set finitely satisfiable, so every
$\Delta_n$ is finitely satisfiable. Let $\Delta = \bigcup_n \Delta_n$. Then:

- $\Sigma \subseteq \Delta$;
- for every wff $\alpha$, either $\alpha \in \Delta$ or $(\neg\alpha) \in \Delta$
  (it was decided at stage $n+1$ when $\alpha = \alpha_{n+1}$);
- $\Delta$ is finitely satisfiable — any finite subset lies inside some
  $\Delta_n$, which is finitely satisfiable.

The construction is a walk down a binary tree: at level $n$ it commits to
including $\alpha_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
$\Delta$ instead.

$$
% caption: 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.
\begin{tikzpicture}[font=\footnotesize, level distance=13mm,
  n/.style={draw, circle, minimum size=6mm, inner sep=0pt, font=\scriptsize},
  b/.style={draw=acc, circle, fill=acc!14, minimum size=6mm, inner sep=0pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[b] (r) at (0,0) {};
  \node[n] (l1) at (-2.4,-1.5) {};
  \node[b] (r1) at (2.4,-1.5) {};
  \node[n] (r1l) at (1.1,-3.0) {};
  \node[b] (r1r) at (3.7,-3.0) {};
  \draw[black] (r) -- node[above left, font=\scriptsize] {include} (l1);
  \draw[acc, thick] (r) -- node[above right, font=\scriptsize] {include negation} (r1);
  \draw[black] (r1) -- (r1l);
  \draw[acc, thick] (r1) -- (r1r);
  \node[anchor=west, font=\scriptsize] at (-4.6,0) {premises};
  \node[anchor=west, text=acc, font=\scriptsize] at (4.2,-3.0) {branch kept sat at every stage};
\end{tikzpicture}
$$

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

### Compactness for consequence

The satisfiability form has an implication form, using that $\Sigma \models \tau$
iff $\Sigma; (\neg\tau)$ is unsatisfiable.

> **Corollary (Compactness for tautological consequence).** If $\Sigma \models \tau$, then $\Sigma_0 \models \tau$ for
> some finite $\Sigma_0 \subseteq \Sigma$.

> **Proof.** If _no_ finite $\Sigma_0$ had $\Sigma_0 \models \tau$, then every finite
> $\Sigma_0; (\neg\tau)$ would be satisfiable, so $\Sigma; (\neg\tau)$ would be
> finitely satisfiable, hence satisfiable by compactness, contradicting
> $\Sigma \models \tau$. $\blacksquare$

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.[^enderton-color]
>
> 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 $\Sigma$ collect:
>
> - for each $i$, that $C_i$ gets exactly one color — the disjunction
>   $(A_{i,r} \vee A_{i,g} \vee A_{i,b} \vee A_{i,y})$ and, for each pair of
>   distinct colors $c \ne c'$, the formula $(\neg (A_{i,c} \wedge A_{i,c'}))$;
> - for each pair of adjacent countries $C_i, C_j$ and each color $c$, the formula
>   $(\neg (A_{i,c} \wedge A_{j,c}))$.
>
> A truth assignment satisfying $\Sigma$ is a proper four-coloring of the whole
> map. Any finite $\Sigma_0 \subseteq \Sigma$ mentions finitely many countries,
> which form a finite planar map, four-colorable by the finite theorem, so
> $\Sigma_0$ is satisfiable. Thus $\Sigma$ is finitely satisfiable, and by
> compactness satisfiable — the infinite map is four-colorable.

$$
% caption: 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.
\begin{tikzpicture}[font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{c1}{HTML}{9CB4D8}
  \definecolor{c2}{HTML}{C9D6B0}
  \draw[black, fill=c1] (0,0) rectangle (1.2,1.2);
  \draw[black, fill=c2] (1.2,0) rectangle (2.4,1.2);
  \draw[black, fill=c2] (0,1.2) rectangle (1.2,2.4);
  \draw[black, fill=c1] (1.2,1.2) rectangle (2.4,2.4);
  \node[font=\scriptsize] at (3.4,1.2) {small piece:};
  \node[font=\scriptsize] at (3.4,0.75) {colorable};
  \draw[->, draw=acc, thick] (4.6,1.2) -- (6.0,1.2);
  \node[font=\scriptsize, align=center, text=acc] at (7.6,1.2) {entire map\\colorable};
  \node[font=\scriptsize, anchor=north] at (1.2,-0.2) {a bounded patch of countries};
\end{tikzpicture}
$$

## 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](/logic/computability-and-representability/recursive-functions).
Positive claims — that some effective procedure exists — need only the informal
notion: exhibit the procedure and its effectiveness is evident.

> **Definition (Decidable, semidecidable).** A set $A$ of expressions is
> **decidable** iff some effective procedure, given an expression, decides whether
> it is in $A$. It is **effectively enumerable** (semidecidable) iff some
> procedure lists the members of $A$, equivalently answers "yes" exactly when its
> input is in $A$, possibly never halting otherwise.

A counting argument bounds how much can be decidable. There are uncountably many
($2^{\aleph_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.

> **Theorem (Decidability of tautological consequence).** The set of wffs is decidable, and for a finite set
> $\Sigma; \tau$ it is decidable whether $\Sigma \models \tau$.

The [parsing algorithm](/logic/sentential-logic/unique-readability-and-parsing)
decides wffhood; the truth-table method decides implication for finite premise
sets. As a corollary, the tautological consequences of a finite $\Sigma$ form a
decidable set — in particular, the set of tautologies is decidable.

$$
% caption: Tautologyhood is decidable: a formula enters, the procedure builds its
% truth table, and after finitely many rows it answers yes or no.
\begin{tikzpicture}[font=\footnotesize,
  bx/.style={draw, minimum width=26mm, minimum height=10mm, align=center, font=\scriptsize},
  ok/.style={draw=acc, text=acc, minimum width=18mm, minimum height=9mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[bx] (in) at (0,0) {formula in};
  \node[bx] (tt) at (3.6,0) {check every\\truth-table row};
  \node[ok] (yes) at (7.4,0.8) {tautology: yes};
  \node[ok] (no) at (7.4,-0.8) {some row F: no};
  \draw[->, black] (in) -- (tt);
  \draw[->, black] (tt) -- (yes);
  \draw[->, black] (tt) -- (no);
\end{tikzpicture}
$$

### 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 $\Sigma$ is merely
decidable (or even just effectively enumerable), its set of tautological
consequences is effectively enumerable but not necessarily decidable.

> **Theorem (Effective enumerability of consequences).** If $\Sigma$ is effectively enumerable, the set of tautological
> consequences of $\Sigma$ is effectively enumerable.

> **Proof.** Enumerate $\Sigma$ as $\sigma_1, \sigma_2, \dots$. Given $\tau$, test by
> truth tables successively whether $\varnothing \models \tau$,
> $\{\sigma_1\} \models \tau$, $\{\sigma_1, \sigma_2\} \models \tau$, and so on,
> answering "yes" as soon as one succeeds. By the compactness corollary, if
> $\Sigma \models \tau$ then some finite initial segment already implies $\tau$, so
> the search halts with "yes"; if not, it runs forever. $\blacksquare$

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 $\Sigma = \{(\neg S \vee R), (R \to P), S\}$
> ending in $P$, where each line is a tautology, a member of $\Sigma$, or follows
> from two earlier lines by modus ponens.
>
> | Line | Formula | Justification |
> | --- | --- | --- |
> | 1 | $S$ | member of $\Sigma$ |
> | 2 | $(\neg S \vee R)$ | member of $\Sigma$ |
> | 3 | $((\neg S \vee 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 $\Sigma$ |
> | 7 | $P$ | modus ponens, lines 5, 6 |
>
> Line 3 is a tautology because $(\neg S \vee R)$ tautologically implies
> $(S \to R)$. Every line is a tautological consequence of $\Sigma$, so
> $\Sigma \models 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](/logic/deductive-calculus/completeness-and-consistency)) yet
undecidable, and arithmetic truth is not even effectively enumerable.

[^enderton-compact]: 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-color]: Enderton, §1.7, Exercise 4 — coloring a countable infinite planar map with four colors by applying compactness to the finite four-color theorem.