Edit abstract data
Abstract
In 1963, G. Kreisel [5] initiated the study of formal theories
featuring inductive definitions. Later, in 1982 Feferman [4]
investigated the strength of subsystems of $ID_1$ but only special
cases ($\widehat{ID}_1$ and $ID_1^\#$) were solved. Subsystems of
the theories of iterated inductive definitions ($ID_n$) such as the
fixed point theories $\hat{ID}_n$ where investigated by Aczel and
Feferman in connection with Hancock's conjecture about the strength
of Martin-Loef type theories with universes. Another interesting type
of theory lying between $\hat{ID}_n$ and the usual $ID_n$ is $ID^*_n$.
To illustrate this in the case $n=1$, in contrast to $\hat{ID}_1$,
$ID^*_1$ has an induction principle for the fixed points but it is
restricted to formulas in which other fixed points occur only
positively. Results about the theories $ID^*_n$ were obtained by
Friedman, Feferman [4], and Cantini [2]. However, they did not settle
the proof-theoretic strength of the theories $ID^*_n$. I would like to
talk about our recent results revealing the strength of these
theories.
[1] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers and Wilfried
Sieg. Iterated inductive definitions and subsystems of Analysis:
Recent Proof-Theoretical Studies theories, Springer-Verlag, Berlin,
Heidelberg, 1981.
[2] Andrea Cantini. A note on a predicatively reducible theory of
elementary iterated induction, Bollettino U.M.I., pp. 413-430, 1985.
[3] Andrea Cantini. On the relation between choice and comprehension
principles in second order arithmetic, Journal of Symbolic Logic 51,
pp. 360--373, 1986.
[4] Solomon Feferman. Iterated inductive fixed-point theories:
Application to Hancock's conjecture, Patras Logic Symposion, pp.
171--196, North-Holland, Amsterdam, 1982.
[5] G. Kreisel. Generalized inductive definitions. Tech. rep.,
Stanford University, 1963.
[6] Michael Rathjen. Auwahl und Komprehension in Teitsystemen der
Analysis, M.Sc. thesis, University of Muenster, Germany, 1985.
[7] K. Schuette. Proof Theory, Springer-Verlag, Berlin, Heidelberg,
1977.
[8] Helmut Schwichtenberg. Proof Theory: Some Applications of
Cut-Elimination, Handbook of Mathematical Logic, pp. 868--895,
North-Holland, 1977.
[9] Stephen G. Simpson. Subsystems of Second Order Arithmetic,
Springer-Verlag, Berlin, Heidelberg, 1999.