Deduction theorem

The deduction theorem states that if a formula is derivable from premises plus an assumption, the corresponding implication is derivable from the premises alone. Its precise form depends on the logical system.

Natural deduction: A proof system that represents reasoning with introduction and elimination rules for logical connectives. Its conditional-introduction rule discharges an assumption to derive an implication.
Formal proof: A finite sequence or structured object of expressions justified by explicit inference rules. The theorem compares which conclusions have formal derivations under different premises.
Semantic consequence: A relation in which every model satisfying premises also satisfies the conclusion. The deduction theorem concerns derivability; this relation concerns truth across models.
Proof by conditional introduction: A proof strategy that derives an implication by temporarily assuming its antecedent and proving its consequent. It applies assumption discharge directly to construct implications.
Conditional proof: A proof method that assumes an antecedent temporarily and derives a conditional by discharging that assumption. It is the familiar proof maneuver captured by the theorem.
Logical consequence: A relation in which a conclusion is true in every interpretation satisfying given premises. The semantic analogue connects premise-and-assumption consequence to implication.
Completeness theorem: A theorem stating that every semantically valid consequence is derivable in a specified proof system. It links semantic consequence to derivability rather than discharging a single assumption.
Currying: The transformation that represents a function of multiple arguments as a sequence of single-argument functions. In intuitionistic logic, nested implications correspond to proofs with multiple assumptions.
Sequent calculus: A formal proof system that derives sequents using structural and logical inference rules. Its implication rules express a sequent form of assumption discharge.
Propositional logic: The study of formulas built from propositions using connectives such as negation, conjunction, and implication. The theorem is often first stated and proved for propositional systems.

Linked from 1 page