|Berka I 112
Definition "Deduction Theorem"/Hilbert: if a formula B can be derived from a formula A in such a way that every free variable occurring in A is fixed. i.e. that it is neither used for an insertion, done for it, nor as a designated variable of a shemata (α), (β), then the formula A > B can be derived without using the formula A. ((s) elimination of the premise).
I 116 Note:
Rule of the back Generalization/Scheme (α)/Hilbert:
A > B(a)
A > (x) B(x)
Rule of the front particularisation/Scheme (β)/Hilbert:
B(a) > A
(Ex)B(x) > A ._____________Explanation of symbols: Roman numerals indicate the source, arabic numerals indicate the page number. The corresponding books are indicated on the right hand side. ((s)…): Comment by the sender of the contribution.
K. Berka/L. Kreiser
Logik Texte Berlin 1983