---
title: The Completeness Theorem
module: The Deductive Calculus and Its Metatheorems
moduleNumber: 4
lessonNumber: 4
order: 404
summary: >
  Gödel's completeness theorem is the deep converse of soundness: whatever is
  logically implied can be deduced. Equivalently, every consistent set has a
  model. The Henkin proof manufactures that model out of syntax alone: add
  witnessing constants, extend to a maximal consistent set, and read a term model
  off the formulas it contains. Compactness and the enumerability theorem drop out.
topics: [The Deductive Calculus and Its Metatheorems]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.5 Soundness and Completeness Theorems (completeness, compactness, enumerability)"
draft: false
---

[Soundness](/logic/deductive-calculus/soundness) gave the easy inclusion
$\vdash\ \subseteq\ \models$. The reverse is the deep theorem of first-order
logic: the syntactic calculus is strong enough to derive _every_ semantic
consequence.

> **Theorem (Completeness; Gödel, 1930).** Let $\Gamma$ be a set of formulas and
> $\varphi$ a formula.
> **(a)** If $\Gamma \models \varphi$, then $\Gamma \vdash \varphi$.
> **(b)** Every consistent set of formulas is satisfiable.

Parts (a) and (b) are equivalent, so it suffices to prove (b). For (b) $\Rightarrow$
(a), $\Gamma \models \varphi$ makes $\Gamma \cup \{\neg\varphi\}$ unsatisfiable,
hence inconsistent by (b), so $\Gamma \vdash \varphi$ by reductio. For (a)
$\Rightarrow$ (b), an unsatisfiable set logically implies every formula, in
particular some $\beta$ and $\neg\beta$, so by (a) it is inconsistent. We prove (b)
for a countable language and indicate the changes for larger cardinalities at the
end. The construction is due to Henkin, and unlike Gödel's original proof it
scales to any cardinality.[^hist]

## Consistency versus satisfiability

Consistency is a syntactic property (no formula and its negation are both
provable); satisfiability is semantic (some structure makes everything true).
Completeness asserts they coincide. Soundness already gave satisfiable $\Rightarrow$
consistent. The hard direction builds a structure from nothing but the formulas,
so the model's elements must _be_ syntax. The plan extends $\Gamma$ to a set
$\Delta$ so saturated that a structure can be read directly off it.

$$
% caption: The completeness proof as a pipeline: enrich the language and the set
% until a model can be read off the formulas, then quotient by equality.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  st/.style={draw, minimum width=25mm, minimum height=14mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[st] (c) at (0,0)    {consistent\\set};
\node[st] (w) at (3.3,0)  {add witnessing\\constants};
\node[st] (m) at (6.6,0)  {maximal\\consistent set};
\node[st] (t) at (9.9,0)  {term\\model};
\node[st] (q) at (13.2,0) {quotient\\by equality};
\draw[->, thick] (c) -- (w);
\draw[->, thick] (w) -- (m);
\draw[->, thick] (m) -- (t);
\draw[->, thick] (t) -- (q);
\node[black] at (0,-1.4) {given};
\node[black] at (4.95,-1.4) {steps 1 and 2};
\node[black] at (9.9,-1.4) {step 4};
\node[black] at (13.2,-1.4) {steps 5 and 6};
\end{tikzpicture}
$$

Fix a consistent set $\Gamma$ in a countable language. The target is a set
$\Delta \supseteq \Gamma$ with two properties:

- **maximal consistent**: consistent, and for every $\alpha$, either $\alpha \in
  \Delta$ or $\neg\alpha \in \Delta$;
- **witnessing (Henkin)**: for every $\varphi$ and $x$, some constant $c$ has
  $(\neg\forall x\, \varphi \to \neg\varphi^x_c) \in \Delta$.

Maximality decides every formula; the witnessing property ensures that whenever
$\Delta$ denies a universal, it names a specific counterexample. Those two
features supply what the satisfaction recursion needs.

## Step 1: witnessing constants

Expand the language with a countably infinite set of new constant symbols. As a
set of wffs in the larger language, $\Gamma$ stays consistent.

If not, some $\beta$ has a deduction of $\beta \wedge \neg\beta$ from $\Gamma$ in
the expanded language. A deduction is finite, so it uses only finitely many new
constants; by [generalization on
constants](/logic/deductive-calculus/deduction-theorem-and-derived-rules) each may
be replaced by a variable, yielding a deduction of $\beta' \wedge \neg\beta'$ from
$\Gamma$ in the _original_ language. That contradicts the consistency of $\Gamma$.

## Step 2: Henkin axioms

For each pair $\varphi, x$ we want to add the sentence

$$
\theta \colon\quad \neg\forall x\, \varphi \to \neg\varphi^x_c,
$$

where $c$ is a new constant. The reading: $c$ names a counterexample
to $\varphi$, should one exist. Enumerate all pairs $\langle \varphi_1, x_1
\rangle, \langle \varphi_2, x_2 \rangle, \dots$ (possible since the language is
countable). Define $\theta_n = (\neg\forall x_n\, \varphi_n \to
\neg(\varphi_n)^{x_n}_{c_n})$, taking $c_n$ to be the first new constant occurring in neither
$\varphi_n$ nor any earlier $\theta_k$. Let $\Theta = \{\theta_1, \theta_2,
\dots\}$. Then $\Gamma \cup \Theta$ is consistent.

Suppose not. Deductions are finite, so $\Gamma \cup \{\theta_1, \dots,
\theta_{m+1}\}$ is inconsistent for a least $m$. By reductio,

$$
\Gamma \cup \{\theta_1, \dots, \theta_m\} \vdash \neg\theta_{m+1}.
$$

Now $\theta_{m+1}$ is $\neg\forall x\, \varphi \to \neg\varphi^x_c$, so rule T
extracts both $\Gamma \cup \{\theta_1, \dots, \theta_m\} \vdash \neg\forall x\,
\varphi$ and $\Gamma \cup \{\theta_1, \dots, \theta_m\} \vdash \varphi^x_c$. The
constant $c$ occurs in none of the formulas on the left, so the corollary to
generalization on constants turns the second into $\Gamma \cup \{\theta_1, \dots,
\theta_m\} \vdash \forall x\, \varphi$. That contradicts the first, and the
leastness of $m$ (or the consistency of $\Gamma$ when $m = 0$). So $\Gamma \cup
\Theta$ is consistent.

> **Worked example.** Make one Henkin axiom concrete. For $\varphi = Px$ and the
> variable $x$, with new constant $c$, the sentence is
> $$
> \theta \colon\quad \neg\forall x\, Px \to \neg Pc.
> $$
> Trace both directions of its effect once $\theta$ sits in the saturated set
> $\Delta$. If $\Delta$ denies the universal, $\neg\forall x\, Px \in \Delta$, then
> modus ponens against $\theta$ forces $\neg Pc \in \Delta$: the constant $c$ is a
> named counterexample. Conversely, $\theta$ tautologically implies its
> contrapositive $Pc \to \forall x\, Px$, so if $Pc \in \Delta$ then deductive
> closure forces $\forall x\, Px \in \Delta$. The single witness $c$ decides the
> universal $\forall x\, Px$ inside $\Delta$, as the satisfaction recursion needs
> at the quantifier step.

$$
% caption: The Henkin axiom in force: whenever the saturated set denies a
% universal, its witnessing constant names a specific counterexample inside it.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=48mm, minimum height=12mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (u) at (0,0) {the set denies a universal};
\node[box] (w) at (7.8,0) {a named constant fails the formula};
\draw[->, acc, very thick] (u.east) -- (w.west) node[midway, above, black] {Henkin axiom} node[midway, below, black] {witness};
\end{tikzpicture}
$$

## Step 3: a maximal consistent extension

Extend the consistent $\Gamma \cup \Theta$ to a set $\Delta$ that is maximal:
consistent, with $\alpha \in \Delta$ or $\neg\alpha \in \Delta$ for every wff
$\alpha$. One route imitates the sentential
[compactness](/logic/sentential-logic/compactness-and-effectiveness) construction.
A cleaner route uses
[the tautological-implication characterization of deducibility](/logic/deductive-calculus/a-deductive-calculus): since $\Gamma \cup
\Theta$ is consistent, $\Gamma \cup \Theta \cup \Lambda$ does not tautologically
imply any $\beta \wedge \neg\beta$, so some truth assignment $v$ on the prime
formulas satisfies $\Gamma \cup \Theta \cup \Lambda$. Set

$$
\Delta = \{\varphi : v(\varphi) = T\}.
$$

For every $\varphi$, exactly one of $\varphi, \neg\varphi$ lies in $\Delta$.
Moreover $\Delta$ is **deductively closed**: if $\Delta \vdash \varphi$, then by
consistency $\Delta \nvdash \neg\varphi$, so $\neg\varphi \notin \Delta$, so
$\varphi \in \Delta$ by maximality.

$$
% caption: A maximal consistent set decides every formula. Extending the given
% set, each formula or its negation is admitted, never both, climbing to a set
% that is deductively closed.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  lv/.style={draw, minimum width=30mm, minimum height=9mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[lv] (g) at (0,0)   {given consistent set};
\node[lv] (g1) at (0,1.3){decide one formula};
\node[lv] (g2) at (0,2.6){decide another formula};
\node[lv, draw=acc, thick, fill=acc!12] (top) at (0,4.0) {maximal consistent set};
\draw[->, thick] (g) -- (g1);
\draw[->, thick] (g1) -- (g2);
\draw[->, thick, dashed] (g2) -- (top);
\node[black, align=left, anchor=west] at (2.4,0.65) {admit the formula};
\node[black, align=left, anchor=west] at (2.4,1.95) {or its negation};
\node[black, align=left, anchor=west] at (2.4,3.3) {never both};
\end{tikzpicture}
$$

At this point $\Delta$ decides every sentence and, thanks to $\Theta$, names a
witness against every denied universal. It remains to turn $\Delta$ into a
structure.

## Step 4: the term model

Build a preliminary structure $\fA$ whose universe is the syntax itself.
If the language has equality, first replace $=$ by a fresh two-place predicate
symbol $E$; write $\varphi^{\ast}$ for the result of that replacement in $\varphi$.

> **Definition (Term model).** Let $\fA$ have:
> - **universe** $|\fA| = $ the set of all terms of the expanded language;
> - $\langle u, t \rangle \in E^{\fA}$ iff $(u = t) \in \Delta$;
> - $\langle t_1, \dots, t_n \rangle \in P^{\fA}$ iff $Pt_1 \cdots t_n
>   \in \Delta$, for each predicate symbol $P$;
> - $f^{\fA}(t_1, \dots, t_n) = ft_1 \cdots t_n$, for each function
>   symbol $f$; in particular $c^{\fA} = c$ for constants.

Take $s\colon V \to |\fA|$ to be the identity, $s(x) = x$. Then $s(t) = t$
for every term $t$ (induction on $t$). The core claim links satisfaction to
membership.

> **Lemma (Truth = membership).** For every wff $\varphi$,
> $\models_{\fA} \varphi^{\ast}[s]$ iff $\varphi \in \Delta$.

> **Proof.** Induction on the number of connective and quantifier symbols in
> $\varphi$.
>
> - **Atomic.** By construction. For $Pt$: $\models_{\fA} Pt[s]$ iff $s(t)
>   \in P^{\fA}$ iff $t \in P^{\fA}$ iff $Pt \in \Delta$. For $u =
>   t$: $\models_{\fA} uEt[s]$ iff $\langle u, t \rangle \in E^{\fA}$
>   iff $(u = t) \in \Delta$.
> - **Negation.** $\models_{\fA} (\neg\varphi)^{\ast}[s]$ iff not
>   $\models_{\fA} \varphi^{\ast}[s]$ iff $\varphi \notin \Delta$ (inductive
>   hypothesis) iff $\neg\varphi \in \Delta$ (maximality).
> - **Conditional.** $\models_{\fA} (\varphi \to \psi)^{\ast}[s]$ iff
>   $\varphi \notin \Delta$ or $\psi \in \Delta$, which, since $\Delta$ is maximal
>   and deductively closed, holds iff $(\varphi \to \psi) \in \Delta$.
> - **Quantifier.** The forward direction of $\models_{\fA} \forall x\,
>   \varphi^{\ast}[s]$ iff $\forall x\, \varphi \in \Delta$ is where $\Theta$ is
>   used: if $\varphi^{\ast}$ is true of everything it is true of the witness
>   $c$, so $\varphi^x_c \in \Delta$; the Henkin axiom $\neg\forall x\, \varphi \to
>   \neg\varphi^x_c$ then forces $\forall x\, \varphi \in \Delta$. The converse uses
>   the [substitution lemma](/logic/deductive-calculus/soundness), repaired with an
>   [alphabetic variant](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
>   when the witness term is not substitutable. $\blacksquare$

If the language has no equality, we are done: restricting $\fA$ to the
original language gives a structure satisfying every member of $\Gamma$ with the
identity assignment.

## Steps 5 and 6: quotient by equality

With equality present, $\fA$ is wrong: it may contain distinct terms $c,
d$ with $(c = d) \in \Delta$, yet $c^{\fA} = c \ne d = d^{\fA}$.
The fix collapses $E$-equivalent terms. By the [equality
facts](/logic/deductive-calculus/deduction-theorem-and-derived-rules) Eq1–Eq5,
$E^{\fA}$ is a **congruence**: an equivalence relation (Eq1–Eq3)
compatible with every predicate (Eq4) and function (Eq5).

> **Definition (Quotient structure).** $\fA/E$ has universe the
> $E$-classes $[t]$, with $\langle [t_1], \dots, [t_n]\rangle \in
> P^{\fA/E}$ iff $\langle t_1, \dots, t_n \rangle \in P^{\fA}$,
> and $f^{\fA/E}([t_1], \dots, [t_n]) = [f^{\fA}(t_1, \dots,
> t_n)]$. The natural map $h(t) = [t]$ is a homomorphism onto $\fA/E$.

Congruence makes these definitions independent of representatives, so
$\fA/E$ is well defined, and $E^{\fA/E}$ is the genuine equality
relation on the classes.

> **Worked example.** Follow the quotient merging two forced-equal terms. Suppose
> constants $c, d$ both occur, $(c = d) \in \Delta$, and $Pc \in \Delta$ for a
> unary $P$. In the term model $\fA$ the elements $c$ and $d$ are distinct terms,
> yet $\langle c, d\rangle \in E^{\fA}$ because $(c = d) \in \Delta$. Predicate
> compatibility (Eq4) also puts $Pd \in \Delta$, so $c, d \in P^{\fA}$. The
> quotient collapses them into one class $[c] = [d]$, and $P^{\fA/E}$ contains that
> single class. Congruence is what makes this well defined: the class lies in
> $P^{\fA/E}$ independent of the representative, since $Pc \in \Delta$ iff $Pd \in
> \Delta$.

By the homomorphism theorem, for every $\varphi$,

$$
\varphi \in \Delta
\;\iff\; \models_{\fA} \varphi^{\ast}[s]
\;\iff\; \models_{\fA/E} \varphi^{\ast}[h \circ s]
\;\iff\; \models_{\fA/E} \varphi\,[h \circ s].
$$

$$
% caption: The term model, then its quotient. Distinct terms that the set forces
% equal are merged into one element, so the interpreted equality symbol becomes
% real identity.
\begin{tikzpicture}[font=\footnotesize, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% left: terms
\node[black] at (0,2.2) {terms};
\foreach \p/\n in {(-0.6,1.3)/t1, (0.6,1.5)/t2, (-0.4,0.2)/t3, (0.7,0.3)/t4, (0,-1.0)/t5}
  \fill \p circle (2.6pt);
\draw[draw=acc, thick] (0,0.8) ellipse (1.3 and 1.1);
\draw[draw=acc, thick] (0.15,-1.05) ellipse (1.0 and 0.5);
\node[black] at (0,-2.2) {two equality classes};
% arrow
\draw[->, very thick] (2.0,0) -- (3.6,0) node[midway, above, black] {quotient};
% right: classes as points
\begin{scope}[xshift=5.6cm]
\node[black] at (0,2.2) {quotient};
\node[draw=acc, thick, circle, minimum size=6mm, fill=acc!12] at (0,0.8) {};
\node[draw=acc, thick, circle, minimum size=6mm, fill=acc!12] at (0,-0.8) {};
\node[black] at (0,-2.2) {one point each};
\end{scope}
\end{tikzpicture}
$$

Restricting $\fA/E$ to the original language gives a structure satisfying
every member of $\Gamma$ with $h \circ s$. So the consistent $\Gamma$ is
satisfiable, proving part (b) and with it the completeness theorem.

| Step | Action | Property secured |
| --- | --- | --- |
| 1 | add new constants | room for witnesses; consistency preserved |
| 2 | add Henkin axioms $\neg\forall x\, \varphi \to \neg\varphi^x_c$ | a named counterexample for every denied universal |
| 3 | extend to $\Delta$ maximal consistent | every formula decided; deductively closed |
| 4 | build the term model $\fA$ | satisfaction equals membership in $\Delta$ |
| 5 | quotient by the congruence $E$ | interpreted $=$ becomes real identity |
| 6 | restrict to the original language | a model of $\Gamma$ itself |

For an uncountable language of cardinality $\lambda$, three changes suffice: add
$\lambda$ new constants in step 1; index the pairs by ordinals below $\lambda$ in
step 2 (at each stage only $\aleph_0 \cdot \card(\alpha)$ constants
are excluded, leaving some free); and obtain the maximal set in step 3 by Zorn's
lemma. Everything else is unchanged.[^unc]

## Consistency equals satisfiability

Completeness (b) with the soundness corollary gives the full equivalence.

> **Corollary.** A set of formulas is consistent if and only if it is satisfiable.

The model-theoretic consequences rest on this equivalence. Consistency is
syntactic and _finitary_ (deductions are finite); satisfiability is semantic. The
equivalence transports finiteness from one side to the other.

$$
% caption: The two theorems close a loop. Soundness runs one way, completeness the
% other, so the syntactic and semantic consequence relations coincide.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=34mm, minimum height=13mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (l) at (0,0)   {deducible\\(syntax)};
\node[box] (r) at (6.4,0) {logically implied\\(semantics)};
\draw[->, acc, very thick] (l.north east) ++(-0.2,0) .. controls (3.2,1.5) .. (r.north west) node[midway, above, black] {soundness};
\draw[<-, acc, very thick] (l.south east) ++(-0.2,0) .. controls (3.2,-1.5) .. (r.south west) node[midway, below, black] {completeness};
\node[black] at (3.2,0) {coincide};
\end{tikzpicture}
$$

## Compactness and enumerability

Two further theorems, provable independently, are immediate from completeness.
They underpin the [model
theory](/logic/models-and-theories/compactness-and-lowenheim-skolem) built on
first-order logic.

> **Theorem (Compactness).** **(a)** If $\Gamma \models \varphi$, then $\Gamma_0
> \models \varphi$ for some finite $\Gamma_0 \subseteq \Gamma$. **(b)** If every
> finite subset of $\Gamma$ is satisfiable, then $\Gamma$ is satisfiable.

> **Proof.** (a) $\Gamma \models \varphi$ gives $\Gamma \vdash \varphi$
> (completeness), whose deduction uses a finite $\Gamma_0 \subseteq \Gamma$, so
> $\Gamma_0 \vdash \varphi$, so $\Gamma_0 \models \varphi$ (soundness). (b) If every
> finite subset is satisfiable, then by soundness every finite subset is consistent;
> since deductions are finite, $\Gamma$ is consistent, hence satisfiable by
> completeness. $\blacksquare$

Compactness mentions only semantics, yet the shortest route runs through the
deductive calculus. The finiteness it asserts comes entirely from the finiteness
of deductions.

> **Worked example.** Compactness produces an infinite model from arbitrarily
> large finite ones. Suppose $\Gamma$ has, for each $n$, a model with at least $n$
> elements. Add new constants $c_1, c_2, \dots$ and form
> $$
> \Gamma^+ = \Gamma \cup \{\, c_i \ne c_j : i < j \,\}.
> $$
> Any finite subset of $\Gamma^+$ mentions only finitely many constants, say among
> $c_1, \dots, c_n$; a model of $\Gamma$ with at least $n$ elements interprets those
> as distinct and satisfies the subset. By compactness (b), $\Gamma^+$ is
> satisfiable, and its infinitely many distinct $c_i$ force an infinite universe.
> Restricting to the original language leaves an infinite model of $\Gamma$.

The second theorem needs a mild effectiveness assumption. A
language is **reasonable** if its parameters can be effectively enumerated and the
arity relations for predicate and function symbols are decidable; every finite
language qualifies, and a reasonable language is necessarily countable.

> **Theorem (Enumerability).** For a reasonable language, the set of valid wffs
> is effectively enumerable.

> **Proof.** The axiom set $\Lambda$ is decidable: to test an expression $\varepsilon$,
> check that it is a wff, then check membership in each axiom group in turn
> (group 1 by a truth table, groups 2–6 by their syntactic forms); reject if none
> matches. Since $\Lambda$ is decidable, so is the set of deductions from $\varnothing$,
> and the enumeration is the brute-force sweep:

```algorithm
caption: $\textsc{EnumerateValidities}$ — list every valid wff of a reasonable language
for each finite sequence $\alpha_0, \dots, \alpha_n$ of wffs, in order of increasing code do
  if the sequence is a deduction from $\varnothing$ then
    output $\alpha_n$
```

> **Proof (continued).** Every deduction is eventually generated, so every theorem of $\varnothing$ is
> eventually listed, and by completeness the theorems of $\varnothing$ are exactly
> the valid wffs. $\blacksquare$

The same argument relativizes to any decidable set of nonlogical axioms.

> **Corollary.** If $\Delta$ is a decidable set of formulas in a reasonable
> language, the set $\{\varphi : \Delta \models \varphi\}$ is effectively
> enumerable. If in addition $\Delta$ decides every sentence (for each $\sigma$,
> $\Delta \models \sigma$ or $\Delta \models \neg\sigma$), that set is
> **decidable**.

> **Proof of decidability.** If $\Delta$ is inconsistent the set is all sentences,
> trivially decidable. Otherwise, to test $\sigma$, enumerate the consequences of
> $\Delta$ and wait for $\sigma$ or $\neg\sigma$; completeness guarantees one
> appears. $\blacksquare$

A complete decidable theory is therefore decidable, the link to
[categoricity and the Łoś–Vaught
test](/logic/models-and-theories/theories-elementary-classes-and-categoricity).
Enumerability does _not_ in general upgrade to decidability of validity itself:
for almost all languages the valid wffs are undecidable, which is Church's theorem
in the [incompleteness](/logic/incompleteness/incompleteness-and-undecidability)
chapter.

[^hist]: Enderton, §2.5, Historical Notes. The completeness theorem for countable languages is Gödel's 1930 dissertation, with compactness as a corollary; the Henkin-style proof given here is from Henkin's 1949 dissertation and generalizes to any cardinality.
[^unc]: Enderton, §2.5, the paragraph on uncountable languages; $\lambda$ is taken as an initial ordinal and the language well-ordered.