Editing Normal form (natural deduction)


{{use dmy dates|date=May 2025}}
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.{{sfn|Prawitz|1965}} 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:{{sfn|von Plato|2013|p=85}}
:''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.{{sfn|Prawitz|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 ''[[Proof theory|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 <math>A \rightarrow A</math> that includes a detour:

<pre>
1. [A]    (assumption)
2. A → A  (→ introduction, discharging 1)
3. [A]    (assumption)
4. A      (→ elimination on 2 and 3)
</pre>

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

<pre>
1. [A]
2. A → A  (→ introduction)
</pre>

=== Conjunction ===
A derivation of <math>A, B \vdash A</math> that includes a detour:

:<math>
\frac{
  \frac{
    A \quad B
  }{
    A \land B
  }[\land\text{I}]
}{
  A
}[\land\text{E}]
\quad \Rightarrow \quad A
</math>

The elimination is unnecessary if <math>A</math> 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 assistant]]s''' (e.g. [[Rocq|Coq]], [[Agda (programming language)|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 calculus|typed lambda calculi]].

== See also ==
* [[Natural deduction]]
* [[Curry–Howard correspondence]]
* [[Cut-elimination theorem]]
* [[Sequent calculus]]

== Notes ==
{{Reflist}}

== References ==
* {{cite thesis | last = Prawitz | first = Dag | author-link=Dag Prawitz | title = Natural Deduction: A Proof-Theoretical Study | publisher = Almqvist & Wiksell | year = 1965 | location = Stockholm | series = Stockholm Studies in Philosophy | volume = 3}}
* {{cite book |last=Prawitz |first=Dag |author-link=Dag Prawitz|year=2006|orig-year=1965 |title=Natural Deduction: A Proof-Theoretical Study |location=Mineola, New York|publisher=[[Dover Publications]]|edition=Reprint of the 1965 thesis|isbn=9780486446554|oclc=61296001}}
* {{cite book | last1=Sørensen | first1=Morten Heine | last2=Urzyczyn | first2=Paweł | title=Lectures on the Curry–Howard isomorphism | publisher=[[Elsevier Science]] | year=2006 | orig-year=1998 | isbn=978-0-444-52077-7 | volume=149 | series=Studies in Logic and the Foundations of Mathematics | citeseerx = 10.1.1.17.7385 }}
* {{cite book |last1=Troelstra |first1=A. S. |last2=Schwichtenberg |first2=H. |year=2000 |title=Basic Proof Theory |publisher=Cambridge University Press |isbn=9780521779111}}
* {{Cite book |last=von Plato |first=Jan|title=Elements of logical reasoning |date=2013 |publisher=[[Cambridge University Press]] |isbn=978-1-107-03659-8 |edition=1|location=Cambridge}}


{{Normal forms in logic}}
{{DEFAULTSORT:Normal Form (Natural Deduction)}}
[[Category:Logic]]