On the scope of the classical deduction theorem
Witold Pogorzelski · Journal of Symbolic Logic · 1968
§1. The set Cn(R, A + X) is the set of all expressions deducible, on the ground of formulas A, from the class X of formulas of the implicational propositional calculus, by means of rules belonging to the set R. In other words, Cn(R, A + X) is the set of expressions obtained from the set X by the help of a two-parameter function Cn[R, A]. The formula is called the classical deduction theorem. The classical deduction theorem is true for the system 〈R, A〉 (where R is the set of primitive rules, A is the set of axioms of the propositional calculus) if it holds for the function Cn[R, A].