The Soundness Theorem

The 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.

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 $\phi$ deducible from $\Gamma$ satisfies $\Gamma \models \phi$. The three cases match the definition of a deduction line.

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

Everything reduces to the lemma.

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 1 uses the fact that a truth assignment on prime formulas induced by a structure $\mathfrak{A}$ and assignment $s$ agrees with satisfaction: $v(\alpha )=T$ iff ${\models }_{\mathfrak{A}}\alpha [s]$. So a tautology is satisfied by every $\mathfrak{A},s$, i.e. valid.¹

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 $\mathfrak{A},s$ with ${\models }_{\mathfrak{A}}\alpha [s]$. To get ${\models }_{\mathfrak{A}}\forall x\alpha [s]$ we must show ${\models }_{\mathfrak{A}}\alpha [s(x\mid d)]$ for every $d\in |\mathfrak{A}|$. 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.² 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 xPx$ is not valid.

Group 6 needs a small term fact. Suppose ${\models }_{\mathfrak{A}}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^{\prime })$ (an induction on $t$). For an atomic $\alpha =(t_1=t_2)$ this gives ${\models }_{\mathfrak{A}}\alpha [s]$ iff ${\models }_{\mathfrak{A}}{\alpha }^{\prime }[s]$, and similarly for $\alpha =P{t}_1\cdots t_n$, where equal argument values put the same tuple into or out of $P^{\mathfrak{A}}$. Hence $\{x=y,\alpha \}\models {\alpha }^{\prime }$, which is the group-6 schema.

Quantifier instantiation is the one hard group. The schema $\forall x\alpha \to {\alpha }_t^x$ 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 }_t^x$ is valid whenever $t$ is substitutable for $x$ in $\alpha$. The atomic-like special case $\forall xPx\to Pt$ is easy: from ${\models }_{\mathfrak{A}}\forall xPx[s]$ we get ${\models }_{\mathfrak{A}}Px[s(x\mid d)]$ for every $d$, and taking $d=s(t)$ lands on ${\models }_{\mathfrak{A}}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.

A substitution can be carried out either in the term $u$ or in the assignment$s$, with the same value.

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

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

Consequences

Soundness draws the containment $⊢\subseteq \models$: every deducible pair is a logical-implication pair. It is a one-way inclusion until completeness closes the loop.

Read the other way, soundness proves non-derivability: a single countermodel to $\Gamma \models \phi$ certifies $\Gamma ⊬\phi$.

Two equivalence corollaries and one reformulation follow.

The second half validates the alphabetic-variant maneuver semantically: renaming bound variables never changes truth. Both are pure applications of soundness. For the first, $⊢(\phi \leftrightarrow \psi )$ gives $\models (\phi \leftrightarrow \psi )$, i.e. $\phi$ and $\psi$ agree in every $\mathfrak{A},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 $\phi$ has both $\Gamma ⊢\phi$ and $\Gamma ⊢\neg \phi$, and satisfiable iff some $\mathfrak{A},s$ satisfies every member.

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 ⊢\phi$; then $\Gamma \cup \{\neg \phi \}$ is inconsistent (it proves $\phi$ and $\neg \phi$), hence unsatisfiable, which is exactly $\Gamma \models \phi$. 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. 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.³

• Adding a non-valid axiom breaks soundness. Suppose $\psi \in \Lambda$ with $\psi$ not valid. Then $⊢\psi$ (a one-line deduction) but $/\models \psi$, so $⊢⊈\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).