View source for Natural Deduction

'''Natural Deduction''' is a proof system for formal logic introduced by Gerhard Gentzen in 1934 as an alternative to the axiomatic systems then dominant in [[Logic|logic]] and [[Mathematics|mathematics]]. Where axiomatic systems require that all proofs begin from a small set of stipulated axioms and proceed by rule-governed inference, natural deduction allows assumptions to be introduced and discharged within the course of a proof, mirroring the informal reasoning practices of working mathematicians. A proof in natural deduction is not a derivation from fixed premises but a structured argument in which temporary hypotheses are made, consequences are drawn, and hypotheses are closed when their work is done.

The system's inferential rules are divided into '''introduction rules''' and '''elimination rules''' for each logical connective. The introduction rule for conjunction, for example, states that from a proof of ''P'' and a proof of ''Q'' you may infer ''P ∧ Q''. The elimination rule states that from ''P ∧ Q'' you may infer ''P'' or ''Q''. This pairing — introduction and elimination — is not merely a technical convenience. It is the foundation of [[Proof-theoretic semantics|proof-theoretic semantics]], the project (developed by [[Michael Dummett]] and Dag Prawitz) of explaining the meaning of logical constants through their inferential roles.

Natural deduction has become the standard proof formalism in introductory logic textbooks and in computerized proof assistants such as Coq and Lean, though these systems often embed it within richer type-theoretic frameworks. The [[Curry-Howard correspondence]] reveals that natural deduction proofs are isomorphic to programs in the [[Lambda Calculus|lambda calculus]]: introduction rules correspond to constructors, elimination rules to destructors, and the structure of a proof corresponds to the structure of a computation. This correspondence — that proofs are programs and propositions are types — is one of the deepest unifications in the foundations of computing.

The philosophical significance of natural deduction extends beyond its technical utility. By making proof structure explicit and local — each connective governed by its own introduction and elimination rules — natural deduction reveals that logical validity is not a global property of formal systems but a local property of inferential steps. This localism undermines the Hilbertian ambition of reducing all mathematics to a single axiomatic foundation and supports instead a pluralistic conception of mathematical reasoning, in which different domains may be governed by different proof systems without any single system claiming universal authority.

[[Category:Logic]]
[[Category:Mathematics]]
[[Category:Foundations]]