Deduction Theorem

Abstract

This most important metalogical theorem asserts that to prove an implication it is sufficient to derive the consequent of this implication from its antecedents. As it is known today, the statement of this theorem as a postulate of deductive inference can be found in Bolzano (1837). The development of mathematical logic in the 19th century was not sufficient for Bolzano’s discovery to be appreciated and it was rediscovered in the 1920s by Alfred Tarski and, independently, by Jacques Herbrand, but published not earlier than 1930. The term deduction theorem is due to David Hilbert (Hilbert and Bernays 34–39). There is a series of publications concerning the deduction theorem, the conditions it satisfies, its generalizations, and its modifications valid in certain nonclassical logical systems.