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

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 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 $A\rightarrow A$ 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 $A,B\vdash A$ that includes a detour:

${\frac {{\frac {A\quad B}{A\land B}}[\land {\text{I}}]}{A}}[\land {\text{E}}]\quad \Rightarrow \quad A$

The elimination is unnecessary if $A$ 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. Coq, Agda), 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 calculi.

See also

• Natural deduction
• Curry–Howard correspondence
• Cut-elimination theorem
• Sequent calculus

References

• Prawitz, Dag (1965). Natural Deduction: A Proof-Theoretical Study (Thesis). Stockholm Studies in Philosophy. Vol. 3. Stockholm: Almqvist & Wiksell.
• Prawitz, Dag (2006) [1965]. Natural Deduction: A Proof-Theoretical Study (Reprint of the 1965 thesis ed.). Mineola, New York: Dover Publications. ISBN 9780486446554. OCLC 61296001.
• 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. CiteSeerX 10.1.1.17.7385. ISBN 978-0-444-52077-7.
• Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory. Cambridge University Press. ISBN 9780521779111.
• von Plato, Jan (2013). Elements of logical reasoning (1 ed.). Cambridge: Cambridge University Press. ISBN 978-1-107-03659-8.