Deduction equivalence Glossary
Definition
The deduction equivalence is the fundamental logical
principle governing the implication
connective. It states that
'If A then B' follows from premises if
and only if B follows from those premises
together with A. In symbols:
X ⊢
A IMP B
is equivalent to
X, A
⊢ B
Comments
The deduction equivalence is the basis for the natural deduction rules governing implication. IMPI just is half of the equivalence, while IMPE amounts to the other half massaged into a form where the left sides of the sequents consist of arbitrary assumptions.
The deduction equivalence is sometiomes called the "deduction theorem" as it has to be proved to hold of any deductive system for orthodox logic. For our natural deduction calculus, this is trivial, but for a formulation where the introduction rule for implication is not given as a primitive rule, it may require some work.