Theorem·T58
The deduction theorem
Adding a formula as an assumption and proving a consequence is, apart from a side condition on generalization, the same as proving the implication outright.
For a language
,
, and
: (i) if
, then
. (ii) if there is a proof
of
from
such that, for every
and every
with
for some
:
- then
.
In words
If a theory proves an implication, extending it by the antecedent proves the consequent - always, no side condition. Conversely, given a proof of the consequent from the extended theory in which no generalization step binds a variable free in the antecedent, the original theory already proves the implication.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1(i). By L68 (as ): . Also directly: the length- sequence is a proof of from ( ). By modus ponens: .
- 2(ii), setup. Let be the given proof, , , satisfying the side condition on every generalization step. We show, by strong induction on : .
- 3(ii), logical axiom or member of . If is a logical axiom, the length- sequence is a proof of from , so ; likewise if , the same length- sequence is a proof via the assumption clause of D104, so again . Either way, is an instance of schema A1 (taking the schema's , ), so proves it too; by modus ponens with : .
- 4(ii), . If is justified as a member of but , then . By L70: , i.e. .
- 5(ii), modus ponens. If is justified by modus ponens from ( , ): by the induction hypothesis (IH) at and : and . The formula is an instance of schema A2 (taking , , ), so proves it; two applications of modus ponens (first with the second IH fact, then with the first) give .
- 6(ii), generalization. If is justified by generalization from ( , for some ): by the side condition, . By the IH at : . By L71: . The formula is an instance of schema A9 (taking the schema's , , using for its side condition), so proves it; by modus ponens with the previous line: , i.e. .
- 7T08 concludes the claim for every ; in particular at : .
∎
Remarks
The side condition in (ii) is not bookkeeping - it is exactly what schema A9 needs to fire at each generalization step, and dropping it makes the theorem false: from
(the one-line proof
, an equality axiom) one could generalize to
, matching a "proof" of
from
for a DIFFERENT variable
never even mentioned - but
is not generally true. Whenever
is a sentence (
), the side condition holds automatically for every proof, with no restriction at all - the form this theorem takes in the Lindenbaum construction, which only ever extends by sentences.