Normal form (natural deduction)

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. Rocq, 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 ==