Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory

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


Until the 1970s, proof theoretic investigations were mainly concerned with theories of inductive definitions, subsystems of analysis and finite type systems. With the pioneering work of Gerhard Jäger in the late 1970 s and early 1980s, the focus switched to set theories, furnishing ordinal-theoretic proof theory with a uniform and elegant framework. More recently it was shown that these tools can even sometimes be adapted to the context of strong axioms such as the powerset axiom, where one does not attain complete cut elimination but can nevertheless extract witnessing information and characterize the strength of the theory in terms of provable heights of the cumulative hierarchy. Here this technology is applied to intuitionistic Kripke-Platek set theories \(\mathbf{IKP }({\mathcal {P}})\) and \(\mathbf{IKP }({\mathcal {E}})\), where the operation of powerset and exponentiation, respectively, is allowed as a primitive in the separation and collection schemata. In particular, \(\mathbf{IKP }({\mathcal {P}})\) proves the powerset axiom whereas \(\mathbf{IKP }({\mathcal {E}})\) proves the exponentiation axiom. The latter expresses that given any sets A and B, the collection of all functions from A to B is a set, too. While \(\mathbf{IKP }({\mathcal {P}})\) can be dealt with in a similar vein as its classical cousin, the treatment of \(\mathbf{IKP }({\mathcal {E}})\) posed considerable obstacles. One of them was that in the infinitary system the levels of terms become a moving target as they cannot be assigned a fixed level in the formal cumulative hierarchy solely based on their syntactic structure. As adumbrated in an earlier paper, the results of this paper are an important tool in showing that several intuitionistic set theories with the collection axiom possess the existence property, i.e., if they prove an existential theorem then a witness can be provably described in the theory, one example being intuitionistic Zermelo-Fraenkel set theory with bounded separation.


Ordination Analysis Intuitionistic Power Powerset Axiom Proof-theoretic Ordinals Existential Dimension 
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.



The work of the second author was supported by a Leverhulme Research Fellowship and the Engineering and Physical Sciences Research Council under grant number EP/K023128/1.


  1. 1.
    P. Aczel, M. Rathjen, Notes on constructive set theory, Technical Report 40, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences, Stockholm, 2001).
  2. 2.
    P. Aczel, M. Rathjen, Constructive set theory, book draft (2010)Google Scholar
  3. 3.
    T. Arai, Proof theory for theories of ordinals II: \(\Pi _3\)-Reflection. Ann. Pure Appl. Log. 129, 39–92 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    J. Barwise, Admissible Sets and Structures (Springer, Berlin, 1975)CrossRefzbMATHGoogle Scholar
  5. 5.
    M. Beeson, Foundations of Constructive Mathematics (Springer, Berlin, 1985)CrossRefzbMATHGoogle Scholar
  6. 6.
    W. Buchholz, A new system of proof-theoretic ordinal functions. Ann. Pure Appl. Log. 32, 195–207 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    W. Buchholz, A simplified version of local predicativity, in Leeds Proof Theory 1991, ed. by P. Aczel, H. Simmons, S. Wainer (Cambridge University Press, Cambridge, 1993), pp. 115–147Google Scholar
  8. 8.
    J. Cook, Ordinal Analysis of Set Theories; Relativised and Intuitionistic. Ph.D. thesis University of Leeds, 2015Google Scholar
  9. 9.
    H. Friedman, Countable models of set theories, in Cambridge Summer School in Mathematical Logic, vol. 337, Lectures Notes in Mathematics, ed. by A. Mathias, H. Rogers (Springer, Berlin, 1973), pp. 539–573CrossRefGoogle Scholar
  10. 10.
    H. Friedman, S. Ščedrov, The lack of definable witnesses and provably recursive functions in intuitionistic set theory. Adv. Math. 57, 1–13 (1985)CrossRefzbMATHGoogle Scholar
  11. 11.
    G. Jäger, Beweistheorie von KPN. Arch. Math. Logik 2, 53–64 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    G. Jäger, Zur Beweistheorie der Kripke-Platek Mengenlehre über den natürlichen Zahlen. Arch. Math. Logik 22, 121–139 (1982)CrossRefzbMATHGoogle Scholar
  13. 13.
    G. Jäger, Iterating admissibility in proof theory, in Proceedings of the Herbrand Logic Colloquium’81, by ed. J. Stern (North-Holland, Amsterdam, 1982), pp. 137–146Google Scholar
  14. 14.
    G. Jäger, Theories for Admissible Sets: A Unifying Approach to Proof Theory (Bibliopolis, Naples, 1986)zbMATHGoogle Scholar
  15. 15.
    G. Jäger, W. Pohlers, Eine beweistheoretische Untersuchung von \({\varvec {\Delta }}^{ 1}_{ 2}\)-\({\mathbf{CA}}+{\mathbf{BI}}\) und verwandter Systeme (Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse, 1982)Google Scholar
  16. 16.
    W. Pohlers, Subsystems of set theory and second order number theory, in Handbook of Proof Theory, ed. by S. Buss (Elsevier Science B.V., 1998), pp. 209–335Google Scholar
  17. 17.
    M. Rathjen, Unpublished Lecture Notes on Proof Theory (Ohio State University, 1993)Google Scholar
  18. 18.
    M. Rathjen, How to develop proof-theoretic ordinal functions on the basis of admissible ordinals. Math. Log. Q. 39, 47–54 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    M. Rathjen, Proof theory of reflection. Ann. Pure Appl. Log. 68, 181–224 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    M. Rathjen, The realm of ordinal analysis, in Sets and Proofs, ed. by S.B. Cooper, J.K. Truss (Cambridge University Press, 1999), pp. 219–279Google Scholar
  21. 21.
    M. Rathjen, S. Tupailo, Characterizing the interpretation of set theory in Martin-Löf type theory. Ann. Pure Appl. Log. 141, 442–471 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    M. Rathjen, The disjunction and other properties for constructive Zermelo-Fraenkel set theory. J. Symb. Log. 70, 1233–1254 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    M. Rathjen, An ordinal analysis of parameter-free \(\Pi ^1_2\) comprehension. Arch. Math. Log. 44, 263–362 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    M. Rathjen, Metamathematical properties of intuitionistic set theories with choice principals, in New Computational Paradigms: Changing Conceptions of What is Computable, ed. by S.B. Cooper, B. Löwe, A. Sorbi (Springer, New York, 2008), pp. 287–312CrossRefGoogle Scholar
  25. 25.
    M. Rathjen, From the weak to the strong existence property. Ann. Pure Appl. Log. 163, 1400–1418 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    M. Rathjen, Constructive Zermelo-Fraenkel set theory, power set, and the calculus of constructions, in Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, ed. by P. Dybjer, S. Lindström, E. Palmgren, G. Sundholm (Springer, Heidelberg, 2012), pp. 313–349CrossRefGoogle Scholar
  27. 27.
    M. Rathjen, Relativized ordinal analysis: the case of Power Kripke-Platek set theory. Ann. Pure Appl. Log. 165, 316–393 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    M. Rathjen, The existence property for intuitionistic set theories with collection. In preparationGoogle Scholar
  29. 29.
    K. Schütte, Proof Theory (Springer, Berlin, 1977)CrossRefzbMATHGoogle Scholar
  30. 30.
    A.W. Swan, CZF does not have the existence property. Ann. Pure Appl. Log. 165, 1115–1147 (2014)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Pure MathematicsUniversity of LeedsLeedsUK

Personalised recommendations