Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

A note on Gentzen’s ordinal assignment

  • 88 Accesses

Abstract

Gentzen’s height measure of the 1938 consistency proof is a cumulative complexity measure for sequents that is measured bottom-up in a derivation. By a factorisation of the ordinal assignment a top-down ordinal assignment can be given that does not depend on information occurring below the sequent to which the ordinal is assigned. Furthermore, an ordinal collapsing function is defined in order to collapse the top-down ordinal to the one assigned by Gentzen’s own ordinal assignment. A direct definition of the factorised assignment follows as a corollary. This extraction of an ordinal collapsing function hopes to provide a formal or conceptual clarification of Gentzen’s ordinal assignment and its height-line argument.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Gentzen, G.: Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften 4, 19–44 (1938)

  2. 2.

    Mints, G.: Selected Papers in Proof Theory. Bibliopolis, Napoli (1992)

  3. 3.

    Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)

  4. 4.

    Takeuti, G.: Proof Theory: Second Edition. Dover Books on Mathematics. Dover Publications, New York (2013). First ed. 1987

Download references

Author information

Correspondence to Annika Kanckos.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Kanckos, A. A note on Gentzen’s ordinal assignment. Arch. Math. Logic 58, 347–352 (2019). https://doi.org/10.1007/s00153-018-0641-4

Download citation

Keywords

  • Relative consistency proof (03F25)
  • Normalization (03F05)
  • Ordinal notations (03F15)

Mathematics Subject Classification

  • 03F25 (Relative consistency and interpretations)
  • 03F30 (First-order arithmetic and fragments)
  • 03F05 (Cut-elimination and normal-form theorems)
  • 03F15 (Recursive ordinals and ordinal notations)