Natural deduction

Summary

Natural deduction is a proof system whose rules mimic the way mathematicians reason. Each connective has introduction rules, which say how to prove a formula with it, and elimination rules, which say how to use such a formula. Assumptions can be made for a while and then discharged, as in "suppose $\varphi$; then ...; hence $\varphi \to \psi$". It was introduced by Gerhard Gentzen, and independently by Stanisław Jaśkowski, and it is a basic system of proof theory.