A note on Gentzen’s ordinal assignment

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
JournalArchive for Mathematical Logic
Volume58
Issue number3-4
Pages (from-to)347-352
Number of pages6
ISSN0933-5846
DOIs
Publication statusPublished - May 2019
MoE publication typeA1 Journal article-refereed

Fields of Science

  • 611 Philosophy
  • Relative consistency proof (03F25)
  • Normalization (03F05)
  • Ordinal notations (03F15)
  • COMPLEXITY CLASSES
  • p
  • np
  • clay math institute ?
  • human rights watch ?
  • nelimarkka is unknown to me
  • allow access or wanted?
  • 111 Mathematics

Cite this