deduction-theorem
Last updated
Was this helpful?
Last updated
Was this helpful?
The deduction theorem states that a sentence of the form
π½ -> πΏis provable from a set of axiomsπiff the sentenceπ½is provable from the system whose axioms consist ofπΏand all the axioms ofπ.
The deduction theorem (DT) is a metatheorem of propositional and FOL
DT is a formalization of the proof technique in which an implication p -> q is proved by assuming p and then deriving q from this assumption, conjoined with other, previously established, theorems.
DT explains why proofs of conditional sentences in math are logically correct
Though it seemed "obvious" for centuries that proving q from p conjoined with a set of theorems is tantamount to proving the implication p -> q based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case.
The deduction theorem states that if a formula B is deducible from a set of assumptions π β {A}, where A is a closed formula, then the implication A -> B is deducible from π.
π, {A} |- Bimpliesπ |- A -> B
In case π is empty, DT shows that {A} |- B implies |- A -> B.