Deduction Theorem

In mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication AB is proved by assuming A and then deriving B from this assumption conjoined with known results. The deduction theorem explains why proofs of conditional sentences in mathematics are logically correct. Though it has seemed "obvious" to mathematicians literally for centuries that proving B from A conjoined with a set of theorems is sufficient to proving the implication AB based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case—another instance, perhaps, of modern logic "cleaning up" mathematical practice.

The deduction theorem states that if a formula B is deducible from a set of assumptions, where A is a closed formula, then the implication AB is deducible from In symbols, implies . In the special case where is the empty set, the deduction theorem shows that implies

The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However, there are first-order systems in which new inference rules are added for which the deduction theorem fails.

The deduction rule is an important property of Hilbert-style systems because the use of this metatheorem leads to much shorter proofs than would be possible without it. Although the deduction theorem could be taken as primitive rule of inference in such systems, this approach is not generally followed; instead, the deduction theorem is obtained as an admissible rule using the other logical axioms and modus ponens. In other formal proof systems, the deduction theorem is sometimes taken as a primitive rule of inference. For example, in natural deduction, the deduction theorem is recast as an introduction rule for "→".

Read more about Deduction TheoremExamples of Deduction, Virtual Rules of Inference, Conversion From Proof Using The Deduction Meta-theorem To Axiomatic Proof, The Deduction Theorem in Predicate Logic, Example of Conversion, Paraconsistent Deduction Theorem, The Resolution Theorem

Other articles related to "deduction theorem, theorems, theorem":

Heyting Algebra - Properties - Provable Identities
... In practice, one frequently uses the deduction theorem in such proofs ... It follows from the deduction theorem that is provable if and only if is provable from, that is, if is a provable consequence of.) In particular, if and ... of logic, then in practice it becomes necessary to prove as a lemma a version of the deduction theorem valid for Heyting algebras for any elements and of a Heyting algebra, we have ...
Deduction Theorem - The Resolution Theorem
... The resolution theorem is the converse of the deduction theorem ... It follows immediately from modus ponens which is the elimination rule for implication ...
Using Peirce's Law With The Deduction Theorem
... Peirce's law allows one to enhance the technique of using the deduction theorem to prove theorems ... wish to deduce Z so that we can use the deduction theorem to conclude that (P→Z)→(((P→Q)→Z)→Z) is a theorem ... Applying the deduction theorem, we get that (Z→Q)→Z follows from the original premises ...
Implicational Propositional Calculus - Completeness - Proof
... A proof of the completeness theorem is outlined below ... First, using the compactness theorem and the deduction theorem, we may reduce the completeness theorem to its special case with empty Γ, i.e ... (2) This follows from (1) by the deduction theorem ...

Famous quotes containing the word theorem:

    To insure the adoration of a theorem for any length of time, faith is not enough, a police force is needed as well.
    Albert Camus (1913–1960)