Definition
Natural Deduction
Natural deduction is a proof calculus built around primitive introduction inference rules and elimination inference rules for logical operators. These rules directly construct proofs, rather than merely abbreviating derivations using axioms and modus ponens as in a Hilbert calculus.
Some primitive rules discharge temporary assumptions: if assuming
lets us derive , implication introduction concludes without assuming : The brackets mark the assumption
being discharged by this inference. Any other assumptions used remain in effect.