The Deduction Theorem and Derived Rules

The calculus is complete as defined, but deducing anything directly from the six axiom schemas is laborious: the shortest known deduction of $\forall x\forall y(x=y\to y=x)$ from the axioms is seventeen formulas long. The remedy is a layer of metatheorems, each proved once in the meta-language, that license large deductive steps at will. Together they let a proof of deducibility read like ordinary mathematics while still guaranteeing that a genuine axiom-level deduction exists underneath.

Every metatheorem here is proved by the induction principle for theorems: exhibit a set $S$ containing $\Gamma \cup \Lambda$ and closed under modus ponens, and conclude $S$ holds of every theorem of $\Gamma$.

The generalization theorem

The informal move since $x$ was arbitrary, $\forall x\phi$ is sound only when nothing about $x$ was assumed. The formal condition is that $x$ is not free in any hypothesis.

The proof exposes what axiom groups 3 and 4 are for: group 4 handles the hypothesis case, group 3 the modus ponens case. The freeness restriction is not optional. Semantically $Px\models \forall xPx$ fails, so by soundness $Px⊬\forall xPx$; here $x$ is free in the hypothesis $Px$. The proof also does more than it states: it transforms a given deduction of $\phi$ effectively into a deduction of $\forall x\phi$.

A first consequence collapses any tautological step into one line.

The deduction theorem

The central metatheorem trades a hypothesis for an implication, matching the ordinary move assume $\gamma$; derive $\phi$; conclude $\gamma \to \phi$.

Here $\Gamma ;\gamma$ abbreviates $\Gamma \cup \{\gamma \}$. The converse direction is essentially modus ponens. For the forward direction there are two proofs.

The two proofs illustrate the two available styles: lean on sentential compactness, or grind out a syntactic transformation. The deduction theorem discharges an assumption, moving it from the left of the turnstile into the antecedent of an arrow.

Two corollaries fall out immediately. Call a set of formulas inconsistent iff some $\beta$ has both $\beta$ and $\neg \beta$ as theorems; then every formula is a theorem, since $\beta \to \neg \beta \to \alpha$ is a tautology.

The derived rules

The metatheorems above, plus generalization, are the rules used in practice. Each replaces a long axiom-level detour with a single justified step.

With these rules, proofs of deducibility can be written backward, reducing the goal by one rule at a time. Consider

The reduction runs top to bottom, each line justified by one metatheorem.

The final claim is easy: $\forall x\neg \phi ⊢\neg \phi$ and $\forall y\phi ⊢\phi$, both by axiom group 2 and modus ponens, and $\{\neg \phi ,\phi \}$ is inconsistent. Reading the table bottom to top reconstructs an axiom-level deduction.

There are also purely syntactic strategies keyed to the shape of the goal $\phi$.¹

• $\phi$ is $\psi \to \theta$: show $\Gamma ;\psi ⊢\theta$ (always possible).
• $\phi$ is $\forall x\psi$: if $x$ is not free in $\Gamma$, show $\Gamma ⊢\psi$; otherwise pass to a suitable alphabetic variant.
• $\phi$ is $\neg (\psi \to \theta )$: show $\Gamma ⊢\psi$ and $\Gamma ⊢\neg \theta$ (rule T).
• $\phi$ is $\neg \neg \psi$: show $\Gamma ⊢\psi$.
• $\phi$ is $\neg \forall x\psi$: use contraposition, or reductio; a bare instantiation $\Gamma ⊢\neg {\psi }_t^x$ need not exist for any $t$.

Generalization on constants

A constant symbol behaves like a free variable that happens not to occur in the hypotheses. That interchangeability upgrades a proof about a fresh constant into a universal statement.

Two refinements follow. When a specific variable is wanted in advance:

And the formal counterpart of there is such an $x$; call it $c$; from $c$ derive $\psi$:

Rule EI names an existential instance. It does not claim $\exists x\phi ⊢{\phi }_c^x$, which is usually false: the witness $c$ may be constrained, and nothing lets us prove a specific instance.

Alphabetic variants

Substitutability can fail for an unlucky choice of bound variables, and then a wff sits outside axiom group 2 for no deep reason. For instance $y$ is not substitutable for $x$ in $\forall yPxy$, so $\forall x\forall yPxy\to \forall yPyy$ is not directly an axiom. Renaming the inner bound variable avoids the clash without changing meaning.

The construction is a recursion on $\phi$: at each $\forall y$ whose variable clashes with $t$, pick a fresh $z$ occurring in neither ${\phi }^{\prime }$ nor $t$ nor $\{x\}$ and rename. The resulting ${\phi }^{\prime }$ is an alphabetic variant of $\phi$; it is provably equivalent in both directions and, by soundness, logically equivalent. Failure of substitutability is never a real obstacle: the right alphabetic variant removes it.

Equality reasoning

Axiom groups 5 and 6 are exactly enough to make $=$ behave. Collecting the facts needed for the completeness proof: the relation is an equivalence relation and is compatible with every predicate and function symbol.

• Eq1 (reflexive). $⊢\forall xx=x$. Axiom group 5.
• Eq2 (symmetric). $⊢\forall x\forall y(x=y\to y=x)$.
• Eq3 (transitive). $⊢\forall x\forall y\forall z(x=y\to y=z\to x=z)$.
• Eq4 (predicate compatibility). $⊢\forall x_1\cdots (x_1=y_1\to x_2=y_2\to P{x}_1{x}_2\to P{y}_1{y}_2)$, and similarly for $n$-place predicates.
• Eq5 (function compatibility). $⊢\forall x_1\cdots (x_1=y_1\to x_2=y_2\to f{x}_1{x}_2=f{y}_1{y}_2)$, and similarly for $n$-place functions.

Symmetry is worth writing out in Enderton's abbreviated proof style, where each line is a claim of deducibility with its justification, not a formula in a deduction.

Line 1 is a group-6 congruence axiom, taking $\alpha$ to be $x=x$ and replacing the first $x$ by $y$ to get ${\alpha }^{\prime }=y=x$. Rule T combines lines 1 and 2; generalization closes over $x$ and $y$, both absent from any hypothesis. These four lines are not a deduction; they are a meta-language proof that the seventeen-formula deduction of the symmetry sentence exists. The derived rules exist to avoid writing it out.

The congruence axioms carry into quantified formulas by the same abbreviated style, mixing all five derived moves.

For predicate compatibility (Eq4) the abbreviated proof reduces to showing $\{x_1=y_1,x_2=y_2,P{x}_1{x}_2\}⊢P{y}_1{y}_2$, obtained by two applications of modus ponens to the group-6 axioms $x_1=y_1\to P{x}_1{x}_2\to P{y}_1{x}_2$ and $x_2=y_2\to P{y}_1{x}_2\to P{y}_1{y}_2$. Function compatibility (Eq5) follows the same pattern with $f{x}_1{x}_2=f{x}_1{x}_2$ from reflexivity standing in for the predicate.