Iteration as an Induction Principle in Explicit Mathematics

Dieter Probst

One way to increase the proof-theoretic strength of a theory is to add principles that allow to built transfinite hierarchies. Considering subsystems of second order arithmetic, dependent choice (DC) and arithmetical transfinite recursion (ATR) represent well known examples.

Systems of explicit mathematics where induction is restricted to types lack the possibility of forming types that provably constitute transfinite hierarchies. In this talk we present an axiom IT_{N} that helps to overcome this deficiency: Given an operation f that maps names on names and an arbitrary name a, one obtains a total operation g from the natural numbers into names that associates to each number n the result of the n-fold iterated application of f to a. Depending on the available type existence principles, one then can construct an initial segment of the (hyper)-jump hierarchy by means of join.

We determine the proof-theoretic ordinal of the resulting theories and motivate that IT_{N} can be regarded as an induction principle.

Address: Institut für Informatik und angewandte Mathematik, Universität Bern Neubrückstrasse 10, CH-3012 Bern, Switzerland

E-mail: probst@iam.unibe.ch