In mathematical logic, the deduction theorem states that if a formula F is deducible from E then the implication E → F is demonstrable (i.e. it is "deducible" from the empty set). In symbols, if , then Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics. ...
The deduction theorem may be generalized to a countable sequence of assumption formulas such that from
, infer , and so on until
.
The deduction theorem is a meta-theorem: it is used to deduce proofs in a given theory though it is not a theorem of the theory itself.
See also
conditional proof, propositional calculus. Conditional proof is a proof that takes the form of asserting a conditional, and proving that the premise or antecedent of the conditional necessarily leads to the conclusion. ... The propositional calculus is a formal deduction system whose atomic formulas are propositional variables. ...
Reference
Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks is a comprehensive tutorial. See Section 1.5.
In mathematical logic, the deductiontheorem states that if a conclusion can be inferred (by means of some inference rule) from a premise, then it is possible to assert that the premise implies the conclusion.
The use of DT is a very useful aid to theorem proving (of logical theorems, that is).
But DT is a meta-theorem: it is used to deduce the existence of a proof in a given theory from an already existing proof in the given theory, but it does not belong to the theory itself.
Feeds |
Contact