Proof theory has, after a period, in which it succeeded in analysing that part of mathematics, which is actually used, made strong moves towards the final goal, the analysis of full set theory. The first step was Rathjen's analysis of the Mahlo principle and of Pi_3-reflection. Later Rathjen and shortly afterwards Arai reached a big breakthrough with the analysis of Pi^1_2-CA. However, many researchers believe that a fully satisfactory understanding is not achieved, unless constructive theories of the same strength have been found.

To develop such constructive theories and prove their equiconsistency is the object of reductive proof theory. Constructive type theory is particularly suitable as constructive theory, because its built-up is very well understood and its philosophical basis is solid. It is interesting as well for its applications, since type theory is an idealised functional programming language. However, there were doubts whether it has sufficient strength in order to be applicable in impredicative proof theory. Due to work by myself and independently by Rathjen and Griffor, it is now known that the strength of Martin-Löf's type theory is quite big and that it is therefore suitable as a constructive analogue of strong theories. Later universes in type theory corresponding to the Mahlo principle, Pi_3-reflection and, very recently, Pi_n- and Pi^1_1-reflection were discovered by myself. Type theory has now proof theoretically very strong extensions, which cover of the part of the proof theoretic scale, of which currently an ordinal analysis exist, everything but full stability.

- Preliminary version. The final (slightly changed) version has appeared in Annals of Pure and applied Logic, 92 (1998), 113 -- 159.

- Draft

- Peter Hancock,
Anton Setzer: The IO monad in dependent type theory

( Workshop on Dependent Types in Programming, Göteborg 27-28 March 1999)- Extended slides: dvi, postscript.
- Normalizing version with state-dependend IO, type checked in Half

Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Löf's type theory. It states that we may inductively define a set while simultaneously defining a function from this set into an arbitrary type by structural recursion. This extends the notion of an inductively defined set substantially and allows us to introduce universes and higher order universes (but not a Mahlo universe).

We have given a finite axiomatization of inductive-recursive definitions and shown its consistency by constructing a set-theoretic model which makes use of one Mahlo cardinal. Two preliminary versions exists:

- P. Dybjer,
(Göteborg) and
A. Setzer
A finite axiomatization of inductive-recursive definitions.
- To appear in the proceedings of TLCA'99.
- © Springer-Verlag
- See as well Lecture Notes in Computer Science
- Post-script version.

- P. Dybjer,
(Göteborg) and
Anton Setzer:
Finite axiomatizations of inductive and inductive-recursive definitions.

(Workshop on Generic Programming Marstrand, Sweden, 18 June 1998)

- A. Setzer:
Extending Martin-Löf Type Theory by one
Mahlo-Universe.
- 21pp.
- To appear in Arch. math. log.

- A. Setzer: A Model for a type theory with one Mahlo Universe, 10pp. , 1996.

Another result was the definition of a much stronger extension, the Pi_3-reflecting universe.

- A. Setzer: Rules for the Pi_3-reflecting Universe, 1998. (postscript)

Ordinal systems is an alternative presentation of ordinal notation systems in such a way, that we have intuitive well-ordering arguments. They are defined in such a way that we can transfinitely enumerate all ordinal notations by repetitively selecting out of the set of ordinals, which are denoted by using ordinals previously chosen, the least element not chosen before with respect to some (well-ordered) termination ordering. In order to guarantee the correctness of this process and that it enumerates all ordinals, the following conditions are required:

- An ordinal notation is finite and refers only to smaller ordinals.
- If alpha < beta can be denoted, then alpha is below some of the ordinals, beta is denoted from, or the denotation of alpha is with respect to the termination ordering less than the denotation of beta.
- If A is a set of ordinal notations which is well-ordered, the set of ordinals which can be denoted from ordinals in A is well-ordered with respect to the termination ordering.

It turns out that what is needed are subprocesses: Instead of choosing in the main process the next ordinal directly, at every stage we need to start a subprocess in an ordinal system, which is relativized with respect to the ordinals already denoted in the main process. Once this subprocess is complete and has enumerated all ordinals in the relativized system, we can verify that the set of ordinals denotable from the ones previously selected in the main system is well-ordered with respect to the termination ordering and we can therefore select the next ordinal. For stronger ordinal notation systems, a more complicated arrangement of such subprocesses is necessary and therefore the role of cardinals in ordinal notation systems becomes clear: they are a way of organizing these processes.

We have determined ordinal systems of the strength of admissible ordinals, recursively inaccessible ordinals, recursively Mahlo ordinals and Pi_3-reflecting ordinals. The research up to recursive inaccessible ordinals is written down.

Articles:

- In: G. Sambin and J. Smith (Ed.): Twenty-five years of constructive type theory, Clarendon Press, Oxford, pp. 245 - 263.
- Postscript-version

- In B. Cooper and J. Truss (Eds.): Sets and Proofs, Cambridge University Press, Cambridge, pp. 301 -- 331, 1999.
- Some mistakes have been detected. Here are the corrections:
- Corrections
- Corrected version of Ordinal Systems
- Postscript-version.
- Some people have problems with printing this file, therefore here is the Latex-source

- 22p.
- To appear in the Proceedings of Logic Colloquium 1998, edited by Pavel Pudlak and Sam Buss, Springer Lecture Notes in Logic.
- Postscript version

- P. Clote, A. Setzer: On PHP st-connectivity, and odd charged graphs.
- In: P. Beame, S. Buss (Eds.): Proof complexity and feasible arithemetics. DIMACS workshop April 21 - 24, 1996. American Mathematical Society, 1998, pp. 73 - 92.

- A. Setzer: Inductive definitions with decidable atomic formulas.
- In: D. van Dalen, M. Bezem (Eds.): Computer Science Logic. 10th International workshop CSL '96. Springer Lecture Notes in Computer Science, 1258, 1997, pp. 414 - 431.
- © Springer-Verlag
- See as well Lecture Notes in Computer Science
- Postscript Version

- A. Setzer: Translating set theoretical proofs into type theoretical
programs.
- In: G. Gottlob, A. Leitsch, D. Mundici (Eds.): Computational Logic and Proof Theory. 5th Kurt Gödel Colloquium, KGC' 97. Springer Lecture Notes in Computer Science, 1289, 1997, pp. 278 - 289.

Our research on ordinal systems has resulted in a very good understanding
of ordinal notation systems up to the strength of
finitary iterated inductive definitions (ID_