Deduction theorem for propositional logic ($S\cup \{\varphi \}⊢\psi ⟺S⊢\varphi \Rightarrow \psi$)

An implication is derivable from a theory precisely when its conclusion is derivable after adjoining its antecedent. Together with classical contradiction rules, this identifies failure to prove a proposition with consistency after adjoining its negation.

Conditional modus ponens derives $A\to C$ from $A\to B$ and $A\to (B\to C)$. It is the step which translates a modus ponens rule inference when discharging a common assumption. In the case-elimination Hilbert calculus, the third scheme first gives $A\to (\neg B\to C)$; the second scheme combines the two conditionals to give $A\to C$.

In the usual first-order Hilbert system, logical implication discharge requires the appropriate generalization restriction: a variable generalized in the derivation must not be free in the assumption being discharged. Equivalently use a proof system whose generalization rule already forbids variables free in open assumptions. One can first discharge a temporary assumption and then generalize if the quantified variable is not free in the remaining assumptions. Ignoring this side condition would allow deriving universal conclusions from a single arbitrary instance as an open hypothesis.

For standard effective proof presentations, the syntactic deduction theorem and its reverse give effective transformations between proofs in a one-sentence extension and proofs of an implication in the base theory. Arithmetic can verify these transformations, yielding the displayed internal equivalence under the usual representation and proof-predicate hypotheses. It distinguishes internal proof transformations from an unlicensed reflection step taking provability to truth.