A note on iterated consistency and infinite proofs

  • Anton FreundEmail author


Schmerl and Beklemishev’s work on iterated reflection achieves two aims: it introduces the important notion of \(\varPi ^0_1\)-ordinal, characterizing the \(\varPi ^0_1\)-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the \(\varPi ^0_1\)-ordinals for a range of theories. The present note demonstrates that these achievements are independent: we read off \(\varPi ^0_1\)-ordinals from a Schütte-style ordinal analysis via infinite proofs, in a direct and transparent way.


Iterated consistency Ordinal analysis \(\varPi ^0_1\)-ordinal Infinite proofs \(\omega \)-rule Cut elimination 

Mathematics Subject Classification

03F05 03F25 03F15 03B30 03F30 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Beklemishev, L.: Proof-theoretic analysis by iterated reflection. Arch. Math. Logic 42(6), 515–552 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Buchholz, W.: Notation systems for infinitary derivations. Arch. Math. Logic 30, 277–296 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Fairtlough, M., Wainer, S.S.: Hierarchies of provably recursive functions. In: Buss, S. (ed.) Handbook of Proof Theory, pp. 149–207. Elsevier, New York (1998)CrossRefGoogle Scholar
  4. 4.
    Kreisel, G., Lévy, A.: Reflection principles and their use for establishing the complexity of axiomatic systems. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 14, 97–142 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Schmerl, U.R.: A fine structure generated by reflection formulas over primitive recursive arithmetic. In: Boffa, M., van Dalen, D., MacAloon, K. (eds.) Logic Colloquium ‘78, pp. 335–350. North Holland, New York (1979)Google Scholar
  6. 6.
    Schmerl, U.R.: Iterated reflection principles and the \(\omega \)-rule. J. Symb. Logic 47(4), 721–733 (1982)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Fachbereich MathematikTechnische Universität DarmstadtDarmstadtGermany

Personalised recommendations