In mathematical logic and proof theory, a derivation in normal form in the context of natural deduction refers to a proof which contains no detours – steps in which a formula is first introduced and then immediately eliminated.
The concept of normalization in natural deduction was introduced by Dag Prawitz in the 1960s as part of a general effort to analyze the structure of proofs and eliminate unnecessary reasoning steps. The associated normalization theorem establishes that every derivation in natural deduction can be transformed into normal form.
Definition
Natural deduction is a system of formal logic that uses introduction and elimination rules for each logical connective. Introduction rules describe how to construct a formula of a particular form, while elimination rules describe how to infer information from such formulas. A derivation is in normal form if it contains no formula which is both:
the conclusion of an introduction rule, and
the major premise of an elimination rule.
A derivation containing such a structure is said to include a detour. Normalization involves transforming a derivation to remove all such detours, thereby producing a proof that directly reflects the logical dependencies of the conclusion on the assumptions.
Another definition of normal derivation in classical logic with general elimination rules is:
A derivation in NK is normal if all major premisses of E-rules are assumptions.
Normalization theorem
The normalization theorem for natural deduction states that:
Every derivation in natural deduction can be converted into a derivation in normal form.
This result was first proved by Dag Prawitz in 1965. The normalization process typically involves identifying and eliminating maximal formulas – formulas introduced and immediately eliminated—through a sequence of local reduction steps.
Normalization has several important consequences:
It implies the subformula property: any formula occurring in the proof is a subformula of the assumptions or conclusion.
It guarantees consistency of the system: there is no derivation of a contradiction from no assumptions.
It supports constructive content in logic: proofs correspond to explicit constructions or computations.
Examples
Implication
A derivation of that includes a detour:
1. [A] (assumption)
2. A → A (→ introduction, discharging 1)
3. [A] (assumption)
4. A (→ elimination on 2 and 3)
This introduces and then immediately eliminates an implication. A normal derivation is:
1. [A]
2. A → A (→ introduction)
Conjunction
A derivation of that includes a detour:
The elimination is unnecessary if is already available.
Applications
Normalization is central to several areas of logic and computer science:
In proof theory, it ensures that logical systems have desirable meta-properties such as consistency and the subformula property.
In type theory, it underlies the soundness and completeness of type-checking algorithms.
In proof assistants (e.g. Rocq, Agda), normalization is used to verify that formal proofs are constructive and terminating.
Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998]. Lectures on the Curry–Howard isomorphism. Studies in Logic and the Foundations of Mathematics. Vol.149. Elsevier Science. ISBN978-0-444-52077-7.
Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory. Cambridge University Press. ISBN9780521779111.
von Plato, Jan (2013). Elements of logical reasoning (1ed.). Cambridge: Cambridge University Press. ISBN978-1-107-03659-8.
![{\displaystyle {\frac {{\frac {A\quad B}{A\land B}}[\land {\text{I}}]}{A}}[\land {\text{E}}]\quad \Rightarrow \quad A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/55f62f8f8d4468c52034a6b9e81218b075a756ec)
