Skip to main content
SpringerLink
Log in
Book cover

Advances in Proof Theory pp 319–338Cite as

Birkhäuser

From Subsystems of Analysis to Subsystems of Set Theory

  • Chapter
  • First Online:

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

Abstract

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.

Dedicated to Gerhard Jäger on the occasion of his 60th birthday

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In case that \(\phi \) is a sentence not containing free variables, the calculus is just a verification of \(\phi \) in the structure \(\mathbb {N}\). Details about semi–formal systems in general and the verification calculus together with a proof of Theorem 2.1 can be found in [34].

  2. 2.

    This formulation is quite different from Gentzen’s approach who did not use infinitary logic. However, the idea of the proof is the same. In our formulation Gentzen’s result says that \(\omega ^\alpha \) is an upper bound for the order–type of \(\prec \). A result that sufficed to obtain the proof theoretic ordinal for Peano Arithmetic. Already Schütte improved Gentzen’s result in showing that the order–type of \(\prec \) is \(\le \omega \mathrel {\cdot }\alpha \) (cf. [38] Theorem 23.1).

  3. 3.

    I concentrate on the computation of upper bounds, since only there meta–mathematical methods are needed. Lower bounds are obtained by exhausting the mathematical power of an axiom system.

  4. 4.

    Again the formulation deviates considerably from Gentzen’s original theorem. He did not use infinitary derivations but obtained the result by a complicated assignment of ordinals to the nodes in a finite derivation.

  5. 5.

    In Sect. 3.3 I will briefly comment on Hilbert’s Programme.

  6. 6.

    There are variations of the comprehension scheme, e.g., choice schemata, and even stronger systems such as the system \(\textsf {ATR}_0\) of arithmetical transfinite recursion (cf. [39]) which can also be embedded into Ramified Analysis but this is inessential for our story.

  7. 7.

    Actually the system in my dissertation was weaker than Takeuti’s. The ordinal of the full system was not available in \(\Sigma \).

  8. 8.

    When formulating such rules I tacitly assume \(\alpha <\beta \). I mention the side formula \(\chi \) just to be not too severely cheating. A rigid definition is preferably done in the framework of some form of sequent calculus.

  9. 9.

    This is my naming to emphasize the relationship to the hyperjump operation.

  10. 10.

    Der Physiker verlangt gerade von einer Theorie, dass ohne die Heranziehung von anderweitigen Bedingungen aus den Naturgesetzen oder Hypothesen die besonderen Sätze allein durch Schlüsse, also auf Grund eines reinen Formelspiels abgeleitet werden. Nur gewisse Kombinationen und Folgerungen der physikalischen Gesetze können durch Experimente kontrolliert werden—so wie in meiner Beweistheorie nur die realen Aussagen unmittelbar einer Verifikation fähig sind. (Cited from [18]).

  11. 11.

    Here it is necessary to allow additional number parameters in \(\Pi ^0_2\)–sentences. A more elaborated discussion on the interaction of Hilbert’s programme and ordinal analysis will appear in [33].

  12. 12.

    Das Operieren mit dem Unendlichen kann nur durch das Endliche gesichert werden [17].

  13. 13.

    This, of course, does not mean that these rules are dubious. Contrarily I think that the power of these ingenious rules, especially in respect to second order systems, should be more extensively studied.

  14. 14.

    This is probably the right place to mention that Moschovakis’ book [25] was of central importance for the proof theoretic study of inductive definition.

  15. 15.

    For a rigid proof cf. [32].

  16. 16.

    A bound that in general is useless for proof theoretic studies.

  17. 17.

    In former publications I sometimes talked about “virtual ordinals”.

  18. 18.

    To find the subsets of the class of ordinals with the adequate gaps is actually the most challenging task in the ordinal analysis of strong axiom systems.

  19. 19.

    A proof of this theorem (in a more modern form working already with operator controlled derivations which will be mentioned below) is in [32] Lemma 9.4.5.

  20. 20.

    Which says in its simplest form that for every \(\Sigma ^1_1\)–definable set M of well-orderings there is an ordinal \(\xi <\omega ^{ck}_1\) that bounds the order–types of the well–orderings in M. A fact which actually is a consequence of the Boundedness Theorem 2.2. Cf. [2].

  21. 21.

    During the preparation of this article I received a preprint by Kentaro Sato “A new model construction by making a detour via intutionistic theories. II: Interpretability lower bounds for Feferman’s explicit mathematics \(T_0\)” in which he establishes the equivalence without use of ordinal analysis.

References

  1. J. Barwise, Admissible Sets and Structures, Perspectives in Mathematical Logic (Springer, Berlin, 1975)

    Book  MATH  Google Scholar 

  2. A. Beckmann, W. Pohlers, Application of cut-free infinitary derivations to generalized recursion theory. Ann. Pure Appl. Logic 94, 1–19 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  3. B. Blankertz, Beweistheoretischen Techniken zur Bestimmung von \(\Pi ^0_2\)–Skolem Funktionen, Dissertation, Westfälische Wilhelms-Universität, Münster, 1997

    Google Scholar 

  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)

    MATH  Google Scholar 

  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–233

    Chapter  Google Scholar 

  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–147

    Google Scholar 

  7. W. Buchholz, Explaining the Gentzen-Takeuti reduction steps: a second order system. Arch. Math. Logic 40, 37–59 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  8. W. Buchholz, E.A. Cichon, A. Weiermann, A uniform approach to fundamental sequences and hierarchies. Math. Logic Q. 40, 273–286 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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. S. Feferman, Systems of predicative analysis. J. Symbol. Logic 29, 1–30 (1964)

    Article  MathSciNet  MATH  Google Scholar 

  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–326

    Google Scholar 

  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–32

    Google Scholar 

  14. H.M. Friedman, Set theoretic foundations for constructive analysis. Ann. Math. 105, 1–28 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  15. G. Gentzen, Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann. 119, 140–161 (1943)

    Article  MathSciNet  MATH  Google Scholar 

  16. L. Henkin, A generalization of the notion of \(\omega \)-consistency. J. Symb. Logic 19, 183–196 (1954)

    Article  MathSciNet  MATH  Google Scholar 

  17. D. Hilbert, Über das Unendliche. Math. Ann. 95, 161–190 (1926)

    Article  MathSciNet  MATH  Google Scholar 

  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. W.A. Howard, A system of abstract constructive ordinals. J. Symb. Logic 37, 355–374 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  20. G. Jäger, Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis, Dissertation, Ludwig-Maximilians-Universität, Munich, 1979

    Google Scholar 

  21. G. Jäger, Beweistheorie von KPN. Archiv für Mathematische Logik und Grundlagenforschung 20, 53–63 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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. 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–28

    Google Scholar 

  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)

    MATH  Google Scholar 

  26. S. Orey, On \(\omega \)-consistency and related properties. J. Symb. Logic 21, 246–252 (1956)

    Article  MathSciNet  MATH  Google Scholar 

  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–289

    Google Scholar 

  28. W. Pohlers, Ordinals connected with formal theories for transfinitely iterated inductive definitions. J. Symb. Logic 43, 161–182 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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–357

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  32. W. Pohlers, Proof Theory: The First Step into Impredicativity, Universitext (Springer, Berlin/Heidelberg/New York, 2009)

    MATH  Google Scholar 

  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. 32

    Google Scholar 

  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–232

    Google Scholar 

  35. M. Rathjen, Eine Ordinalzahlanalyse der \({\Pi }_3\)-Reflexion (Westfälische Wilhelms-Universität, Münster, Habilitationsschrift, 1992)

    Google Scholar 

  36. M. Rathjen, An ordinal analyis of parameter free \({\Pi }_2^1\)-comprehension. Arch. Math. Logic 48(3), 263–362 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  38. K. Schütte, Proof Theory, Grundlehren der Mathematischen Wissenschaften, vol. 225 (Springer, Heidelberg/New York, 1977)

    Google Scholar 

  39. S.G. Simpson, Subsystems of Second Order Arithmetic (Springer, Berlin/Heidelberg/New York, 1999)

    Book  MATH  Google Scholar 

  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, 2011

    Google Scholar 

  41. G. Takeuti, Consistency proofs of subsystems of classical analysis. Ann. Math. 86, 299–348 (1967)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für math. Logik und Grundlagenforschung, Westfälische Wilhelms-Universität, Münster, Germany

    Wolfram Pohlers

Authors
  1. Wolfram Pohlers
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wolfram Pohlers .

Editor information

Editors and Affiliations

  1. Campus de Caparica DM FCT, Univ Nova de Lisboa, Caparica, Portugal

    Reinhard Kahle

  2. Inst.of Computer Sci. applied math., University of Bern, Bern, Switzerland

    Thomas Strahm

  3. Institute of Computer Science and A, University of Berne, Berne, Switzerland

    Thomas Studer

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Pohlers, W. (2016). From Subsystems of Analysis to Subsystems of Set Theory. In: Kahle, R., Strahm, T., Studer, T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-29198-7_9

Download citation

Publish with us

Policies and ethics

Search

Navigation