---
title: The Deduction Theorem and Derived Rules
module: The Deductive Calculus and Its Metatheorems
moduleNumber: 4
lessonNumber: 2
order: 402
summary: >
  Raw deductions from axioms are unusable by hand. The generalization theorem,
  the deduction theorem, contraposition, reductio ad absurdum, and rule T reduce
  the calculus to the moves of ordinary mathematics, each proved once to license
  a block of axiom-level steps. Generalization on constants and alphabetic
  variants handle the quantifier and substitution bookkeeping.
topics: [The Deductive Calculus and Its Metatheorems]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.4 A Deductive Calculus (metatheorems and derived rules)"
draft: false
---

The [calculus](/logic/deductive-calculus/a-deductive-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\, \varphi$" is sound only
when nothing about $x$ was assumed. The formal condition is that $x$ is not free
in any hypothesis.

> **Theorem (Generalization).** If $\Gamma \vdash \varphi$ and $x$ does not occur
> free in any formula of $\Gamma$, then $\Gamma \vdash \forall x\, \varphi$.

> **Proof.** Fix $\Gamma$ and a variable $x$ not free in $\Gamma$. Let $S = \{\varphi
> : \Gamma \vdash \forall x\, \varphi\}$. By the induction principle it suffices
> that $S \supseteq \Gamma \cup \Lambda$ and $S$ is closed under modus ponens.
>
> - **$\varphi$ a logical axiom.** Then $\forall x\, \varphi$ is also a logical
>   axiom (a generalization of an axiom is an axiom), so $\Gamma \vdash \forall x\,
>   \varphi$.
> - **$\varphi \in \Gamma$.** Then $x$ is not free in $\varphi$, so $\varphi \to
>   \forall x\, \varphi$ is in axiom group 4; with $\varphi$ and modus ponens,
>   $\Gamma \vdash \forall x\, \varphi$.
> - **$\varphi$ from modus ponens on $\psi$ and $\psi \to \varphi$.** By the
>   inductive hypothesis $\Gamma \vdash \forall x\, \psi$ and $\Gamma \vdash \forall
>   x(\psi \to \varphi)$. Axiom group 3, $\forall x(\psi \to \varphi) \to (\forall
>   x\, \psi \to \forall x\, \varphi)$, plus two applications of modus ponens gives
>   $\Gamma \vdash \forall x\, \varphi$. $\blacksquare$

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 x\, Px$ fails, so by
[soundness](/logic/deductive-calculus/soundness) $Px \nvdash \forall x\, Px$;
here $x$ is free in the hypothesis $Px$. The proof also does more than it states:
it transforms a given deduction of $\varphi$ effectively into a deduction of
$\forall x\, \varphi$.

A first consequence collapses any tautological step into one line.

> **Lemma (Rule T).** If $\Gamma \vdash \alpha_1, \dots, \Gamma \vdash \alpha_n$
> and $\{\alpha_1, \dots, \alpha_n\}$ tautologically implies $\beta$, then
> $\Gamma \vdash \beta$.

> **Proof.** $\alpha_1 \to \cdots \to \alpha_n \to \beta$ is a tautology, hence a
> group-1 axiom; apply modus ponens $n$ times. $\blacksquare$

## The deduction theorem

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

> **Theorem (Deduction theorem).** $\Gamma; \gamma \vdash \varphi$ if and only if
> $\Gamma \vdash (\gamma \to \varphi)$.

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

> **Proof (via tautological implication).** Through
> [the tautological-implication characterization of deducibility](/logic/deductive-calculus/a-deductive-calculus):
>
> $$
> \Gamma; \gamma \vdash \varphi
> \;\iff\; (\Gamma; \gamma) \cup \Lambda \text{ taut. implies } \varphi
> \;\iff\; \Gamma \cup \Lambda \text{ taut. implies } (\gamma \to \varphi)
> \;\iff\; \Gamma \vdash (\gamma \to \varphi). \qquad \blacksquare
> $$

> **Proof (by induction on deductions).** Directly, without sentential
> compactness, by induction on the theorems of $\Gamma; \gamma$; this shows how
> to transform a deduction of $\varphi$ from $\Gamma; \gamma$ into a deduction
> of $\gamma \to \varphi$ from $\Gamma$.
>
> - **$\varphi = \gamma$.** Then $\vdash (\gamma \to \varphi)$, a tautology.
> - **$\varphi$ a logical axiom or in $\Gamma$.** Then $\Gamma \vdash \varphi$, and
>   $\varphi$ tautologically implies $\gamma \to \varphi$, so rule T gives $\Gamma
>   \vdash (\gamma \to \varphi)$.
> - **$\varphi$ from modus ponens on $\psi$ and $\psi \to \varphi$.** By the
>   inductive hypothesis $\Gamma \vdash (\gamma \to \psi)$ and $\Gamma \vdash (\gamma
>   \to (\psi \to \varphi))$; the set $\{\gamma \to \psi, \gamma \to (\psi \to
>   \varphi)\}$ tautologically implies $\gamma \to \varphi$, so rule T applies. $\blacksquare$

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.

$$
% caption: The deduction theorem as discharge: an active assumption on the left
% of the turnstile is absorbed into the antecedent of an implication on the right.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=52mm, minimum height=13mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (l) at (0,1.4) {hypotheses plus one assumption\\prove the conclusion};
\node[box] (r) at (0,-1.4) {hypotheses alone\\prove: assumption implies conclusion};
\draw[->, acc, very thick] (l.south) -- (r.north) node[midway, right, black] {discharge};
\node[align=center, black] at (-4.5,0) {the assumption\\becomes an\\antecedent};
\end{tikzpicture}
$$

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.

> **Corollary (Contraposition).** $\Gamma; \varphi \vdash \neg\psi$ if and only
> if $\Gamma; \psi \vdash \neg\varphi$.

> **Proof.** $\Gamma; \varphi \vdash \neg\psi$ gives $\Gamma \vdash \varphi \to
> \neg\psi$ (deduction theorem), hence $\Gamma \vdash \psi \to \neg\varphi$
> (rule T, since $\varphi \to \neg\psi$ tautologically implies $\psi \to
> \neg\varphi$), hence $\Gamma; \psi \vdash \neg\varphi$ (modus ponens). Symmetry
> gives the converse. $\blacksquare$

> **Corollary (Reductio ad absurdum).** If $\Gamma; \varphi$ is inconsistent,
> then $\Gamma \vdash \neg\varphi$.

> **Proof.** Inconsistency gives some $\beta$ with $\Gamma; \varphi \vdash \beta$
> and $\Gamma; \varphi \vdash \neg\beta$; the deduction theorem yields $\Gamma
> \vdash \varphi \to \beta$ and $\Gamma \vdash \varphi \to \neg\beta$, and $\{\varphi
> \to \beta, \varphi \to \neg\beta\}$ tautologically implies $\neg\varphi$. $\blacksquare$

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

$$
% caption: The derived rules used to write proofs of deducibility, each standing
% in for a block of axiom-level modus ponens steps.
\begin{tikzpicture}[font=\footnotesize,
  tool/.style={draw, minimum width=40mm, minimum height=12mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[tool] (t)   at (0,1.5)   {rule T\\tautological consequence in one step};
\node[tool] (ded) at (0,0)     {deduction theorem\\assume the antecedent};
\node[tool] (gen) at (0,-1.5)  {generalization\\close over a fresh variable};
\node[tool] (con) at (5.2,1.5) {contraposition\\swap and negate the two sides};
\node[tool] (raa) at (5.2,0)   {reductio\\derive a contradiction};
\node[tool] (ei)  at (5.2,-1.5){rule EI\\name a witness, then reason};
\end{tikzpicture}
$$

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

$$
\vdash\; \exists x\, \forall y\, \varphi \to \forall y\, \exists x\, \varphi.
$$

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

| Reduce to showing | by |
| --- | --- |
| $\exists x\, \forall y\, \varphi \vdash \forall y\, \exists x\, \varphi$ | deduction theorem |
| $\exists x\, \forall y\, \varphi \vdash \exists x\, \varphi$ | generalization ($y$ not free on the left) |
| $\neg \forall x\, \neg \forall y\, \varphi \vdash \neg \forall x\, \neg\varphi$ | rewriting $\exists$ as $\neg\forall\neg$ |
| $\forall x\, \neg\varphi \vdash \forall x\, \neg \forall y\, \varphi$ | contraposition and rule T |
| $\forall x\, \neg\varphi \vdash \neg \forall y\, \varphi$ | generalization |
| $\{\forall x\, \neg\varphi,\ \forall y\, \varphi\}$ is inconsistent | reductio ad absurdum |

$$
% caption: Working a goal backward: each derived rule peels one connective off the
% target until the remaining claim is a plain inconsistency.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  stp/.style={draw, minimum width=66mm, minimum height=8mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[stp] (s1) at (0,3.0)  {prove the implication};
\node[stp] (s2) at (0,2.0)  {discharge the antecedent};
\node[stp] (s3) at (0,1.0)  {generalize over a fresh variable};
\node[stp] (s4) at (0,0.0)  {rewrite the existential, apply contraposition};
\node[stp] (s5) at (0,-1.0) {generalize again};
\node[stp, draw=acc, thick, fill=acc!12] (s6) at (0,-2.0) {reduce to an inconsistency};
\draw[->, thick] (s1) -- (s2);
\draw[->, thick] (s2) -- (s3);
\draw[->, thick] (s3) -- (s4);
\draw[->, thick] (s4) -- (s5);
\draw[->, thick] (s5) -- (s6);
\node[black, align=left, anchor=west] at (3.9,0.5) {every arrow is\\one derived rule};
\end{tikzpicture}
$$

The final claim is easy: $\forall x\, \neg\varphi \vdash \neg\varphi$ and
$\forall y\, \varphi \vdash \varphi$, both by axiom group 2 and modus ponens, and
$\{\neg\varphi, \varphi\}$ 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
$\varphi$.[^strategy]

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

> **Worked example.** Suppose $x$ is not free in $\alpha$. Deduce
> $$
> \vdash (\alpha \to \forall x\, \beta) \leftrightarrow \forall x(\alpha \to \beta).
> $$
> Rule T splits the biconditional into its two conditionals. For the forward one,
> $\vdash (\alpha \to \forall x\, \beta) \to \forall x(\alpha \to \beta)$, the
> deduction theorem discharges $\alpha \to \forall x\, \beta$, and generalization
> (legitimate: $x$ is free in neither $\alpha$ nor $\forall x\, \beta$) then a
> second discharge reduce the goal to
> $$
> \{\alpha \to \forall x\, \beta,\ \alpha\} \vdash \beta.
> $$
> Modus ponens gives $\forall x\, \beta$, axiom group 2 gives $\forall x\, \beta
> \to \beta$, and one more modus ponens gives $\beta$. For the converse,
> $\vdash \forall x(\alpha \to \beta) \to (\alpha \to \forall x\, \beta)$, the same
> two reductions leave $\{\forall x(\alpha \to \beta),\ \alpha\} \vdash \beta$:
> instantiate $\forall x(\alpha \to \beta)$ to $\alpha \to \beta$ by group 2, then
> modus ponens with $\alpha$.

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

> **Theorem (Generalization on constants).** If $\Gamma \vdash \varphi$ and $c$
> is a constant symbol not occurring in $\Gamma$, then there is a variable $y$
> (not in $\varphi$) with $\Gamma \vdash \forall y\, \varphi^c_y$, and a deduction
> of it in which $c$ does not occur.

> **Proof.** Let $\alpha_0, \dots, \alpha_n$ be a deduction of $\varphi$ from
> $\Gamma$, and let $y$ be the first variable in none of the $\alpha_i$. Replacing
> $c$ by $y$ throughout, $(\alpha_0)^c_y, \dots, (\alpha_n)^c_y$ is again a
> deduction: hypotheses are unchanged (they lack $c$), logical axioms map to
> logical axioms, and modus ponens is preserved. So $\Gamma \vdash \varphi^c_y$ from
> the finite $\Gamma_0 \subseteq \Gamma$ used, with $y$ not free in $\Gamma_0$;
> generalization gives $\Gamma \vdash \forall y\, \varphi^c_y$. $\blacksquare$

$$
% caption: Generalization on constants. A constant that never appears in the
% hypotheses is truly arbitrary, so a proof about it lifts to a universal claim.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=46mm, minimum height=13mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (l) at (0,0) {proof about a fresh constant\\the constant is not in the hypotheses};
\node[box] (r) at (9.0,0) {universal statement\\the constant becomes a bound variable};
\draw[->, acc, very thick] (l.east) -- (r.west) node[midway, above, black] {generalize} node[midway, below, black] {rename};
\end{tikzpicture}
$$

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

> **Corollary.** If $\Gamma \vdash \varphi^x_c$ where $c$ occurs in neither
> $\Gamma$ nor $\varphi$, then $\Gamma \vdash \forall x\, \varphi$, by a deduction
> in which $c$ does not occur.

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

> **Corollary (Rule EI).** If $c$ occurs in none of $\varphi, \psi, \Gamma$ and
> $\Gamma; \varphi^x_c \vdash \psi$, then $\Gamma; \exists x\, \varphi \vdash
> \psi$, by a deduction without $c$.

> **Proof.** Contraposition gives $\Gamma; \neg\psi \vdash \neg \varphi^x_c$; the
> previous corollary gives $\Gamma; \neg\psi \vdash \forall x\, \neg\varphi$;
> contraposition again yields the result. $\blacksquare$

Rule EI names an **e**xistential **i**nstance. It does not claim $\exists x\,
\varphi \vdash \varphi^x_c$, which is usually false: the witness $c$ may be
constrained, and nothing lets us prove a specific instance.

> **Worked example.** From $\Gamma = \{\forall x(Px \to Qx),\ \forall z\, Pz\}$
> derive $\forall x\, Qx$, routing through a fresh constant.
> - Pick a constant $c$ not in $\Gamma$. Axiom group 2 instantiates $\forall x(Px
>   \to Qx)$ to $Pc \to Qc$ and $\forall z\, Pz$ to $Pc$; two applications of modus
>   ponens give $\Gamma \vdash Qc$.
> - That deduction uses no property of $c$, so replacing $c$ by a variable $y$
>   throughout gives $\Gamma \vdash Qy$ — a constant absent from $\Gamma$ is
>   interchangeable with a free variable.
> - Since $c$ does not occur in $\Gamma$, generalization on constants supplies a
>   variable with $\Gamma \vdash \forall y\, Qy$, and $\forall y\, Qy \vdash \forall
>   x\, Qx$ closes it.
>
> The detour through $c$ is what generalization on constants formalizes: reasoning
> about an arbitrary named object and then quantifying the name away.

## 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 y\, Pxy$, so $\forall x\, \forall y\, Pxy \to
\forall y\, Pyy$ is not directly an axiom. Renaming the inner bound variable
avoids the clash without changing meaning.

> **Theorem (Existence of alphabetic variants).** Given a formula $\varphi$, a
> term $t$, and a variable $x$, there is a formula $\varphi'$ differing from
> $\varphi$ only in its choice of bound variables such that $\varphi \vdash
> \varphi'$ and $\varphi' \vdash \varphi$, and $t$ is substitutable for $x$ in
> $\varphi'$.

The construction is a recursion on $\varphi$: at each $\forall y$ whose variable
clashes with $t$, pick a fresh $z$ occurring in neither $\varphi'$ nor $t$ nor
$\{x\}$ and rename. The resulting $\varphi'$ is an **alphabetic variant** of
$\varphi$; it is provably equivalent in both directions and, by
[soundness](/logic/deductive-calculus/soundness), logically equivalent. Failure
of substitutability is never a real obstacle: the right alphabetic variant
removes it.

$$
% caption: An alphabetic variant renames a bound variable that would otherwise
% capture the incoming term; the two formulas prove each other.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  box/.style={draw, minimum width=40mm, minimum height=12mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\definecolor{red}{HTML}{B23A48}
\node[box, draw=red, text=red, fill=red!7] (bad) at (0,0) {bound letter clashes\\with the term to insert};
\node[box] (good) at (6.4,0) {bound letter renamed\\term now slots in};
\draw[->, acc, very thick] (bad.east) -- (good.west) node[midway, above, black] {rename};
\draw[<->, thick] (0,-0.75) .. controls (3.2,-1.7) .. (6.4,-0.75);
\node[black] at (3.2,-1.65) {each proves the other};
\end{tikzpicture}
$$

## Equality reasoning

Axiom groups 5 and 6 are exactly enough to make $=$ behave. Collecting the facts
needed for the [completeness
proof](/logic/deductive-calculus/completeness-and-consistency): the relation is an
equivalence relation and is compatible with every predicate and function symbol.

- **Eq1 (reflexive).** $\vdash \forall x\; x = x$. Axiom group 5.
- **Eq2 (symmetric).** $\vdash \forall x\, \forall y(x = y \to y = x)$.
- **Eq3 (transitive).** $\vdash \forall x\, \forall y\, \forall z(x = y \to y = z
  \to x = z)$.
- **Eq4 (predicate compatibility).** $\vdash \forall x_1 \cdots (x_1 = y_1 \to
  x_2 = y_2 \to Px_1 x_2 \to Py_1 y_2)$, and similarly for $n$-place predicates.
- **Eq5 (function compatibility).** $\vdash \forall x_1 \cdots (x_1 = y_1 \to x_2
  = y_2 \to fx_1 x_2 = fy_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.

| # | Claim | Justification |
| --- | --- | --- |
| 1 | $\vdash x = y \to x = x \to y = x$ | axiom group 6 |
| 2 | $\vdash x = x$ | axiom group 5 |
| 3 | $\vdash x = y \to y = x$ | lines 1, 2; rule T |
| 4 | $\vdash \forall x\, \forall y(x = y \to y = x)$ | line 3; generalization twice |

Line 1 is a group-6 congruence axiom, taking $\alpha$ to be $x = x$ and replacing
the first $x$ by $y$ to get $\alpha' = 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.

> **Worked example.** Deduce $\vdash x = y \to \forall z\, Pxz \to \forall z\,
> Pyz$, so that equal elements agree on $\forall z\, P{\cdot}z$.
>
> | # | Claim | Justification |
> | --- | --- | --- |
> | 1 | $\vdash x = y \to Pxz \to Pyz$ | axiom group 6 |
> | 2 | $\vdash \forall z\, Pxz \to Pxz$ | axiom group 2 |
> | 3 | $\vdash x = y \to \forall z\, Pxz \to Pyz$ | lines 1, 2; rule T |
> | 4 | $\{x = y,\ \forall z\, Pxz\} \vdash Pyz$ | line 3; modus ponens twice |
> | 5 | $\{x = y,\ \forall z\, Pxz\} \vdash \forall z\, Pyz$ | line 4; generalization |
> | 6 | $\vdash x = y \to \forall z\, Pxz \to \forall z\, Pyz$ | line 5; deduction theorem twice |
>
> Line 3 combines the group-6 congruence with the group-2 instantiation: from
> $x = y \to (Pxz \to Pyz)$ and $\forall z\, Pxz \to Pxz$, rule T yields $x = y \to
> (\forall z\, Pxz \to Pyz)$. Generalization at line 5 is legitimate because $z$ is
> free in neither hypothesis; two discharges recover the arrow form.

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

[^strategy]: Enderton, §2.4, "Strategy"; the case $\neg\forall x\,\psi$ has instances where $\Gamma \vdash \neg\forall x\,\psi$ yet $\Gamma \nvdash \neg\psi^x_t$ for every term $t$, e.g. $\Gamma = \varnothing$, $\psi = \neg(Px \to \forall y\,Py)$.