Definition
Natural deduction is a style of formal proof system developed by Gerhard Gentzen and Stanisław Jaśkowski in the 1930s, designed to mirror the patterns of ordinary mathematical and philosophical argument. Instead of starting from a small list of axioms and deriving theorems by substitution, natural deduction gives each logical connective a pair of rules: an introduction rule that tells you how to derive a statement built with that connective, and an elimination rule that tells you what you can do with a statement once you have it. A proof is a tree or sequence of lines, each justified by one of these rules applied to earlier lines.
The result feels closer to how working mathematicians actually reason than the older axiomatic systems of Frege, Russell, or Hilbert. Assumptions can be introduced and later discharged, sub-proofs can be nested, and the overall structure tracks the informal moves of conditional proof and proof by contradiction.
Why it matters
How it works
The signature features of a natural deduction proof are assumption introduction and assumption discharge. To prove a conditional statement of the form "if P then Q", a natural deduction proof temporarily assumes P, derives Q within the scope of that assumption, and then discharges the assumption when stating the conditional as a conclusion. The discharge step is what distinguishes natural deduction from axiomatic systems: an assumption used inside a sub-proof leaves no residue in the final claim. The proof says, in effect, "supposing P were true, Q would follow" — exactly the informal pattern of conditional reasoning.
Each connective has its own pair of rules. Conjunction introduction lets you combine two derived statements into a conjunction; conjunction elimination lets you extract either component from a conjunction. Disjunction introduction is generous — any statement can be weakened into a disjunction — while disjunction elimination requires a more careful argument by cases. Conditional introduction discharges an assumption; conditional elimination is modus ponens. Negation, universal, and existential quantifiers each get their own paired rules. The collection is small enough to memorise and powerful enough to derive every theorem of classical propositional and predicate logic. This balance of expressivity and modularity is why natural deduction now dominates logic pedagogy and underlies many computer-checked proof systems.