Deduction theorem

Under the term deduction theorem , two closely related theorems are known that are important in mathematical logic . A variant of the theorem, also known as the inference theorem, targets the notion of semantic inference . The other variant, which is used within calculi , makes the ( syntactic ) derivation the starting point instead of the ( semantic ) inference . In both cases a relationship to the material implication is established.

The deduction theorem for semantic inferences (⊨)

The semantic version of the deduction theorem is as follows:

A formula is a semantic consequence of the set of formulas with , formal , if and only if the implication ${\displaystyle B}$ ${\displaystyle T}$ ${\displaystyle T=\{A_{1},A_{2},...,A_{n}\}}$ ${\displaystyle T\models B}$

${\displaystyle A_{1}\land A_{2}\land ...\land A_{n}\rightarrow B}$

general , d. H. is a tautology (in classical logic this is the case if and only if the implication is true for every possible interpretation ).

In general, in classical logic, a formula is a semantic consequence of the set of formulas , i. H. , if for every interpretation for which all formulas of the formula set are true, the formula is also true. The inference theorem relates this general definition of semantic inference to implication. It thus forms one of the essential mechanisms for making the semantic concept of inference in computer systems manageable through purely formal manipulations (see derivation in computer science ). It is therefore closely related to the refutation theorem . ${\displaystyle B}$ ${\displaystyle T}$ ${\displaystyle T\models B}$ ${\displaystyle I}$ ${\displaystyle T}$ ${\displaystyle B}$

The deduction theorem for derivatives (⊢)

In the area of ​​calculi, another definition of the inference theorem is used, which moves purely on the syntactic level. This variant of the deduction theorem was found and proven as early as 1930 by Jacques Herbrand and (independently of him and almost simultaneously) by Alfred Tarski . In contrast to the semantic inference, the (syntactic) derivation is at the center of this definition . As in the deduction theorem described above, this is related to the implication:

If

${\displaystyle T,A\vdash B,}$

then

${\displaystyle T\vdash A\rightarrow B.}$

David Hilbert and Paul Bernays put it this way: "If a formula B can be derived from a formula A in such a way [...], then the formula A → B can be derived without using the formula A"

The reverse is also true in many calculi. That is, if the formula A → B can be derived from a set, so also the formula B with the aid of the additional hypothesis A. If the modus ponens applies in a calculus , this final direction is trivial.

Individual evidence

1. ^ David Hilbert, Paul Bernays: Fundamentals of Mathematics , Volume 2, Berlin: 1939, page 387.

See also

• Model theory
• Knowledge representation with logic
• Negation , for logic polarity see switching algebra
• Metascience

literature

• Franz von Kutschera , Alfred Breitkopf: Introduction to modern logic , 8th edition (2007), ISBN 978-3-495-482711 , pp. 72-75 (proof of the deduction theorem)