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.[1] The associated normalization theorem establishes that every derivation in natural deduction can be transformed into normal form.
Definition
[edit]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:[2]
- A derivation in NK is normal if all major premisses of E-rules are assumptions.
Normalization theorem
[edit]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.[1] 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
[edit]Implication
[edit]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
[edit]A derivation of that includes a detour:
The elimination is unnecessary if is already available.
Applications
[edit]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
[edit]Notes
[edit]- ^ a b Prawitz 1965.
- ^ von Plato 2013, p. 85.
References
[edit]- 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.