Draft:Normalization thesis

  • Comment: All information provided needs to be backed with inline citations referencing verifiable secondary sources. Dan arndt (talk) 04:50, 23 March 2026 (UTC)

In proof theory and mathematical logic, the Normalization Thesis (also known as the Martin-Löf–Prawitz Conjecture on the identity of proofs) is a proposal for defining when two different formal derivations represent the same underlying mathematical proof.

The thesis suggests that the identity of a proof is determined by its normal form. It provides a technical solution to the philosophical question: "When are two proofs the same?"

Definition

The conjecture states that:

Two derivations represent the same proof if and only if they reduce to the same normal form (or long normal form) under a specified set of reduction rules (normalization).

In the context of natural deduction, this means that two arguments are equivalent if, after all "logical detours" (the introduction of a connective immediately followed by its elimination) are removed, the resulting irreducible proof trees are identical.

History and Attribution

The thesis is the subject of a famous mutual attribution between Dag Prawitz and Per Martin-Löf.

  • Prawitz (1971) originally proposed that the equivalence relation generated by reduction steps defines the identity of proofs, attributing it to Martin-Löf.
  • Conversely, Martin-Löf has referred to the conjecture as formulated in Prawitz’s 1971 paper.

This correspondence is deeply linked to the Curry–Howard isomorphism, which equates proofs with lambda terms. In this framework, the Normalization Thesis is equivalent to saying that two proofs are identical if their corresponding terms have the same β-normal form.

Connection to Hilbert's 24th Problem

The Normalization Thesis is often viewed as a potential answer to Hilbert's twenty-fourth problem. Hilbert's 24th problem asks for a "criteria of simplicity" for proofs and, more fundamentally, a way to determine the identity of proofs. Hilbert sought a theory that could distinguish between different ways of presenting the same argument versus truly distinct mathematical insights. The Normalization Thesis provides a rigorous, proof-theoretic answer to Hilbert's inquiry by using the algorithmic process of normalization as the yardstick for equivalence.

See also

References

  • Prawitz, Dag (1971). "Ideas and Results in Proof Theory". Proceedings of the Second Scandinavian Logic Symposium.
  • Martin-Löf, Per (1975). "An Intuitionistic Theory of Types: Predicative Part". Logic Colloquium '73.

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.