Deduction Theorem

- Natural & Formal Sciences -
Mathematics & Logic Dictionary
A metatheorem relating syntactic provability to implication: if a formula B is provable from assumption A (possibly together with other assumptions), then the implication A → B is provable in the surrounding formal system, subject to system-specific conditions about discharged assumptions.