Lemma·L71
Generalization as a derived rule on provability
If a theory proves a formula, it proves the universal quantification of that formula over any variable - just append one more step to the witnessing proof.
For a language
,
,
, and
: if
, then
In words
For any formula and any variable: if a theory proves the formula, it proves its universal quantification too - append one more generalization step to the witnessing proof.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1Let be a proof of from , of length . Let , of length .
- 2For : (T29), justified exactly as within , unaffected by the one entry appended after position .
- 3For : (T29). This is justified by generalization from , at index , matching D104's generalization clause exactly (generalization is unrestricted, so no side condition on is needed here).
- 4So is a proof of from : .
∎
Remarks
The companion derived rule to modus ponens on provability, for the other inference rule of D104. Together the two let proofs be manipulated at the level of provability statements (
) rather than by hand-building sequence-of-formulas witnesses every time - used repeatedly in the deduction theorem's generalization case.