# Subsystems of Second Order Arithmetic and Set Theory

### Theories of (iterated) admissible sets and beyond

Since the eighties, theories of admissible sets have been studied in proof theory and have turned out to provide a useful unitary framework for classifying relevant subsystems of second order arithmetic and set theory. They also serve as a good starting point for studying stronger systems based on additional comprehension and reflection principles.### Metapredicative systems

Technically speaking, a formal system $\mathsf{T}$ is called predicatively reducible if there exists a proof-theoretic reduction of $\mathsf{T}$ to the system $\mathsf{RA}_{\lt\Gamma_0}$ of ramified analysis with levels less than $\Gamma_0$. Interestingly, however, there are also many natural theories whose proof-theoretic strength goes beyond $\Gamma_0$, but whose proof-theoretic analysis does not make use of impredicative methods (e.g. collapsing techniques); the collection of metapredicative theories comprises all those. Of course, this description of metapredicativity is informal, and therefore it would be very interesting to answer the following two questions:- Is there a formal counterpart of this informal notion?
- And if so, what is the limit of metapredicativity?

### Lifting the proof theory of second order arithmetic to theories of sets and classes

The basic question is simple: What happens if we replace Peano arithmetic and subsystems of second order arithmetic by Zermelo-Fraenkel set theory (with or without the axiom of choice) and subsystems of Morse-Kelley theory of sets and classes, respectively? Which proof-theoretic results have direct analogues and for which results do such analogues not exist? Clearly, von Neumann-Gödel-Bernays $\mathsf{NBG}$ set theory plays the role of the system $\mathsf{ACA}_0$ of arithmetic comprehension with induction restricted to sets, and there are results which show that $\Sigma^1_1$ choice over $\mathsf{NBG}$ can be characterized by iterated comprehensions, similarly to what we know from second order arithmetic. Beyond that the situation becomes more interesting.### Some References:

- Proof theory for theories of ordinals. I. Recursively Mahlo ordinals, Annals of Pure and Applied Logic 122, 2003, pp. 1-85 :
- Proof theory for theories of ordinals. II. \Pi_3-reflection, Annals of Pure and Applied Logic 129, 2004, pp. 39-92 :
- Eine beweistheoretische Untersuchung von $(\Delta^1_2\hbox{-}\mathsf{CA}) + (\mathsf{BI})$ und verwandter Systeme, Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 1982, pp. 1-22 :
- Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibioplois, Naples, 1986 :
- Reflections on reflections in explicit mathematics, Annals of Pure and Applied Logic 136(1-2), 2005, pp. 116-133 :
- Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, Journal of Symbolic Logic 66(2), 2001, pp. 935-958 :
- The proof-theoretic analysis of transfinitely iterated fixed point theories, Journal of Symbolic Logic 64(1), 1999, pp. 53-67 :
- ${Σ^1_1}$ choice in a theory of sets and classes, Ways of Proof Theory (R. Schindler - editor), Ontos Verlag, 2010, pp. 283-314 :
- Proof Theory: The first step into impredicativity, Springer, 2009 :
- Proof theory of reflection, Annals of Pure and Applied Logic 68, 1994, pp. 181-224 :
- An ordinal analysis of stability, Archive for Mathematical Logic 44, 2005, pp. 1-62 :
- An ordinal analysis of parameter free $\Pi^1_2$-comprehension, Archive for Mathematical Logic 44, 2005, pp. 263-362 :
- Wellordering proofs for metapredicative Mahlo, Journal of Symbolic Logic 67(1), 2002, pp. 260-278 :
- Autonomous fixed point progressions and fixed point transfinite recursion, Proceedings of Logic Colloquium '98 (S. Buss, P. Hajek, P. Pudlak - editors), A K Peters, 2000, pp. 449-464 :