Natural Deduction and Gentzen Systems

Motivation: How to Formalize Real Mathematical Reasoning?

Hilbert's axiom system (A1, A2, A3 + MP) is technically adequate, but inconvenient in practice: real mathematicians do not reason in terms of "prove $p \to p$ in five steps." Natural deduction (Gentzen, 1935) is a system that imitates standard mathematical practice: we introduce hypotheses, perform case analysis, apply introduction and elimination rules for connectives. This is the basis of modern proof verification systems (Coq, Lean, Agda).

Rules of Natural Deduction

A proof is a tree with the proven formula at the root and hypotheses at the leaves (which may be "discharged").

Conjunction (∧):

• ∧-introduction (∧I): from $\varphi$ and $\psi$ infer $\varphi \wedge \psi$.
• ∧-elimination (∧E₁): from $\varphi \wedge \psi$ infer $\varphi$. (∧E₂): infer $\psi$.

Implication (→):

• →-introduction (→I): if $\psi$ is derived from $[\varphi]$ (the hypothesis $\varphi$ is discharged) then infer $\varphi \to \psi$.
• →-elimination (modus ponens): from $\varphi \to \psi$ and $\varphi$ infer $\psi$.

Disjunction (∨):

• ∨-introduction: from $\varphi$ infer $\varphi \vee \psi$ (and from $\psi$ infer $\varphi \vee \psi$).
• ∨-elimination: from $\varphi \vee \psi$, $[\varphi] \vdash \chi$, $[\psi] \vdash \chi$ infer $\chi$ (case analysis).

Negation: $\neg \varphi := \varphi \to \bot$. From $\varphi$ and $\neg \varphi$ infer $\bot$. From $[\neg \varphi] \vdash \bot$ infer $\varphi$ (reductio ad absurdum — in classical logic).

Quantifiers (First-Order Predicate Logic):

• $\forall$-introduction: from $\varphi(y)$ (where $y$ is not free in the hypotheses) infer $\forall x,\varphi(x)$.
• $\forall$-elimination: from $\forall x,\varphi(x)$ infer $\varphi(t)$ for any term $t$.
• $\exists$-introduction: from $\varphi(t)$ infer $\exists x,\varphi(x)$.
• $\exists$-elimination: from $\exists x \varphi(x)$ and $[\varphi(y)\vdash\chi]$ (where $y$ is not free in $\chi$) infer $\chi$.

Curry–Howard Correspondence

Isomorphism of Types and Proofs:

Consequence: a constructive proof of $\varphi \to \psi$ is a program transforming a proof of $\varphi$ into a proof of $\psi$. In Coq and Agda: writing programs = constructing mathematical proofs.

Numerical Example

Problem: To prove in natural deduction: $(p \wedge q) \to (q \wedge p)$ (commutativity of conjunction).

Step 1. Introduce the hypothesis $[h: p \wedge q]$.

Step 2. Apply ∧E₂ to $h$: deduce $q$.

Step 3. Apply ∧E₁ to $h$: deduce $p$.

Step 4. Apply ∧I to $q$ and $p$: obtain $q \wedge p$.

Step 5. Apply →I, discharging hypothesis $h$: obtain $(p \wedge q) \to (q \wedge p)$. ■

Proof tree (schematically):

$[p \wedge q]^h \xrightarrow{\wedge E_2} q;\ [p \wedge q]^h \xrightarrow{\wedge E_1} p;$ then $\wedge I$ gives $q \wedge p$; rule $\to I$ discharges $h$ to obtain $(p \wedge q) \to (q \wedge p)$.

Corresponding λ-term: $\lambda h: A \times B.\ \langle \pi_2(h),\ \pi_1(h)\rangle$ — a function that takes a pair $(h.\text{first},\ h.\text{second})$ and returns $(h.\text{second},\ h.\text{first})$. This is exactly swap: $A \times B \to B \times A$.

Additional Aspects

Proof theory is the branch of logic studying proofs as formal objects. Hilbert systems provide an axiomatic approach; Gentzen's natural deduction is closer to intuitive reasoning; the sequent calculi LK/LJ make it possible to prove normalization theorems (cut-elimination). From cut-elimination follow the consistency of arithmetic (Gentzen 1936, via $\varepsilon_0$-induction), the Craig interpolation theorem, and Herbrand's theorem. Modern applications: Coq, Lean, Agda — interactive provers based on type theory and the Curry–Howard principle (programs = proofs, types = formulas). In Lean, theorems such as Fermat's, fragments of the classification of finite simple groups, and large portions of analysis textbooks have already been formalized, ushering in the era of verified mathematics.

Real-World Application

Coq is a language for proofs and programming based on natural deduction with dependent types. The Feit–Thompson theorem proof in Coq (Gonthier et al., 2012): 150,000 lines, 6 years of work. Used in OS kernel verification (CompCert — certified C compiler).

Connection with Other Areas of Mathematics

Natural deduction and sequent systems provide a language for analyzing structural properties of proofs, which is then transferred into “real” mathematics. In differential equations, the Gödel–Gentzen techniques of normalization and cut-elimination underlie constructive versions of existence theorems: the Gödel–Gentzen–Kreisel interpretations allow one to extract an explicit algorithm for constructing a solution from a non-constructive proof when initial data is given. This approach was used, for example, by Ulrich Kohler and Ulrich Kohler–Koch for analyzing proofs in the theory of boundary values for solutions of elliptic equations.

In algebra, natural deduction is closely related to category theory. Lambek's results show that proofs in intuitionistic logic correspond to morphisms in cartesian closed categories, and the rules of natural deduction translate into composition and exponential objects. Generalization to Girard's linear logic leads to monoidal closed categories, and further, to models in operator theory and quantum logic.

In topology, higher-order logic and dependent types (as a generalization of natural deduction) are realized in Voevodsky's univalent foundations: types are regarded as spaces, terms as points, and equalities as paths. Here, the introduction and elimination rules for quantifiers and type constructors describe topological operations, and the Curry–Howard–Lambek correspondence becomes a bridge between homotopical algebra and formal logic.

In probability theory, logic with natural deduction is applied via the stochastic λ-calculus apparatus: the work of Jones and Morgan connects proofs with probabilistic programs, and normalization of proofs is interpreted as a process of sampling distributions. In numerical methods, analysis of proofs of convergence and stability theorems makes it possible, through program extractors (Kreisel, Kohlenbach), to obtain explicit algorithmic estimates and bounds for rates of convergence of iteration schemes.

Historical Note and Development of the Idea

The prerequisites of natural deduction can be traced to the works of Frege (Begriffsschrift, 1879) and the subsequent axiomatization of Hilbert (Grundlagen der Geometrie, 1899), where the idea of controlled derivation from explicitly listed premises was already present. However, it was Gerhard Gentzen in the article "Untersuchungen über das logische Schließen" (Mathematische Zeitschrift, 1934–1935) who formalized natural deduction and sequent calculus as two interconnected proof formats. Gentzen's motivation was Hilbert's program for the foundation of arithmetic and the need for syntactic proof analysis. His cut-elimination theorem (1935) and subsequent 1936 work on the consistency of Peano arithmetic via transfinite induction up to ordinal $\varepsilon_0$ became central results in early proof theory. In the mid-twentieth century, Gentzen's ideas were developed by Paul Lorenzen, Stephen Kleene, Kurt Schütte, who systematized various variants of natural deduction and sequent systems for intuitionistic and classical logic.