---
title: The Soundness Theorem
module: The Deductive Calculus and Its Metatheorems
moduleNumber: 4
lessonNumber: 3
order: 403
summary: >
  Soundness is the easy half of the match between proof and truth. Whatever the
  calculus deduces is logically implied, by an induction on deduction length that
  rests on one lemma: every logical axiom is valid. The only hard case, quantifier
  instantiation, needs the substitution lemma. The contrapositive corollary states
  that every satisfiable set is consistent.
topics: [The Deductive Calculus and Its Metatheorems]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.5 Soundness and Completeness Theorems (soundness)"
draft: false
---

The [deductive calculus](/logic/deductive-calculus/a-deductive-calculus) was
built by syntactic fiat: six axiom schemas and modus ponens, defined without any
reference to structures or truth. Nothing so far guarantees the two sides agree.
Soundness supplies one direction of the agreement, that deduction never proves a
falsehood.

> **Theorem (Soundness).** If $\Gamma \vdash \varphi$, then $\Gamma \models
> \varphi$.

The proof rests on two observations:
logical axioms are logically implied by anything (being valid), and modus ponens
preserves logical implication. Both are folded into an induction on the length of
the deduction.

## The induction on deductions

Fix $\Gamma$. We show by induction that every $\varphi$ deducible from $\Gamma$
satisfies $\Gamma \models \varphi$. The three cases match the definition of a
deduction line.

- **$\varphi$ a logical axiom.** By the lemma below, $\models \varphi$ (it is
  valid), so a fortiori $\Gamma \models \varphi$.
- **$\varphi \in \Gamma$.** Then $\Gamma \models \varphi$ trivially.
- **$\varphi$ from modus ponens on $\psi$ and $\psi \to \varphi$.** By the
  inductive hypothesis $\Gamma \models \psi$ and $\Gamma \models (\psi \to
  \varphi)$; any structure and assignment satisfying $\Gamma$ then satisfies both,
  hence satisfies $\varphi$.

$$
% caption: Soundness by induction on deduction length. Each line is valid, in the
% hypotheses, or inferred by modus ponens; validity propagates down the sequence.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  line/.style={draw, minimum width=15mm, minimum height=8mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[line]  (a0) at (0,0)   {axiom};
\node[line]  (a1) at (2.2,0) {hyp.};
\node[line]  (a2) at (4.4,0) {axiom};
\node[line] (a3) at (7.0,0) {modus\\ponens};
\node[line] (a4) at (9.6,0) {conclusion};
\draw[->, acc, thick] (a0.south) .. controls (2.5,-1.7) and (6.0,-1.7) .. (a3.250);
\draw[->, acc, thick] (a2.south) .. controls (5.2,-0.9) and (6.3,-0.9) .. (a3.290);
\draw[->, acc, thick] (a3.east) -- (a4.west);
\node[align=center, black] at (4.8,-2.2) {every earlier line is logically implied by the hypotheses};
\end{tikzpicture}
$$

Everything reduces to the lemma.

> **Lemma (Validity of the logical axioms).** Every logical axiom is valid.

Any generalization of a valid formula is valid, so it suffices to check the
schemas themselves, not their generalizations. We take the groups roughly in
order of difficulty.

## Validity of the axiom groups

The sentential and equality groups are quick.

| Group | Schema | Why valid |
| --- | --- | --- |
| 1 | tautologies | a tautologically valid wff is logically valid[^ch1] |
| 3 | $\forall x(\alpha \to \beta) \to (\forall x\, \alpha \to \forall x\, \beta)$ | direct from the satisfaction clauses for $\forall$ and $\to$ |
| 4 | $\alpha \to \forall x\, \alpha$, $x$ not free in $\alpha$ | the value of $\alpha$ is independent of $x$ |
| 5 | $x = x$ | $s(x) = s(x)$ always holds |
| 6 | $x = y \to (\alpha \to \alpha')$, $\alpha$ atomic | equal terms have equal values |

Group 1 uses the fact that a truth assignment on prime formulas induced by a
structure $\fA$ and assignment $s$ agrees with satisfaction: $v(\alpha)
= T$ iff $\models_{\fA} \alpha[s]$. So a tautology is satisfied by every
$\fA, s$, i.e. valid.[^ch1]

Group 4 is worth spelling out. The claim is that $\alpha \to \forall x\, \alpha$ is valid _when
$x$ is not free in $\alpha$_. Take any $\fA, s$ with
$\models_{\fA} \alpha[s]$. To get $\models_{\fA} \forall x\,
\alpha[s]$ we must show $\models_{\fA} \alpha[s(x \mid d)]$ for every $d
\in |\fA|$. But $s$ and $s(x \mid d)$ differ only at $x$, and $x$ is not
free in $\alpha$, so $\alpha$ has the same truth value under both.[^free] That the
value of $\alpha$ stays blind to the reassignment follows from the freeness side
condition. Drop it and the schema fails: $Px \to \forall x\, Px$ is not valid.

Group 6 needs a small term fact. Suppose $\models_{\fA} x = y\,[s]$, i.e.
$s(x) = s(y)$. Then replacing $x$ by $y$ at some places in a term $t$ leaves its
value unchanged: $s(t) = s(t')$ (an induction on $t$). For an atomic $\alpha =
(t_1 = t_2)$ this gives $\models_{\fA} \alpha[s]$ iff
$\models_{\fA} \alpha'[s]$, and similarly for $\alpha = Pt_1 \cdots t_n$,
where equal argument values put the same tuple into or out of $P^{\fA}$.
Hence $\{x = y, \alpha\} \models \alpha'$, which is the group-6 schema.

> **Worked example.** Verify that $x = y \to Pzfx \to Pzfy$ is valid, where $f$ is
> a one-place function symbol and $P$ a two-place predicate. Fix any $\fA, s$ and
> suppose the two antecedents hold. From $\models_{\fA} x = y\,[s]$ comes $s(x) =
> s(y)$, so applying $f^{\fA}$ to equal inputs gives equal outputs:
> $$
> s(fx) = f^{\fA}(s(x)) = f^{\fA}(s(y)) = s(fy).
> $$
> From $\models_{\fA} Pzfx\,[s]$ comes $\langle s(z), s(fx)\rangle \in P^{\fA}$.
> Substituting the equal value $s(fy)$ for $s(fx)$ keeps the pair in $P^{\fA}$, so
> $\langle s(z), s(fy)\rangle \in P^{\fA}$, i.e. $\models_{\fA} Pzfy\,[s]$. The
> conditional holds under every $\fA, s$, so it is valid. This is the group-6
> congruence propagated one function symbol and one predicate deep.

Quantifier instantiation is the one hard group. The schema $\forall x\, \alpha \to
\alpha^x_t$ replaces the variable $x$ by a whole term $t$, so validity has to
connect a statement about a _reassigned variable_ (what $\forall$ ranges over) to a
statement about a _substituted term_ (what the axiom writes). The substitution
lemma links the two.

## The substitution lemma

Group 2 asserts $\forall x\, \alpha \to \alpha^x_t$ is valid whenever $t$ is
substitutable for $x$ in $\alpha$. The atomic-like special case $\forall x\, Px
\to Pt$ is easy: from $\models_{\fA} \forall x\, Px\,[s]$ we get
$\models_{\fA} Px\,[s(x \mid d)]$ for every $d$, and taking $d = s(t)$
lands on $\models_{\fA} Pt\,[s]$. The substitution lemma provides, in general, the
passage from the modified-assignment statement to the substituted-formula
statement. It rests on a companion fact about terms.

> **Lemma (Term substitution).** For a term $u$, $s(u^x_t) = s(x \mid s(t))(u)$.

A substitution can be carried out either _in the term_ $u$ or _in the assignment_
$s$, with the same value.

> **Proof.** Induction on $u$: for a constant or a variable other than $x$, both
> sides reduce to $s(u)$; for $u = x$, both reduce to $s(t)$; the function-symbol
> step is routine. $\blacksquare$

> **Lemma (Substitution).** If $t$ is substitutable for $x$ in $\varphi$, then
> $$
> \models_{\fA} \varphi^x_t\,[s]
> \quad\text{iff}\quad
> \models_{\fA} \varphi\,[s(x \mid s(t))].
> $$

The same claim one level up: substitute inside $\varphi$, or reassign $x$ to the
value of $t$, and satisfaction is unchanged. The substitutability hypothesis is
what makes the two operations commute.

$$
% caption: The substitution lemma as a commuting square: substituting the term
% then evaluating gives the same truth value as reassigning the variable then
% evaluating.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=34mm, minimum height=11mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (f)  at (0,1.7)  {formula};
\node[box] (fs) at (6.8,1.7){formula with term put in};
\node[box] (r)  at (0,-1.0) {value under reassigned s};
\node[box, draw=acc, thick, fill=acc!12] (v) at (6.8,-1.0) {same truth value};
\draw[->, thick] (f) -- (fs) node[midway, above, black] {substitute term};
\draw[->, thick] (fs) -- (v) node[midway, right, black] {evaluate};
\draw[->, thick] (f) -- (r) node[midway, left, black] {reassign variable};
\draw[->, thick] (r) -- (v) node[midway, below, black] {evaluate};
\end{tikzpicture}
$$

> **Proof of the substitution lemma.** Induction on $\varphi$, for every $s$.
>
> - **Atomic.** From the term lemma. E.g. $\models_{\fA} Pu^x_t\,[s]$ iff
>   $s(u^x_t) \in P^{\fA}$ iff $s(x \mid s(t))(u) \in P^{\fA}$ iff
>   $\models_{\fA} Pu\,[s(x \mid s(t))]$.
> - **$\neg\psi$ and $\psi \to \theta$.** Immediate from the inductive hypotheses.
> - **$\forall y\, \psi$ with $x$ not free.** Then $s$ and $s(x \mid s(t))$ agree on
>   the free variables of $\varphi$, and $\varphi^x_t = \varphi$, so both sides
>   coincide.
> - **$\forall y\, \psi$ with $x$ free.** Substitutability forces $y$ not to occur
>   in $t$ and $t$ substitutable for $x$ in $\psi$. The first gives $s(t) = s(y \mid
>   d)(t)$ for every $d$. Since $x \ne y$, $\varphi^x_t = \forall y\, \psi^x_t$, and
>   a chase through the inductive hypothesis and the $\forall$ clause closes the
>   case. $\blacksquare$

Applying it to group 2: from $\models_{\fA} \forall x\, \varphi\,[s]$ we
get $\models_{\fA} \varphi\,[s(x \mid d)]$ for all $d$, in particular
$d = s(t)$, so $\models_{\fA} \varphi\,[s(x \mid s(t))]$, and the
substitution lemma delivers $\models_{\fA} \varphi^x_t\,[s]$. Hence
$\forall x\, \varphi \to \varphi^x_t$ is valid. Every logical axiom is valid, and
the soundness theorem is proved.

## Consequences

Soundness draws the containment $\vdash\ \subseteq\ \models$: every deducible pair
is a logical-implication pair. It is a one-way inclusion until
[completeness](/logic/deductive-calculus/completeness-and-consistency) closes the
loop.

$$
% caption: Soundness places the syntactic consequence relation inside the
% semantic one; completeness will prove the two coincide.
\begin{tikzpicture}[font=\footnotesize]
\definecolor{acc}{HTML}{4A6FA5}
\draw[thick] (0,0) ellipse (3.9 and 2.3);
\draw[thick, fill=acc!14] (-0.9,0) ellipse (1.9 and 1.35);
\node at (-0.9,0) {deducible};
\node at (2.0,0.9) {logically implied};
\node[black, align=center] at (0,-2.95) {soundness: the inner region\\sits inside the outer};
\end{tikzpicture}
$$

Read the other way, soundness proves _non_-derivability: a single countermodel to
$\Gamma \models \varphi$ certifies $\Gamma \nvdash \varphi$.

> **Worked example.** Show $Px \nvdash \forall x\, Px$. By the contrapositive of
> soundness it suffices to refute $Px \models \forall x\, Px$. Take $\fA$ with
> universe $\{a, b\}$, $P^{\fA} = \{a\}$, and $s(x) = a$. Then $\models_{\fA}
> Px\,[s]$, since $s(x) = a \in P^{\fA}$. But $\forall x\, Px$ fails at $s$:
> reassigning $x$ to $b$ gives $\not\models_{\fA} Px\,[s(x \mid b)]$, because $b
> \notin P^{\fA}$. So $Px \not\models \forall x\, Px$, hence $Px \nvdash \forall x\,
> Px$. The [generalization
> theorem](/logic/deductive-calculus/deduction-theorem-and-derived-rules) forbids
> generalizing on a variable free in the hypotheses for exactly this reason.

$$
% caption: A two-element countermodel separating Px from the universal: P holds of
% the assigned element but not the other, so the universal statement fails at s.
\begin{tikzpicture}[font=\footnotesize, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
\definecolor{red}{HTML}{B23A48}
\draw[draw=acc, thick] (0,0) ellipse (2.7 and 1.5);
\node[draw=acc, thick, circle, minimum size=9mm, fill=acc!14] (a) at (-1.0,0) {a};
\node[draw=red, thick, circle, minimum size=9mm, fill=red!7] (b) at (1.0,0) {b};
\node[acc] at (-1.0,-1.05) {P holds};
\node[red] at (1.0,-1.05) {P fails};
\node[black] at (0,1.85) {universe with two elements};
\node[black, align=center] at (0,-2.25) {the assignment sends the variable to the left element};
\end{tikzpicture}
$$

Two equivalence corollaries and one reformulation follow.

> **Corollary.** If $\vdash (\varphi \leftrightarrow \psi)$, then $\varphi$ and
> $\psi$ are logically equivalent. If $\varphi'$ is an alphabetic variant of
> $\varphi$, then $\varphi$ and $\varphi'$ are logically equivalent.

The second half validates the
[alphabetic-variant](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
maneuver semantically: renaming bound variables never changes truth. Both are
pure applications of soundness. For the first, $\vdash (\varphi \leftrightarrow
\psi)$ gives $\models (\varphi \leftrightarrow \psi)$, i.e. $\varphi$ and $\psi$
agree in every $\fA, s$. This is the licence to swap provably equivalent
formulas inside a larger context, used constantly in practice.

The reformulation is the one used throughout the completeness argument. Recall a
set is **consistent** iff no $\varphi$ has both $\Gamma \vdash \varphi$ and
$\Gamma \vdash \neg\varphi$, and **satisfiable** iff some $\fA, s$
satisfies every member.

> **Corollary.** If $\Gamma$ is satisfiable, then $\Gamma$ is consistent.

> **Proof.** Suppose $\Gamma$ is satisfiable but inconsistent. Inconsistency gives
> $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$ for some $\varphi$; by
> soundness $\Gamma \models \varphi$ and $\Gamma \models \neg\varphi$. A satisfying
> $\fA, s$ for $\Gamma$ would then satisfy both $\varphi$ and $\neg\varphi$,
> impossible. $\blacksquare$

$$
% caption: The contrapositive form of soundness used in the completeness proof:
% having a model rules out deriving a contradiction.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=34mm, minimum height=12mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (sat) at (0,0) {a structure makes\\every member true};
\node[box] (con) at (6.0,0) {no contradiction\\(consistent)};
\draw[->, acc, very thick] (sat.east) -- (con.west) node[midway, above, black] {soundness};
\end{tikzpicture}
$$

> **Worked example.** Consistency by a model. The set
> $$
> \Gamma = \{\forall x\, \neg(x < x),\ \forall x\, \forall y\, \forall z(x < y \to
> y < z \to x < z),\ \forall x\, \exists y\; x < y\}
> $$
> (irreflexivity, transitivity, no maximum) is consistent. Exhibit one model:
> $(\mathbb{N}, <)$ satisfies all three, since $<$ on $\mathbb{N}$ is irreflexive
> and transitive and every $n$ has $n < n + 1$. By the corollary, a satisfiable set
> is consistent, so no deduction from $\Gamma$ produces both some $\beta$ and
> $\neg\beta$. One structure settles a purely syntactic question without inspecting
> a single deduction.

This corollary is in fact _equivalent_ to soundness. One direction is the proof
just given. For the other, suppose every satisfiable set is consistent, and let
$\Gamma \vdash \varphi$; then $\Gamma \cup \{\neg\varphi\}$ is inconsistent (it
proves $\varphi$ and $\neg\varphi$), hence unsatisfiable, which is exactly
$\Gamma \models \varphi$. So the model-flavored statement and the derivation-flavored
statement carry the same content.

The corollary's own converse, that every consistent set is satisfiable, is the
substantive half and is much harder. Soundness follows from checking six schemas
and one rule, a finite local inspection. Its converse must produce a structure
from a consistent set, and a consistent set carries no structure on its face, only
the absence of a derivable contradiction. Building a model out of pure syntax is
the [completeness theorem](/logic/deductive-calculus/completeness-and-consistency).
Everything the calculus reaches is true; the harder claim is that everything true
is reached.

## Sensitivity to the axiom set

Soundness and completeness together measure how exactly $\Lambda$ is tuned;
perturbing the axiom set breaks one theorem or the other.[^perturb]

- **Adding a non-valid axiom breaks soundness.** Suppose $\psi \in \Lambda$
  with $\psi$ not valid. Then $\vdash \psi$ (a one-line deduction) but
  $\not\models \psi$, so $\vdash\ \not\subseteq\ \models$. Soundness is
  the statement that every axiom sits inside the validities, and it fails the
  moment one does not.
- **Removing all axioms breaks completeness.** With $\Lambda = \varnothing$
  the only theorems of $\Gamma$ are the formulas reachable from $\Gamma$ alone
  by modus ponens. Valid formulas such as $x = x$ are then not deducible from
  $\varnothing$, though $\models x = x$.
- **Adding one more valid formula changes nothing.** Both theorems survive: the
  new axiom is valid, so the soundness induction still goes through, and
  enlarging $\Lambda$ only makes more deductions available, so completeness is
  preserved a fortiori.

So the six schemas are not sacred as individual formulas; any decidable set of
valid formulas rich enough to drive the Henkin construction would do. What is
essential is the pair of boundary conditions: nothing invalid gets in
(soundness), and enough gets in to prove every consequence (completeness).

[^ch1]: Enderton, §2.5, treatment of axiom group 1; the induced truth assignment on prime formulas agrees with satisfaction because $\neg$ and $\to$ are handled identically in Chapters 1 and 2 (§2.4, Exercise 3). Lemma 25A collects the validity of all six axiom groups.
[^free]: Enderton, §2.2; the value of a formula under an assignment depends only on the assignment's values at the formula's free variables, so reassigning a non-free variable leaves satisfaction unchanged.
[^perturb]: Enderton, §2.5, Exercise 9: adding a non-valid formula to $\Lambda$ falsifies soundness, taking $\Lambda = \varnothing$ falsifies completeness, and adding a valid formula preserves both.