Deduction theorem for propositional logic
ID: deduction-theorem-for-propositional-logic
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.
New to topics? Read the docs here!