Computability in Europe 2008
Logic and Theory of Algorithms

Regular Talk:
Subsystems of Iterated Inductive Definitions

Edit abstract data

Speaker:	Bahareh Afshari
Slot:	Fri, 11:00-11:20, Room 19 (col. 5)

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.