Editing Deduction theorem (section)

{{Short description|Metatheorem in mathematical logic}}
{{use dmy dates|date=May 2025}}
In [[mathematical logic]], a '''deduction theorem''' is a [[metatheorem]] that justifies doing [[conditional proof]]s from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication <math>A \to B</math>, it is sufficient to assume <math>A</math> as a hypothesis and then proceed to derive <math>B</math>. Deduction theorems exist for both [[propositional logic]] and [[first-order logic]].{{sfn|Kleene|2002|p=39,112}}{{sfn|Shoenfield|2001|p=33}} The deduction theorem is an important tool in [[Hilbert-style deduction system]]s 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 <math>B</math> is deducible from a set of assumptions <math>\Delta \cup \{A\}</math> then the implication <math> A \to B </math> is deducible from <math>\Delta </math>; in symbols, <math>\Delta \cup \{A\} \vdash B </math> implies <math>\Delta \vdash A \to B </math>. In the special case where <math>\Delta </math> is the [[empty set]], the deduction theorem claim can be more compactly written as: <math>A \vdash B</math> implies <math>\vdash A \to B</math>. The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if <math>A</math> is a [[sentence (mathematical logic)|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<ref>For example, [[Hilbert-style deductive system]]s, [[natural deduction]], the [[sequent calculus]], the [[Method of analytic tableaux|tableaux method]], and [[Resolution (logic)|resolution]] —see [[First order logic]]</ref> [[First order logic#Deductive systems|deductive system]]s for first-order logic.<ref>An explicit verification of this result may be found in https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v</ref> However, there are first-order systems in which new inference rules are added for which the deduction theorem fails.{{sfn|Kohlenbach|2008|p=148}} Most notably, the deduction theorem fails to hold in [[Garrett Birkhoff|Birkhoff]]–[[John von Neumann|von Neumann]] [[quantum logic]], because the [[linear subspace]]s of a [[Hilbert space]] form a [[distributive lattice | non-distributive lattice]].