---
title: A Deductive Calculus for First-Order Logic
module: The Deductive Calculus and Its Metatheorems
moduleNumber: 4
lessonNumber: 1
order: 401
summary: >
  A proof must be finite and mechanically checkable. A Hilbert-style calculus
  meets both demands: six schemas of logical axioms, a single rule of inference
  (modus ponens), and the syntactic consequence relation they generate.
  Substitution and substitutability are defined by recursion, and the bridge
  theorem reduces deducibility to tautological implication from the axioms.
topics: [The Deductive Calculus and Its Metatheorems]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.4 A Deductive Calculus (axioms and deductions)"
draft: false
---

The semantic account of first-order logic answers _what_ follows from a set of
hypotheses: $\Gamma \models \varphi$ holds when every structure satisfying all
of $\Gamma$ also satisfies $\varphi$. That definition quantifies over all
structures and all variable assignments, an uncountable search with no obvious
stopping point.[^sem] A proof settles the same question by finite, inspectable
means. The syntactic counterpart is a _deductive calculus_ whose proofs are
finite strings, checkable without insight.

Two constraints fix the design.[^design] A proof must be **finite**, because it
is an object handed from one person to another, and an infinite set of
hypotheses cannot be handed over whole. A proof must also be **effectively
checkable**: verifying that a purported proof contains no fallacy must be a
mechanical procedure, not a matter of flashes of insight. In particular, the set
of proofs from no hypotheses should be decidable, so that the provable-from-nothing
formulas can be effectively listed by generating all strings and sorting proofs
from non-proofs.

To keep the two levels apart we reserve the word **deduction** for the formal
object and leave "proof" for the ordinary mathematical arguments (in English)
that we make _about_ deductions. A deduction lives in the object language; our
reasoning about deductions lives in the meta-language.

$$
% caption: The two levels kept apart throughout: ordinary mathematical
% reasoning in the meta-language studies the formal calculus below it.
\begin{tikzpicture}[font=\footnotesize, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw, minimum width=72mm, minimum height=15mm, align=center]
  (meta) at (0,1.5) {meta-language\\ordinary mathematics: we prove theorems about deductions};
\node[draw, minimum width=72mm, minimum height=15mm, align=center]
  (obj) at (0,-1.5) {object language\\the deductive calculus: axioms, modus ponens, deductions};
\draw[->, thick] (meta.south) ++(-2.4,0) -- ++(0,-1.7) node[midway, left, black] {studies};
\draw[<-, thick] (meta.south) ++(2.4,0) -- ++(0,-1.7) node[midway, right, black] {is an object of study};
\end{tikzpicture}
$$

## Deductions from a rule of inference

Fix a first-order language. We will select an infinite set $\Lambda$ of formulas,
the **logical axioms**, and one **rule of inference**. For a set $\Gamma$ of
formulas, a formula counts as a theorem of $\Gamma$ if and only if it is
obtainable from $\Gamma \cup \Lambda$ by applying the rule finitely many times.

The single rule is **modus ponens**: from $\alpha$ and $\alpha \to \beta$, infer
$\beta$.

$$
\frac{\alpha, \qquad \alpha \to \beta}{\beta}
$$

The choice of $\Lambda$ and of the rules is far from unique; every deductive
calculus trades axioms against rules. Taking $\Lambda = \varnothing$ forces many
rules of inference; the opposite extreme, taken here, keeps a single rule and
pays for it with an infinite axiom set.

> **Definition (Deduction).** A **deduction** of $\varphi$ from $\Gamma$ is a
> finite sequence $\alpha_0, \dots, \alpha_n$ of formulas with $\alpha_n =
> \varphi$ such that for each $k \le n$, either
> $\alpha_k \in \Gamma \cup \Lambda$, or $\alpha_k$ is obtained by modus ponens
> from two earlier formulas $\alpha_i, \alpha_j$ (with $j < k$, $i < k$, and
> $\alpha_j = (\alpha_i \to \alpha_k)$). If such a deduction exists we write
> $\Gamma \vdash \varphi$ and say $\varphi$ is a **theorem** of $\Gamma$, or
> **deducible** from $\Gamma$.

Checking a purported deduction is the mechanical procedure the design demanded:
scan the sequence once, verifying each line locally.

```algorithm
caption: $\textsc{CheckDeduction}(\alpha_0, \dots, \alpha_n;\ \Gamma)$ — verify a purported deduction
for each $k \gets 0, 1, \dots, n$ do
  if $\alpha_k \in \Gamma \cup \Lambda$ then accept line $k$
  else if some $i, j < k$ have $\alpha_j = (\alpha_i \to \alpha_k)$ then accept line $k$
  else reject the sequence
accept the sequence as a deduction of $\alpha_n$
```

Line-by-line acceptance needs membership in $\Gamma \cup \Lambda$ to be
checkable; for $\Lambda$ that is arranged below by giving the axioms a purely
syntactic definition, and for hypotheses it holds whenever $\Gamma$ is decidable.

The word "theorem" now lives on two levels. Inside the object language,
$\alpha$ is a theorem of $\Gamma$ when $\Gamma \vdash \alpha$. In the
meta-language, statements about deductions (each proved in English) are also
called theorems; when the distinction matters we call the latter **metatheorems**.

A deduction is a construction sequence: it records how $\varphi$ is obtained from
the base set $\Gamma \cup \Lambda$ by applying modus ponens zero or more times.
This resembles building a wff from atoms, with two differences. Modus ponens is
_partial_ (its domain is only pairs of the form $\alpha, \alpha \to \beta$), and
it can produce a _shorter_ formula from longer ones. The deeper difference is that
the set of theorems is **not freely generated**: a theorem has many deductions, and its
construction tree is not unique.[^free] An induction principle still holds.

> **Theorem (Induction principle for theorems).** If $S$ is a set of wffs that
> includes $\Gamma \cup \Lambda$ and is **closed under modus ponens** (whenever
> $\alpha \in S$ and $(\alpha \to \beta) \in S$, also $\beta \in S$), then $S$
> contains every theorem of $\Gamma$.

Every metatheorem below that quantifies over all theorems of $\Gamma$ is proved
by exhibiting a set $S$ of the right shape and invoking this principle.

## Substitution

The logical axioms depend on substituting a term for a variable, so we pin that
operation down first. For a formula $\alpha$, a variable $x$, and a term $t$,
the expression $\alpha^x_t$ is the result of replacing $x$ by $t$ at every
_free_ occurrence of $x$ in $\alpha$. Officially this is a recursion on $\alpha$
(with an auxiliary recursion on terms for the atomic case).[^subst]

> **Definition (Substitution).** For a term $t$ and variable $x$:
> $$
> (\neg \alpha)^x_t = \neg(\alpha^x_t), \qquad
> (\alpha \to \beta)^x_t = (\alpha^x_t \to \beta^x_t),
> $$
> $$
> (\forall y\, \alpha)^x_t =
> \begin{cases}
> \forall y\, \alpha & \text{if } x = y,\\
> \forall y\, (\alpha^x_t) & \text{if } x \ne y,
> \end{cases}
> $$
> and for atomic $\alpha$, replace $x$ by $t$ throughout. The quantifier clause
> stops at $\forall x$ because occurrences of $x$ under it are bound, not free.

For example $\varphi^x_x = \varphi$, and $(Qx \to \forall x\, Px)^x_y = (Qy \to
\forall x\, Px)$: the $x$ inside $\forall x\, Px$ is bound and untouched.

> **Worked example.** Run the recursion on $(Qx \to \forall x\, Px)^x_y$ clause by
> clause. The conditional clause splits the substitution across the arrow:
> $$
> (Qx \to \forall x\, Px)^x_y = \bigl((Qx)^x_y \to (\forall x\, Px)^x_y\bigr).
> $$
> The left conjunct is atomic, so every free $x$ becomes $y$: $(Qx)^x_y = Qy$. The
> right conjunct hits the quantifier clause. Its bound letter is the substitution
> variable itself, so the clause returns the formula unchanged:
> $$
> (\forall x\, Px)^x_y = \forall x\, Px.
> $$
> Reassembling gives $(Qy \to \forall x\, Px)$. The occurrence of $x$ under
> $\forall x$ is bound, and substitution never reaches it.

Substitution alone is not always safe. Take $\alpha = \neg \forall y\; x = y$ and
substitute $y$ for $x$:

$$
\forall x\, \alpha \to \alpha^x_y \quad\text{ is }\quad
\forall x\, \neg \forall y\; x = y \;\to\; \neg \forall y\; y = y.
$$

The antecedent $\forall x\, \neg \forall y\; x = y$ is true in any structure whose
universe has two or more elements. The consequent $\neg \forall y\; y = y$ is
false in every structure, since $y = y$ holds always. So this instance of the
plausible-looking schema "if $\alpha$ holds of everything, it holds of $t$" is
nearly always false. The fault is **capture**: the substituted $y$ was seized by
the $\forall y$ quantifier already present.

$$
% caption: Variable capture. Substituting the term for the free variable sends
% it under a quantifier that binds the same letter, changing its meaning.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  cell/.style={draw, minimum width=30mm, minimum height=10mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\definecolor{red}{HTML}{B23A48}
\node[cell] (a) at (0,1.3) {free occurrence\\of the variable};
\node[cell] (b) at (0,-1.3) {term put in its place\\shares a bound letter};
\node[cell, draw=red, text=red, fill=red!7] (c) at (5.6,0) {captured:\\meaning changed};
\draw[->, acc, thick] (a.east) -- (c.north west);
\draw[->, red, thick] (b.east) -- (c.south west);
\node[align=center, black] at (2.7,-2.5) {a term is not substitutable when this happens};
\end{tikzpicture}
$$

To exclude capture we define when a term may be substituted at all.

> **Definition (Substitutable).** $t$ is **substitutable** for $x$ in $\alpha$
> by the recursion: for atomic $\alpha$, always; for $\neg\alpha$ and $\alpha \to
> \beta$, componentwise; and $t$ is substitutable for $x$ in $\forall y\, \alpha$
> iff either $x$ does not occur free in $\forall y\, \alpha$, **or** $y$ does not
> occur in $t$ and $t$ is substitutable for $x$ in $\alpha$.

Two easy cases: $x$ is always substitutable for itself, and any $t$ whose
variables all avoid $\alpha$ is substitutable for $x$ in $\alpha$. The word
choice is deliberate: even when $t$ is _not_ substitutable, $\alpha^x_t$ is still
formed by replacing every free $x$ with $t$. Substitutability is a licensing
condition on the axioms, not on the operation. It coincides with the "free for"
condition studied for the [substitution
lemma](/logic/first-order-languages/terms-substitution-and-parsing).

## The logical axioms

Before listing $\Lambda$ we widen each schema to its generalizations. A wff
$\varphi$ is a **generalization** of $\psi$ iff $\varphi = \forall x_1 \cdots
\forall x_n\, \psi$ for some $n \ge 0$ and variables $x_1, \dots, x_n$; the case
$n = 0$ makes every wff a generalization of itself. The logical axioms are all
generalizations of wffs of the following six forms, where $x, y$ are variables
and $\alpha, \beta$ are wffs.

| Group | Schema | Reads as |
| --- | --- | --- |
| 1 | tautologies | the sentential content |
| 2 | $\forall x\, \alpha \to \alpha^x_t$, with $t$ substitutable for $x$ in $\alpha$ | instantiation of a universal |
| 3 | $\forall x(\alpha \to \beta) \to (\forall x\, \alpha \to \forall x\, \beta)$ | $\forall$ distributes over $\to$ |
| 4 | $\alpha \to \forall x\, \alpha$, with $x$ not free in $\alpha$ | vacuous quantification |
| 5 | $x = x$ | reflexivity of equality |
| 6 | $x = y \to (\alpha \to \alpha')$, $\alpha$ atomic, $\alpha'$ replaces $x$ by $y$ at some places | equals substitute into atoms |

Groups 5 and 6 are included only when the language carries equality. The list is
not meant to look natural; each group is justified below. Group 2 encodes the
meaning of the quantifier; groups 3 and 4 exist precisely to make the
[generalization theorem](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
go through; groups 5 and 6 are exactly enough to prove the properties of equality.

$$
% caption: The six axiom schemas as one reference card, grouped by the fragment
% of the logic each governs: sentential, quantifier, and equality.
\begin{tikzpicture}[font=\footnotesize,
  grp/.style={draw, minimum width=34mm, minimum height=11mm, align=center},
  hd/.style={font=\footnotesize\bfseries}]
\definecolor{acc}{HTML}{4A6FA5}
\node[hd] at (0,2.0) {sentential};
\node[grp] (g1) at (0,1.0) {group 1\\tautologies};
\node[hd] at (5.0,2.0) {generality};
\node[grp] (g2) at (5.0,1.2) {group 2\\instantiation};
\node[grp] (g3) at (5.0,-0.1) {group 3\\distribution};
\node[grp] (g4) at (5.0,-1.4) {group 4\\vacuous binding};
\node[hd] at (10.0,2.0) {equality};
\node[grp] (g5) at (10.0,1.2) {group 5\\$x = x$ always};
\node[grp] (g6) at (10.0,-0.1) {group 6\\congruence for atoms};
\draw[thick] (1.8,0.5) -- (3.1,0.5);
\draw[thick] (6.8,0.5) -- (8.1,0.5);
\node[align=center, black] at (0,-1.1) {every generalization\\of a schema instance\\is also an axiom};
\end{tikzpicture}
$$

Deciding whether a formula is a group-2 axiom means matching it against $\forall
x\, \alpha \to \alpha^x_t$ and checking substitutability. Both halves have to hold.

> **Worked example.** Is $\forall v_3\bigl(\forall v_1(Av_1 \to \forall v_2\, Av_2)
> \to (Av_2 \to \forall v_2\, Av_2)\bigr)$ a group-2 axiom? Strip the leading
> generalization $\forall v_3$ and read the body as $\forall x\, \alpha \to
> \alpha^x_t$ with $x = v_1$, $\alpha = (Av_1 \to \forall v_2\, Av_2)$, $t = v_2$.
> Compute the substitution:
> $$
> \alpha^{v_1}_{v_2} = (Av_2 \to \forall v_2\, Av_2),
> $$
> since $Av_1$ becomes $Av_2$ and $\forall v_2\, Av_2$ is untouched ($v_2$ is
> bound). Substitutability holds: $v_2$ enters $Av_1$ freely, and $v_1$ is not free
> in $\forall v_2\, Av_2$. The body is $\forall v_1\, \alpha \to \alpha^{v_1}_{v_2}$
> and the whole is its $\forall v_3$-generalization, so it is in group 2.
>
> The near-miss $\forall v_1\, \forall v_2\, Bv_1 v_2 \to \forall v_2\, Bv_2 v_2$
> matches the shape with $\alpha = \forall v_2\, Bv_1 v_2$, $t = v_2$: indeed
> $\alpha^{v_1}_{v_2} = \forall v_2\, Bv_2 v_2$. But $v_2$ is _not_ substitutable
> for $v_1$ in $\forall v_2\, Bv_1 v_2$, because $v_1$ occurs free there and the
> incoming $v_2$ is captured by $\forall v_2$. The side condition fails, so this
> one is not an axiom.

### Tautologies as axioms

Group 1 needs spelling out, because "tautology" was defined for
[sentential logic](/logic/sentential-logic/truth-assignments-and-tautologies).
Split the wffs into **prime** formulas (atomic formulas and those of the form
$\forall x\, \alpha$) and **nonprime** formulas (the $\neg\alpha$ and $\alpha \to
\beta$). Every wff is built from prime formulas by the two operations for $\neg$
and $\to$. Now treat the prime formulas as sentence symbols. A wff is in axiom
group 1 iff, read this way, it is a tautology of sentential logic in the
connectives $\neg, \to$. No replacement is needed; the prime formulas already
_are_ first-order wffs.

$$
% caption: The prime / nonprime split behind group 1. Prime formulas become the
% sentence symbols; the two connectives rebuild every wff on top of them.
\begin{tikzpicture}[font=\footnotesize,
  box/.style={draw, minimum width=42mm, minimum height=10mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[box] (a) at (0,1.2) {atomic formula};
\node[box] (u) at (0,-0.2) {universal formula};
\node[box] (n) at (7.2,1.2) {negation};
\node[box] (c) at (7.2,-0.2) {conditional};
\node[black] at (0,2.2) {prime: the sentence symbols};
\node[black] at (7.2,2.2) {nonprime: connective-built};
\node[black, align=center] at (3.6,-1.5) {read a formula over its prime formulas, then run the sentential truth table};
\end{tikzpicture}
$$

For example, the contraposition tautology $(A \to \neg B) \to (B \to \neg A)$,
with $A = \forall y\, \neg Py$ and $B = Px$, yields the group-1 axiom

$$
(\forall y\, \neg Py \to \neg Px) \to (Px \to \neg \forall y\, \neg Py).
$$

Its truth table has four rows (two prime formulas), and every row comes out true.

> **Worked example.** Treat the prime formulas $A = \forall y\, \neg Py$ and $B =
> Px$ as sentence symbols and tabulate $(A \to \neg B) \to (B \to \neg A)$ over the
> four assignments.
>
> | $A$ | $B$ | $A \to \neg B$ | $B \to \neg A$ | $(A \to \neg B) \to (B \to \neg A)$ |
> | --- | --- | --- | --- | --- |
> | T | T | F | F | T |
> | T | F | T | T | T |
> | F | T | T | T | T |
> | F | F | T | T | T |
>
> The final column is constant $T$, so the wff is a tautology of sentential logic
> in $\neg, \to$, hence a group-1 axiom. The row $A = B = T$ is the only one where
> both branches are false, and a conditional with a false antecedent is true, so
> the whole comes out $T$ there as well.

By contrast $\forall x(Px \to Px)$ and $\forall x\, Px \to Px$ are _not_
tautologies: their quantified prime formulas can independently take either truth
value, even though both are in fact valid for quantifier-level reasons.

Taking all tautologies as axioms is more than needed. The tautologies form a
decidable set (which matters for the enumerability theorem in
[soundness and completeness](/logic/deductive-calculus/completeness-and-consistency)),
but there is no known fast decision procedure for them. One could instead take a
polynomial-time-decidable subset of tautologies as axioms and derive the rest by
modus ponens.

## Deducibility as tautological implication

First-order formulas are now also sentential wffs (over the prime formulas), so
sentential concepts apply to them. If $\Sigma$ **tautologically implies**
$\varphi$ then $\Sigma$ **logically implies** $\varphi$, but not conversely:
$\forall x\, Px$ logically implies $Pc$, yet does not tautologically imply it,
because $\forall x\, Px$ and $Pc$ are distinct prime formulas.[^taut]

The following metatheorem reduces the whole deductive calculus to sentential
tautological implication from $\Gamma \cup \Lambda$.

> **Theorem (Deducibility equals tautological implication).** $\Gamma \vdash \varphi$ if and only if $\Gamma
> \cup \Lambda$ tautologically implies $\varphi$.

> **Proof.** ($\Rightarrow$) The set $\{\alpha, \alpha \to \beta\}$ tautologically
> implies $\beta$. Suppose a truth assignment $v$ satisfies every member of $\Gamma
> \cup \Lambda$. By the induction principle, the set of formulas $v$ satisfies
> includes $\Gamma \cup \Lambda$ and is closed under modus ponens, so it contains
> every theorem of $\Gamma$. Hence $v$ satisfies $\varphi$.
>
> ($\Leftarrow$) Suppose $\Gamma \cup \Lambda$ tautologically implies $\varphi$. By
> the sentential
> [compactness theorem](/logic/sentential-logic/compactness-and-effectiveness),
> a finite subset $\{\gamma_1, \dots, \gamma_m, \lambda_1, \dots, \lambda_n\}$
> already tautologically implies $\varphi$. Then
>
> $$
> \gamma_1 \to \cdots \to \gamma_m \to \lambda_1 \to \cdots \to \lambda_n \to \varphi
> $$
>
> is a tautology, hence a group-1 axiom, hence in $\Lambda$. Applying modus ponens
> $m + n$ times to it and to $\{\gamma_1, \dots, \gamma_m, \lambda_1, \dots,
> \lambda_n\}$ yields $\varphi$. $\blacksquare$

The proof uses sentential compactness for a possibly uncountable language, since
we never assumed the first-order language has only countably many symbols.

## A worked deduction

Consider deducing, from no hypotheses, that a property holds of $x$ implies it
holds of some element:

$$
\vdash\; Px \to \exists y\, Py.
$$

The existential is an abbreviation: $\exists y\, Py$ is $\neg \forall y\, \neg
Py$. The deduction has three lines.

| # | Formula | Justification |
| --- | --- | --- |
| 1 | $\forall y\, \neg Py \to \neg Px$ | axiom group 2: instance of $\forall y\, \alpha \to \alpha^y_x$ with $\alpha = \neg Py$ |
| 2 | $(\forall y\, \neg Py \to \neg Px) \to (Px \to \neg \forall y\, \neg Py)$ | axiom group 1: contraposition tautology |
| 3 | $Px \to \neg \forall y\, \neg Py$, i.e. $Px \to \exists y\, Py$ | modus ponens, lines 1 and 2 |

Line 1 is a group-2 instantiation: substituting the term $x$ for the quantified
$y$ in $\neg Py$ gives $\neg Px$, and $x$ is substitutable for $y$ there. Line 2
is a tautology by the truth table above. One application of modus ponens closes
the deduction. The same three formulas, drawn as a **pedigree tree**, show modus
ponens as a single node with the two axioms as inputs.

$$
% caption: The same deduction as a pedigree tree; the two axioms feed one modus
% ponens node whose output is the theorem. Squashing the tree gives the linear
% deduction above.
\begin{tikzpicture}[font=\footnotesize, >=stealth,
  ax/.style={draw, minimum width=26mm, minimum height=10mm, align=center},
  concl/.style={draw=acc, thick, minimum width=30mm, minimum height=10mm, align=center, fill=acc!12}]
\definecolor{acc}{HTML}{4A6FA5}
\node[ax] (a1) at (-3.2,1.6) {line 1\\group 2};
\node[ax] (a2) at (3.2,1.6) {line 2\\group 1};
\node[concl] (mp) at (0,-1.0) {line 3\\modus ponens};
\draw[->, thick] (a1.south) -- (mp.north west);
\draw[->, thick] (a2.south) -- (mp.north east);
\node[black] at (0,1.7) {the two premises};
\end{tikzpicture}
$$

Generalizing to $\vdash \forall x(Px \to \exists y\, Py)$ prepends quantifiers,
licensed by the [generalization
theorem](/logic/deductive-calculus/deduction-theorem-and-derived-rules). The
[derived rules](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
replace these hand-drawn trees with reusable moves.

## The choice of a syntactic axiom set

It might seem cleaner to take the set of all _valid_ formulas as $\Lambda$. Two
objections rule it out.[^why] First, validity is a **semantic** notion, defined
by quantifying over structures and truth. To prove that the validities are
effectively enumerable we need $\Lambda$ to have a **finitary, syntactic**
definition, one that inspects only the arrangement of symbols. Second, we want
$\Lambda$ to be **decidable**, and the set of validities is not decidable
(Church's theorem, reached in the
[incompleteness](/logic/incompleteness/incompleteness-and-undecidability) chapter).
The six schemas meet both demands: membership in $\Lambda$ is a mechanical syntax
check, run group by group.

The design succeeds only if the syntactic relation $\vdash$ matches the semantic
relation $\models$. That two-way match is the content of the
[soundness](/logic/deductive-calculus/soundness) and
[completeness](/logic/deductive-calculus/completeness-and-consistency) theorems.
The [metatheorems](/logic/deductive-calculus/deduction-theorem-and-derived-rules)
(deduction theorem, generalization, the derived rules) make the calculus usable
by hand.

[^sem]: Enderton, §2.2. Logical implication $\Gamma \models \varphi$ is truth in all models under all assignments; the deductive calculus of §2.4 is its finitary syntactic counterpart.
[^design]: Enderton, §2.4, opening remarks on what constitutes a proof: finiteness and effective checkability, with the promised compactness and enumerability theorems (proved in §2.5) as the necessary and sufficient conditions for finite proofs of logical implication to exist.
[^free]: Enderton, §2.4; contrast with the free generation of wffs in §1.4 and §2.3. A theorem never has a unique deduction, so its construction tree is not unique, unlike a formula's formation tree.
[^subst]: Enderton, §2.4, "Substitution"; the atomic case is elaborated as Exercise 1 of that section.
[^taut]: Enderton, §2.4, third remark on tautologies, and Exercise 3: a truth assignment on prime formulas extends to all wffs exactly as in Chapter 1, so tautological implication entails logical implication. Theorem 24B then reduces deducibility from $\Gamma$ to tautological implication from $\Gamma \cup \Lambda$.
[^why]: Enderton, §2.4, "Final Comments"; the meta-language / object-language separation is Enderton's Figure 8.