From Subsystems of Analysis to Subsystems of Set Theory

Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


To honor a part of Gerhard Jäger’s contributions to proof theory we give a non technical, personally biased account of how we got from the proof theory of subsystems of Analysis to the proof theory of subsystems of set theory.


Axiom System Proof Theory Ramify Analysis Ordinal Analysis Peano Arithmetic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    J. Barwise, Admissible Sets and Structures, Perspectives in Mathematical Logic (Springer, Berlin, 1975)CrossRefzbMATHGoogle Scholar
  2. 2.
    A. Beckmann, W. Pohlers, Application of cut-free infinitary derivations to generalized recursion theory. Ann. Pure Appl. Logic 94, 1–19 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    B. Blankertz, Beweistheoretischen Techniken zur Bestimmung von \(\Pi ^0_2\)–Skolem Funktionen, Dissertation, Westfälische Wilhelms-Universität, Münster, 1997Google Scholar
  4. 4.
    B. Blankertz, A. Weiermann, How to Characterize Provably Total Functions by the Buchholz Operator Method, vol. 6, Lecture Notes in Logic (Springer, Heidelberg, 1996)zbMATHGoogle Scholar
  5. 5.
    W. Buchholz, The \({\Omega }_{\mu +1}\)-rule, in Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics, ed. by W. Buchholz, et al. (Springer, Heidelberg/New York, 1981), pp. 188–233CrossRefGoogle Scholar
  6. 6.
    W. Buchholz, A simplified version of local predicativity, in Proof Theory, eds. by P. Aczel et al. (Cambridge University Press, Cambridge, 1992), pp. 115–147Google Scholar
  7. 7.
    W. Buchholz, Explaining the Gentzen-Takeuti reduction steps: a second order system. Arch. Math. Logic 40, 37–59 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    W. Buchholz, E.A. Cichon, A. Weiermann, A uniform approach to fundamental sequences and hierarchies. Math. Logic Q. 40, 273–286 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    W. Buchholz, S. Feferman, W. Pohlers, W. Sieg (eds.), Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics (Springer, Heidelberg/New York, 1981)zbMATHGoogle Scholar
  10. 10.
    W. Buchholz, K. Schütte, Proof Theory of Impredicative Subsystems of Analysis, in Studies in Proof Theory: Monographs, vol. 2 (Bibliopolis, Naples, 1988)Google Scholar
  11. 11.
    S. Feferman, Systems of predicative analysis. J. Symbol. Logic 29, 1–30 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    S. Feferman, Formal theories for transfinite iteration of generalized inductive definitions and some subsystems of analysis, in Intuitionism and Proof Theory, Studies in Logic and the Foundations of Mathematics, ed. by A. Kino, et al. (North-Holland Publishing Company, Amsterdam, 1970), pp. 303–326Google Scholar
  13. 13.
    S. Feferman, Predicatively reducible systems of set theory, in Axiomatic Set Theory, vol. 2, ed. by D.S. Scott, T.J. Jech, Proceedings of Symposia in Pure Mathematics, vol. 13, American Mathematical Society, Providence (1974), pp. 11–32Google Scholar
  14. 14.
    H.M. Friedman, Set theoretic foundations for constructive analysis. Ann. Math. 105, 1–28 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    G. Gentzen, Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann. 119, 140–161 (1943)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    L. Henkin, A generalization of the notion of \(\omega \)-consistency. J. Symb. Logic 19, 183–196 (1954)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    D. Hilbert, Über das Unendliche. Math. Ann. 95, 161–190 (1926)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    D. Hilbert, Die Grundlagen, der Mathematik. Vortrag gehalten auf Einladung des Mathema-tischen Seminars im Juli, in Hamburg, Hamburger Mathematische Einzelschriften, vol. 5. Heft 1928, 1–21 (1927)Google Scholar
  19. 19.
    W.A. Howard, A system of abstract constructive ordinals. J. Symb. Logic 37, 355–374 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    G. Jäger, Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis, Dissertation, Ludwig-Maximilians-Universität, Munich, 1979Google Scholar
  21. 21.
    G. Jäger, Beweistheorie von KPN. Archiv für Mathematische Logik und Grundlagenforschung 20, 53–63 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    G. Jäger, A well ordering proof for Feferman’s theory T\(_0\). Archiv für Mathematische Logik und Grundlagenforschung 23, 65–77 (1983)CrossRefzbMATHGoogle Scholar
  23. 23.
    G. Jäger, Theories for Admissible Sets: A Unifying Approach to Proof Theory, vol. 2, Studies in Proof Theory, Lecture Notes (Bibliopolis, Naples, 1986)Google Scholar
  24. 24.
    G. Jäger, W. Pohlers, Eine beweistheoretische Untersuchung von (\({\Delta }^1_2-{\rm CA})+({\rm BI})\) und verwandter Systeme, Bayerische Akademie der Wissenschaften, Sitzungsberichte 1982 (1983), pp. 1–28Google Scholar
  25. 25.
    Y.N. Moschovakis, Elementary Induction on Abstract Structures, vol. 77, Studies in Logic and the Foundations of Mathematics (North-Holland Publishing Company, Amsterdam, 1974)zbMATHGoogle Scholar
  26. 26.
    S. Orey, On \(\omega \)-consistency and related properties. J. Symb. Logic 21, 246–252 (1956)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    W. Pohlers, An upper bound for the provability of transfinite induction, in \(\models \) ISILC Proof Theory Symposium, vol. 500, Lecture Notes in Mathematics, ed. by J. Diller, G.H. Müller (Springer, Heidelberg/New York, 1975), pp. 271–289Google Scholar
  28. 28.
    W. Pohlers, Ordinals connected with formal theories for transfinitely iterated inductive definitions. J. Symb. Logic 43, 161–182 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    W. Pohlers, Cut-elimination for impredicative infinitary systems I. Ordinal analysis for ID\(_1\), Archiv für Mathematische Logik und Grundlagenforschung 21, 113–129 (1981)Google Scholar
  30. 30.
    W. Pohlers, Proof-theoretical analysis of ID\(_{\nu }\) by the method of local predicativity, in Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics ed. by W. Buchholz et al. (Springer, Heidelberg/New York, 1981), pp. 261–357Google Scholar
  31. 31.
    W. Pohlers, Cut elimination for impredicative infinitary systems II. Ordinal analysis for iterated inductive definitions. Archiv für Mathematische Logik und Grundlagenforschung 22, 69–87 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    W. Pohlers, Proof Theory: The First Step into Impredicativity, Universitext (Springer, Berlin/Heidelberg/New York, 2009)zbMATHGoogle Scholar
  33. 33.
    W. Pohlers, Hilbert’s programme and ordinal analysis, in Concepts of Proof in Mathematics, Philosophy, and Computer Science, ed. by Dieter Probst, Peter Schuster (DeGryuter, 2016), p. 32Google Scholar
  34. 34.
    W. Pohlers, Semi-formal calculi and their applications, in Gentzen’s Centenary: The Quest for Consistency,ed. by R. Kahle, M. Rathjen (Springer, New York, 2015), pp. 195–232Google Scholar
  35. 35.
    M. Rathjen, Eine Ordinalzahlanalyse der \({\Pi }_3\)-Reflexion (Westfälische Wilhelms-Universität, Münster, Habilitationsschrift, 1992)Google Scholar
  36. 36.
    M. Rathjen, An ordinal analyis of parameter free \({\Pi }_2^1\)-comprehension. Arch. Math. Logic 48(3), 263–362 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    K. Schütte, Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik. Archiv für Mathematische Logik und Grundlagenforschung 7, 45–60 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    K. Schütte, Proof Theory, Grundlehren der Mathematischen Wissenschaften, vol. 225 (Springer, Heidelberg/New York, 1977)Google Scholar
  39. 39.
    S.G. Simpson, Subsystems of Second Order Arithmetic (Springer, Berlin/Heidelberg/New York, 1999)CrossRefzbMATHGoogle Scholar
  40. 40.
    J.-C. Stegert, Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles, Ph.D. thesis, Westfälische Wilhelms-Universität, Münster, 2011Google Scholar
  41. 41.
    G. Takeuti, Consistency proofs of subsystems of classical analysis. Ann. Math. 86, 299–348 (1967)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Institut für math. Logik und GrundlagenforschungWestfälische Wilhelms-UniversitätMünsterGermany

Personalised recommendations