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.

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:

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:

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: