Natural Deduction

Natural deduction is a family of proof systems in logic that formalizes deductive reasoning through applications of inference rules. Its characteristic feature is reasoning under temporary assumptions: a proof may contain a subordinate argument whose assumption is later discharged. This structure captures familiar patterns of mathematical proof, such as establishing a conditional by assuming its antecedent and deriving its consequent. “Natural” refers to this intended resemblance to ordinary argumentation, not to an absence of formal constraints. (plato.stanford.edu)

Historical development and presentation

Gerhard Gentzen and Stanisław Jaśkowski independently introduced natural deduction systems in work published in 1934. Gentzen presented derivations as trees, with formulas connected by inference steps; Jaśkowski developed methods for organizing subordinate proofs. Their approaches made hypothetical reasoning an explicit component of a formal system. Natural deduction subsequently became prominent in introductory logic textbooks during the 1950s and 1960s. (plato.stanford.edu)

Different presentations preserve this underlying structure. In proof trees, assumptions appear above the conclusions derived from them, and discharge annotations indicate where their dependence ends. In Fitch notation, numbered lines and indented or boxed subproofs display the scope of assumptions. Presentation conventions differ, so the same argument may have different visual forms without differing in its logical content. (plato.stanford.edu)

Introduction and elimination rules

For propositional logic, rules are commonly organized into introduction and elimination pairs. Introduction rules explain how to establish a compound formula; elimination rules explain how to use one already established. These are rules for constructing formal proofs, rather than procedures for calculating a truth table. (leanprover.github.io)

Typical rules include:

• Conjunction: from $A$ and $B$, infer $A\land B$; from $A\land B$, infer either conjunct.
• Implication: if a subproof derives $B$ under assumption $A$, discharge that assumption and infer $A\to B$. From $A\to B$ and $A$, infer $B$; this elimination rule is modus ponens.
• Disjunction: from $A$, infer $A\lor B$, and similarly from $B$. To use $A\lor B$, derive the same conclusion $C$ separately under assumptions $A$ and $B$, then discharge both case assumptions.
• Negation: derive $\neg A$ by obtaining a contradiction, written $\bot$, under assumption $A$. From $A$ and $\neg A$, infer $\bot$.
• Falsehood: in standard intuitionistic and classical systems, infer any formula from $\bot$. (leanprover.github.io)

An elimination rule does not necessarily produce a shorter formula: disjunction elimination, for example, can establish an arbitrary conclusion supported by both cases. (leanprover.github.io)

Assumptions, discharge, and an example

Assumption discharge changes which premises a conclusion depends on. It does not assert that the temporary assumption was true, nor erase other assumptions still in force. A formula derived inside a subproof cannot simply be reused outside it while ignoring its dependence on the subproof’s assumption. (plato.stanford.edu)

For example, conjunction commutativity has the following derivation:

1. | A ∧ B                 Assumption
2. | A                     ∧ elimination, 1
3. | B                     ∧ elimination, 1
4. | B ∧ A                 ∧ introduction, 3, 2
5. (A ∧ B) → (B ∧ A)       → introduction, 1–4

Lines 2–4 depend on line 1. Line 5 discharges that assumption, establishing a conditional with no remaining premises. This illustrates the difference between proving a conclusion from an assumption and proving that the assumption implies the conclusion. (leanprover.github.io)

Quantifiers and first-order logic

Natural deduction for first-order logic adds rules for quantifiers. Universal elimination permits the passage from $\forall x\,P(x)$ to $P(t)$, provided substitution avoids variable capture. Existential introduction permits the passage from $P(t)$ to $\exists x\,P(x)$. (leanprover.github.io)

The complementary rules impose restrictions on arbitrary parameters. Universal introduction derives $\forall x\,P(x)$ from $P(a)$ only when $a$ is not free in any undischarged assumption on which that derivation depends. Otherwise, a result about a specially constrained object could be mistaken for a result about every object. (leanprover.github.io)

Existential elimination opens a subproof with a fresh parameter $a$ and assumption $P(a)$. A conclusion $C$ may then be inferred from $\exists x\,P(x)$ if $C$ does not depend on the identity of that witness: $a$ must not occur freely in $C$ or the other relevant undischarged assumptions. Equality rules typically supply reflexivity and substitution of equals. (leanprover.github.io)

Classical and intuitionistic systems

Natural deduction is a proof-system format, not a single choice of logic. Standard intuitionistic logic uses the constructive introduction and elimination rules described above. Classical logic can be obtained by adding double-negation elimination, the law of excluded middle, or an appropriate classical proof-by-contradiction rule. Over the usual intuitionistic base, these principles are equivalent. (leanprover.github.io)

The distinction concerns what contradiction establishes. Assuming $A$ and deriving $\bot$ justifies $\neg A$ intuitionistically. Assuming $\neg A$ and deriving $\bot$ directly justifies $\neg\neg A$; inferring $A$ requires a classical principle. (leanprover.github.io)

Metatheory and computational interpretation

Proof theory studies properties of these derivations. Soundness connects derivability with logical validity: if $\Gamma\vdash A$, then $\Gamma\models A$. Completeness establishes the converse relative to the chosen semantics. These properties concern the correspondence between proofs and semantic consequence, not the ease of finding a proof. (leanprover.github.io)

Normalization removes certain inferential detours, such as introducing a conjunction and immediately extracting one of its components. Normalization results depend on the precise calculus; classical rules require particular care. Natural deduction is closely related to sequent calculus, whose cut-elimination results provide another approach to analyzing proof structure. (plato.stanford.edu)

Under the Curry–Howard correspondence, suitable natural deduction systems correspond to typed computational calculi. Propositions correspond to types, proofs to terms, implication introduction to function abstraction, and implication elimination to function application. This connects natural deduction with type theory and programming languages. Proof assistants such as Lean represent related reasoning through machine-checkable proof expressions, although their underlying foundations are richer than elementary natural deduction. (cs.cmu.edu)