Deduction theorem
Deduction theorem
In a logistic system (q. v.) containing propositional calculus (pure or applied) or a suitable part of the propositional calculus, it is often desirable to have the property that if the inference from A to B is a valid inference then A ? B is a theorem, or, more generally, that if the inference from A1, A2, . . . , An ? B is valid then the inference from A1, A2, . . . , An ? B is valid. The syntactical theorem, asserting of a given logistic system that it has this property, is called the deduction theorem for that system. (Certain cautions are necessary in defining the notion of valid inference where free variables are present; cf. Logic, formal, 1, 3.) — A.C.