Formal Proof Systems and Natural Deduction

⚡ Key Takeaways

Formal proof systems are precise, rule-governed frameworks for deriving theorems from axioms and assumptions. Natural deduction, introduced by Gentzen and Jaśkowski (1934), is a proof system designed to mirror intuitive human reasoning through introduction and elimination rules for each logical connective. It applies across logic, mathematics, type theory, and computer science. Result in words: any valid argument of classical (or intuitionistic) propositional and predicate logic can be derived using a small fixed set of inference rules.

💡 The Core Insight

Every logical connective is fully characterized by how to prove it (its introduction rule) and how to use it (its elimination rule). These two rules stand in perfect harmony: the elimination rule extracts exactly the information that the introduction rule put in, no more and no less. This balance — called local soundness and local completeness — is the conceptual heart of natural deduction and explains why proofs can be normalized (simplified to a canonical form without detours).

Formal Statement

DefinitionFormal Proof System

A formal proof system is a triple ⟨L,A,R⟩\langle \mathcal{L}, \mathcal{A}, \mathcal{R}\rangle where:

  • L\mathcal{L} is a formal language: a set of well-formed formulas (wffs) built recursively from atomic symbols and connectives.
  • A⊆L\mathcal{A} \subseteq \mathcal{L} is a (possibly empty) set of axioms.
  • R\mathcal{R} is a set of inference rules, each a relation between finite sets of premises and a conclusion.

A derivation of φ\varphi from a set of hypotheses Γ\Gamma is a finite tree whose root is φ\varphi, whose leaves are elements of Γ∪A\Gamma \cup \mathcal{A} (or discharged assumptions), and each of whose internal nodes follows from its children by a rule in R\mathcal{R}. We write Γ⊢φ\Gamma \vdash \varphi to mean such a derivation exists.

The central syntactic relation is derivability:

1
Γ⊢φ  ⟺  there is a finite derivation of φ with undischarged hypotheses⊆Γ\quad \Gamma \vdash \varphi \iff \text{there is a finite derivation of } \varphi \text{ with undischarged hypotheses} \subseteq \Gamma

Derivation hint: Read ⊢\vdash as "proves"; it is purely syntactic, defined by the existence of a rule-governed tree, independent of meaning or truth. The complementary semantic relation is entailment:

2
Γ⊨φ  ⟺  every model (valuation) satisfying all of Γ also satisfies φ\quad \Gamma \models \varphi \iff \text{every model (valuation) satisfying all of } \Gamma \text{ also satisfies } \varphi

Derivation hint: ⊨\models quantifies over all interpretations; contrast it with ⊢\vdash, which quantifies over proofs. The Soundness and Completeness theorems link the two. The natural deduction rules for the propositional connectives are:

3
φψφ∧ψ (∧I)φ∧ψφ (∧E1)φ∧ψψ (∧E2)\quad \dfrac{\varphi \quad \psi}{\varphi \wedge \psi}\ (\wedge I) \qquad \dfrac{\varphi \wedge \psi}{\varphi}\ (\wedge E_1) \qquad \dfrac{\varphi \wedge \psi}{\psi}\ (\wedge E_2)

Derivation hint: To introduce a conjunction you must already have both conjuncts; to use one, you may extract either component.

4
[φ] n    ⋮    ψφ→ψ (→I, n)φ→ψφψ (→E)\quad \dfrac{[\varphi]^{\,n} \;\;\vdots\;\; \psi}{\varphi \to \psi}\ (\to I,\,n) \qquad \dfrac{\varphi \to \psi \quad \varphi}{\psi}\ (\to E)

Derivation hint: →I\to I discharges the temporary assumption φ\varphi (labelled nn); →E\to E is modus ponens. The bracket notation [φ]n[\varphi]^n marks an assumption that is later cancelled.

5
φφ∨ψ (∨I1)ψφ∨ψ (∨I2)φ∨ψ[φ]n⋮χ[ψ]m⋮χχ (∨E, n,m)\quad \dfrac{\varphi}{\varphi \vee \psi}\ (\vee I_1) \qquad \dfrac{\psi}{\varphi \vee \psi}\ (\vee I_2) \qquad \dfrac{\varphi \vee \psi \quad \begin{array}{c}[\varphi]^n\\ \vdots\\ \chi\end{array} \quad \begin{array}{c}[\psi]^m\\ \vdots\\ \chi\end{array}}{\chi}\ (\vee E,\,n,m)

Derivation hint: Disjunction elimination is proof by cases: if χ\chi follows from each disjunct separately, it follows from the disjunction.

6
[φ]n⋮⊥¬φ (¬I, n)φ¬φ⊥ (¬E)⊥φ (⊥E)\quad \dfrac{\begin{array}{c}[\varphi]^n\\ \vdots\\ \bot\end{array}}{\neg\varphi}\ (\neg I,\,n) \qquad \dfrac{\varphi \quad \neg\varphi}{\bot}\ (\neg E) \qquad \dfrac{\bot}{\varphi}\ (\bot E)

Derivation hint: ¬φ\neg\varphi is defined operationally as "φ\varphi leads to absurdity"; ⊥E\bot E (ex falso quodlibet) lets anything follow from a contradiction. The quantifier rules require eigenvariable conditions:

7
φ(a)∀x φ(x) (∀I)†∀x φ(x)φ(t) (∀E)φ(t)∃x φ(x) (∃I)∃x φ(x)[φ(a)]n⋮χχ (∃E, n)‡\quad \dfrac{\varphi(a)}{\forall x\,\varphi(x)}\ (\forall I)^{\dagger} \qquad \dfrac{\forall x\,\varphi(x)}{\varphi(t)}\ (\forall E) \qquad \dfrac{\varphi(t)}{\exists x\,\varphi(x)}\ (\exists I) \qquad \dfrac{\exists x\,\varphi(x) \quad \begin{array}{c}[\varphi(a)]^n\\ \vdots\\ \chi\end{array}}{\chi}\ (\exists E,\,n)^{\ddagger}

Derivation hint: †\dagger — in ∀I\forall I, the variable aa must not occur free in any undischarged hypothesis; ‡\ddagger — in ∃E\exists E, the witness aa must not occur in χ\chi or remaining hypotheses. These conditions guard against illicit generalization.

TheoremSoundness and Completeness (Gödel, 1929)

For classical first-order logic, derivability and entailment coincide:

Γ⊢φ⟺Γ⊨φ.\Gamma \vdash \varphi \quad\Longleftrightarrow\quad \Gamma \models \varphi.

The left-to-right direction is soundness (every provable formula is valid); the right-to-left is completeness (every valid formula is provable).

Why It Holds / Derivation

ProofSketch of Soundness for →I\to I and →E\to E

We prove Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi by induction on the height of the derivation. We show the inductive cases for implication; other rules are analogous. 1. Base case. A leaf φ∈Γ\varphi \in \Gamma trivially satisfies Γ⊨φ\Gamma \models \varphi, since any model of Γ\Gamma satisfies each of its members. 2. Case →E\to E. Suppose the last rule is →E\to E, with premises φ→ψ\varphi \to \psi and φ\varphi derived from Γ\Gamma. By the induction hypothesis Γ⊨φ→ψ\Gamma \models \varphi \to \psi and Γ⊨φ\Gamma \models \varphi. Take any model MM with M⊨ΓM \models \Gamma. Then M⊨φ→ψM \models \varphi \to \psi and M⊨φM \models \varphi, so by the truth-table for →\to, M⊨ψM \models \psi. Hence Γ⊨ψ\Gamma \models \psi. 3. Case →I\to I. Suppose the last rule is →I\to I discharging assumption φ\varphi: from Γ,φ⊢ψ\Gamma, \varphi \vdash \psi we conclude Γ⊢φ→ψ\Gamma \vdash \varphi \to \psi. By induction Γ,φ⊨ψ\Gamma, \varphi \models \psi. Take any M⊨ΓM \models \Gamma. If M⊨φM \models \varphi, then M⊨Γ∪{φ}M \models \Gamma \cup \{\varphi\}, so M⊨ψM \models \psi; thus M⊨φ→ψM \models \varphi \to \psi. If M⊭φM \not\models \varphi, then M⊨φ→ψM \models \varphi \to \psi vacuously. Either way Γ⊨φ→ψ\Gamma \models \varphi \to \psi. 4. By structural induction over all rules, every derivable sequent is valid. ■\blacksquare (Completeness is harder; the standard route is the Henkin construction, building a model from a maximally consistent, witnessed extension of Γ\Gamma.)

∎
GG
Gerhard Gentzen
1909–1945

Gerhard Gentzen, a German mathematician and logician, invented both natural deduction (natürliches Schließen) and the sequent calculus in his 1934–35 doctoral work Untersuchungen über das logische Schließen ("Investigations into Logical Deduction"). His goal was to formalize reasoning "as it actually occurs in mathematical proofs," in contrast to the artificial axiom chains of Frege, Russell, and Hilbert. Gentzen's crowning achievement was the Hauptsatz (cut-elimination theorem) and a consistency proof of arithmetic using transfinite induction up to ε0\varepsilon_0. He died of starvation in a Prague prison camp in 1945, but his methods became the foundation of proof theory and, decades later, of computer-checked mathematics.

Building Intuition

🧠 Intuition

Think of natural deduction as a game of assumptions and debts. When you write down "φ→ψ\varphi \to \psi", you are claiming: if you grant me φ\varphi, I can pay you back ψ\psi. To prove it, you temporarily borrow φ\varphi (open a sub-proof), use it freely to reach ψ\psi, then repay the debt by discharging φ\varphi — the implication packages "φ\varphi in, ψ\psi out" into a single statement that no longer depends on the borrowed assumption. Every connective has this dual rhythm: a constructor (introduction) telling you how to manufacture it, and a destructor (elimination) telling you what you can do with it once built. Proof becomes a kind of bookkeeping: assumptions are opened, used, and closed, and the structure of the final formula records exactly which debts remain (the undischarged hypotheses Γ\Gamma) and which have been settled.

Figure
Natural deduction derivation tree for (φ→ψ)→(¬ψ→¬φ)(\varphi \to \psi)\to(\neg\psi \to \neg\varphi) — contraposition
Derivation of contraposition [φ→ψ]³ [φ]¹ [¬ψ]² →E ψ ¬E ⊥ ¬I ¹ ¬φ →I ² ¬ψ → ¬φ →I ³ (φ→ψ) → (¬ψ → ¬φ) Bracketed formulas [·]ⁿ are temporary assumptions, discharged at the rule labelled n. Each horizontal bar is a rule application; premises above, conclusion below. Gold = key intermediate/final formulas. All three assumptions are eventually discharged.

Worked Examples

ExampleProving φ∧ψ⊢ψ∧φ\varphi \wedge \psi \vdash \psi \wedge \varphi (commutativity of conjunction)

Given: the single hypothesis φ∧ψ\varphi \wedge \psi. Goal: derive ψ∧φ\psi \wedge \varphi. Steps (each line justified by a rule): 1. φ∧ψ\varphi \wedge \psi — hypothesis (assumption in Γ\Gamma). 2. ψ\psi — from line 1 by ∧E2\wedge E_2. 3. φ\varphi — from line 1 by ∧E1\wedge E_1. 4. ψ∧φ\psi \wedge \varphi — from lines 2 and 3 by ∧I\wedge I. No assumptions remain undischarged besides the original hypothesis, so we have shown φ∧ψ⊢ψ∧φ\varphi \wedge \psi \vdash \psi \wedge \varphi.

 φ∧ψ  ⊢  ψ∧φ \boxed{\ \varphi \wedge \psi \;\vdash\; \psi \wedge \varphi\ }
ExampleProving the tautology ⊢φ→(ψ→φ)\vdash \varphi \to (\psi \to \varphi) from no hypotheses

Given: nothing (we prove a theorem outright, Γ=∅\Gamma = \varnothing). Goal: φ→(ψ→φ)\varphi \to (\psi \to \varphi). Steps: 1. Assume φ\varphi. — open assumption [φ]1[\varphi]^1. 2. Assume ψ\psi. — open assumption [ψ]2[\psi]^2. 3. φ\varphi — reiterate line 1 (it is still available; ψ\psi was not needed). 4. ψ→φ\psi \to \varphi — from the sub-proof (2)–(3) by →I\to I, discharging [ψ]2[\psi]^2. 5. φ→(ψ→φ)\varphi \to (\psi \to \varphi) — from the sub-proof (1)–(4) by →I\to I, discharging [φ]1[\varphi]^1. Both assumptions are discharged, leaving an empty hypothesis set:

 ⊢ φ→(ψ→φ) \boxed{\ \vdash\ \varphi \to (\psi \to \varphi)\ }

Notice the assumption ψ\psi was introduced and discharged without ever being used — perfectly legal in natural deduction, and the syntactic shadow of the "weakening" allowed in this tautology.

Common Misconceptions

⚠️ Common mistake

⊢\vdash and ⊨\models are not the same symbol with the same meaning. Γ⊢φ\Gamma \vdash \varphi is syntactic — it asserts a proof object exists. Γ⊨φ\Gamma \models \varphi is semantic — it asserts truth-preservation over all models. They coincide only because of the Soundness and Completeness theorems, which are nontrivial results, not definitions. In incomplete systems (e.g., second-order logic under standard semantics), ⊨\models can hold without ⊢\vdash.

Discharge is mandatory bookkeeping, not optional. A formula derived under an open assumption still depends on it. You cannot claim ⊢φ→ψ\vdash \varphi \to \psi unless the assumption φ\varphi has actually been discharged by →I\to I. Forgetting to discharge — or discharging a variable that violates the eigenvariable condition — produces invalid "proofs."

CounterexampleIllicit ∀\forall-introduction

Consider the (false) attempted derivation that everything equals a fixed witness. Suppose we have P(a)P(a) as a hypothesis, where aa is a free variable occurring in the assumption. Applying ∀I\forall I to conclude ∀x P(x)\forall x\, P(x) is forbidden, because the eigenvariable condition requires that aa not occur free in any undischarged hypothesis. If we ignored this, we could "prove":

P(a)  ⊢  ∀x P(x),P(a) \;\vdash\; \forall x\, P(x),

i.e. because a single object aa has property PP, every object does — patently invalid. Take P(x):=P(x) := "xx is even" and a:=2a := 2: from "2 is even" we would derive "every number is even." The eigenvariable condition exists precisely to block this fallacy: aa must be arbitrary, used nowhere else, so that generalizing over it is sound.

Connections

connection

Natural deduction sits at the crossroads of several fields. It is equivalent in deductive power to Hilbert-style systems and to Gentzen's <span class="wiki-link-missing">Sequent Calculus</span>, but trades many axioms for many rules and explicit assumption management. Through the <span class="wiki-link-missing">Curry–Howard Correspondence</span>, intuitionistic natural deduction proofs correspond exactly to terms of the simply typed lambda calculus: introduction rules build data, elimination rules consume it, and <span class="wiki-link-missing">Proof Normalization</span> corresponds to program evaluation (β\beta-reduction). The semantic side connects to <span class="wiki-link-missing">Model Theory</span> via the Soundness/Completeness bridge, and the limits of provability connect to <a class="wiki-link" href="/wiki/godels-incompleteness-theorems">Gödel&#39;s Incompleteness Theorems</a>. The constructive fragment relates to <span class="wiki-link-missing">Intuitionistic Logic</span>, where the law of excluded middle φ∨¬φ\varphi \vee \neg\varphi is not derivable.

Real-World Applications

🔬 Where this appears

Historical Development

⏳ History
- 1879 — Gottlob Frege publishes Begriffsschrift, the first formal logical system with quantifiers, using an axiomatic (Hilbert-style avant la lettre) approach.
- 1910–1913 — Whitehead and Russell's Principia Mathematica develops a vast axiomatic deduction of mathematics from logic.
- 1920s — David Hilbert and Paul Bernays refine the axiomatic ("Hilbert-style") proof system and pose the Entscheidungsproblem and consistency program.
- 1929 — Kurt Gödel proves the Completeness Theorem for first-order logic in his doctoral dissertation.
- 1934 — Stanisław Jaśkowski publishes a system of "suppositional" reasoning (the basis of Fitch-style proofs), independently of Gentzen.
- 1934–1935 — Gerhard Gentzen introduces natural deduction and the sequent calculus; proves the Hauptsatz (cut elimination).
- 1936 — Gentzen gives a consistency proof of Peano arithmetic via transfinite induction to ε0\varepsilon_0.
- 1958–1969 — Haskell Curry and William Howard articulate the proofs-as-programs correspondence, linking deduction to computation.
- 1965–1971 — Dag Prawitz's monograph Natural Deduction systematizes normalization theory; Per Martin-Löf develops intuitionistic type theory, marrying natural deduction to constructive mathematics.

Subtleties & Limits

open-problem

Natural deduction is complete for classical and intuitionistic first-order logic, but the surrounding landscape contains deep limits. By <a class="wiki-link" href="/wiki/godels-incompleteness-theorems">Gödel&#39;s Incompleteness Theorems</a>, any consistent, recursively axiomatized system strong enough to encode arithmetic contains true sentences it cannot prove — so no single natural-deduction system captures all mathematical truth. The exact proof-theoretic strength (the ordinal measuring how much induction a theory's consistency requires) is known for arithmetic (ε0\varepsilon_0) but remains open or only partially determined for many strong subsystems of second-order arithmetic and set theory — the program of ordinal analysis. A related research frontier asks how to design natural-deduction systems with optimal normalization and harmony properties for non-classical logics (modal, linear, substructural), where the clean introduction/elimination symmetry of Gentzen's connectives is harder to preserve. Whether all "logical" constants admit harmonious natural-deduction rules — Prawitz's and Dummett's question of what counts as a logical constant — remains philosophically and technically unsettled.

See Also

Sequent Calculus · Curry–Howard Correspondence · Intuitionistic Logic · First-Order Logic · Hilbert Systems · Proof Normalization · Gödel's Incompleteness Theorems · Model Theory · Type Theory