Normal form (natural deduction)

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

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 is:

Normalization theorem

The normalization theorem for natural deduction states that:
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. 
2. A → A 
3. 
4. A

This introduces and then immediately eliminates an implication. A normal derivation is:


1. 
2. A → A

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, normalization is used to verify that formal proofs are constructive and terminating.
In functional programming, the normalization process corresponds to evaluation strategies for Typed [lambda calculus|typed lambda calculi].