Concept
Deduction theorem
Overview
In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication
A
→
B
{\displaystyle A\to B}
, it is sufficient to assume
A
{\displaystyle A}
as a hypothesis and then proceed to derive
B
{\displaystyle B}
. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.
In more detail, the propositional logic deduction theorem states that if a formula
B
{\displaystyle B}
is deducible from a set of assumptions
Δ
∪
{
A
}
{\displaystyle \Delta \cup \{A\}}
then the implication
A
→
B
{\displaystyle A\to B}
is deducible from
Δ
{\displaystyle \Delta }
; in symbols,
Δ
∪
{
A
}
⊢
B
{\displaystyle \Delta \cup \{A\}\vdash B}
implies
Δ
⊢
A
→
B
{\displaystyle \Delta \vdash A\to B}
. In the special case where
Δ
{\displaystyle \Delta }
is the empty set, the deduction theorem claim can be more compactly written as:
A
⊢
B
{\displaystyle A\vdash B}
implies
⊢
A
→
B
{\displaystyle \vdash A\to B}
. The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if
A
{\displaystyle A}
is a closed formula). In general a deduction theorem needs to take into account all logical details of the theory under consideration, so each logical system technically needs its own deduction theorem, although the differences are usually minor.
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. Most notably, the deduction theorem fails to hold in Birkhoff–von Neumann quantum logic, because the linear subspaces of a Hilbert space form a non-distributive lattice.
Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).
Possible passages
Found by search and not yet checked by a person; they may only mention the idea in passing.
Any such select set is called the set of postulates, or premises, from which the reasoning proceeds. The reasoning is nothing else than the exhibition of the whole pattern of general conditions involved in the pattern derived from the selected postulates.
Alfred North Whitehead, Science and the modern world
States what Deduction theorem is.
Or, finally, the premises, of whichever kind they are, may never have been conceived in so distinct a manner as to produce any clear consciousness by what means they were arrived at; as in the case of what is called reasoning in a circle; and then the fallacy is one of Confusion.
John Stuart Mill, A System of Logic, Ratiocinative and Inductive
States what Deduction theorem is.
Hence, in the conclusion of a syllogism we restrict a predicate to a certain object, after having thought it in the major in its whole extent under a certain condition. This complete quantity of the extent in relation to such a condition is called universality (universalitas). To this corresponds totality (universitas) of conditions in the synthesis of intuitions.
Immanuel Kant, The Critique of Pure Reason
States what Deduction theorem is.
Related ideas
- Method of analytic tableaux
- First-order logic
- Garrett Birkhoff
- Free variables and bound variables
- John von Neumann
- Propositional logic
- Modus ponens
- Mathematical logic
- Rule of inference
- Sequent calculus
- Curry–Howard correspondence
- Well-formed formula
- Begging the question
- Tautology (logic)
- Peirce's law
- Natural deduction
- Conditional proof
- Empty set
- Universal generalization
Place in the tradition
Part of Minimal logic.