Subsystems of Second Order Arithmetic and Set Theory

Following the tradition of classical proof theory, we are interested in the proof-theoretic analysis of systems of second order arithmetic and set theory. Special emphasis is presently put on the following three topics:

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:

  • T. Arai: Proof theory for theories of ordinals. I. Recursively Mahlo ordinals, Annals of Pure and Applied Logic 122, 2003, pp. 1-85
  • T. Arai: Proof theory for theories of ordinals. II. \Pi_3-reflection, Annals of Pure and Applied Logic 129, 2004, pp. 39-92
  • G. Jäger, W. Pohlers: 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
  • G. Jäger: Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibioplois, Naples, 1986
  • G. Jäger, T. Strahm: Reflections on reflections in explicit mathematics, Annals of Pure and Applied Logic 136(1-2), 2005, pp. 116-133
  • G. Jäger, T. Strahm: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, Journal of Symbolic Logic 66(2), 2001, pp. 935-958
  • G. Jäger, R. Kahle, A. Setzer, T. Strahm: The proof-theoretic analysis of transfinitely iterated fixed point theories, Journal of Symbolic Logic 64(1), 1999, pp. 53-67
  • G. Jäger, J. Krähenbühl: ${Σ^1_1}$ choice in a theory of sets and classes, Ways of Proof Theory (R. Schindler - editor), Ontos Verlag, 2010, pp. 283-314
  • W. Pohlers: Proof Theory: The first step into impredicativity, Springer, 2009
  • M. Rathjen: Proof theory of reflection, Annals of Pure and Applied Logic 68, 1994, pp. 181-224
  • M. Rathjen: An ordinal analysis of stability, Archive for Mathematical Logic 44, 2005, pp. 1-62
  • M. Rathjen: An ordinal analysis of parameter free $\Pi^1_2$-comprehension, Archive for Mathematical Logic 44, 2005, pp. 263-362
  • T. Strahm: Wellordering proofs for metapredicative Mahlo, Journal of Symbolic Logic 67(1), 2002, pp. 260-278
  • T. Strahm: 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