Advertisement

# Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory

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

## Abstract

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.

## Keywords

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.

## References

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). http://www.ml.kva.se/preprints/archive2000-2001.php
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)
4. 4.
J. Barwise, Admissible Sets and Structures (Springer, Berlin, 1975)
5. 5.
M. Beeson, Foundations of Constructive Mathematics (Springer, Berlin, 1985)
6. 6.
W. Buchholz, A new system of proof-theoretic ordinal functions. Ann. Pure Appl. Log. 32, 195–207 (1986)
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–573
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)
11. 11.
G. Jäger, Beweistheorie von KPN. Arch. Math. Logik 2, 53–64 (1980)
12. 12.
G. Jäger, Zur Beweistheorie der Kripke-Platek Mengenlehre über den natürlichen Zahlen. Arch. Math. Logik 22, 121–139 (1982)
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)
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)
19. 19.
M. Rathjen, Proof theory of reflection. Ann. Pure Appl. Log. 68, 181–224 (1994)
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)
22. 22.
M. Rathjen, The disjunction and other properties for constructive Zermelo-Fraenkel set theory. J. Symb. Log. 70, 1233–1254 (2005)
23. 23.
M. Rathjen, An ordinal analysis of parameter-free $$\Pi ^1_2$$ comprehension. Arch. Math. Log. 44, 263–362 (2005)
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–312
25. 25.
M. Rathjen, From the weak to the strong existence property. Ann. Pure Appl. Log. 163, 1400–1418 (2012)
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–349
27. 27.
M. Rathjen, Relativized ordinal analysis: the case of Power Kripke-Platek set theory. Ann. Pure Appl. Log. 165, 316–393 (2014)
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)
30. 30.
A.W. Swan, CZF does not have the existence property. Ann. Pure Appl. Log. 165, 1115–1147 (2014)

## Copyright information

© Springer International Publishing Switzerland 2016

## Authors and Affiliations

1. 1.Department of Pure MathematicsUniversity of LeedsLeedsUK