Research area of Anton Setzer

This Page on the Research of Anton Setzer will soon be updated

a) Area

My research area combines two fascinating and difficult areas of mathematical logic, proof theory and type theory, both of which are currently undergoing a fast development. I am particularly specialised in the definition of new proof theoretically strong, predicative extensions of type theory and in carrying out proof theoretic analyses of them.

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.

b) Major Results obtained

The strength of Martin-Löf's Type Theory with W-type and one Universe

This was work of my PhD-thesis, in which the precise strength of that theory was determined, a problem which was open for a long time. The lower bound was shown by directly carrying out well-ordering proofs in type theory. It is due to these results (and similar ones by Rathjen and Griffor) that type theory is now considered as of great importance in proof theory, because they show that type theory has sufficient strength to be able to carry in principal out all ordinary mathematical proofs. This research can be found as well in the following article and draft:
  • A. Setzer: Well-ordering proofs for Martin-Löf Type Theory with W-type and one Universe.
  • A. Setzer: An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe , 33pp, 1996.

    Interactive Programs in Type Theory

    This research is a real application of proof theoretic knowledge about strong principles, in this case the W-type, to computer science. The question was how to introduce interactive programs in dependent type theory and formulate the IO-monad. Peter Hancock and myself found a quite satisfying solution. It led to the clarification of the role of the parameters input, output in programs. Further we could formulate while- and repeat-loops and a new concept of redirection, which allows to refine high level interactive programs by low level programs for the commands contained in them.

    A finite axiomatization of inductive recursive definitions

    This is joint work with Peter Dybjer, (Göteborg).

    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:

    We are currently writing on an improved version of it.

    Mahlo Universe and Pi_3-reflection

    After the determination of the strength of ordinary type theory, the question was whether it could be extended to cover the strength of a recursively Mahlo ordinal. This question was answered positively by the definition of the Mahlo universe. With the Mahlo universe a new paradigm for the definition of sets, the Mahlo-principle, was added to type theory. The Mahlo universe led to long discussions among type and proof theorists about, whether the Mahlo universe can be considered as predicative. One result of these discussions was the discovery of the data type of inductive recursive definitions (see below).
    Another result was the definition of a much stronger extension, the Pi_3-reflecting universe.

    Pi_n-, Pi_alpha- and Pi^1_1-reflection

    During visits of Rathjen in Leeds, England and Arai in Hiroshima, Japan, this year I developed universes, which reach the strength of Pi_n-, Pi_alpha- and Pi^1_1-reflection, principles which are already ordinal theoretically analysed, but proofs of which exist only in the form of preprints. In order to show that they really are as strong as conjectured, well-ordering proofs have to be carried out. I am currently working out the details for them. With these universes, the area of reflection principles is exhausted; future universes need to cover the notion of stability.

    Ordinal Systems

    Since Gentzen's analysis of Peano Arithmetic, one goal in proof theory has been the reduction of the consistency of mathematical theories to the well-ordering of ordinal notation systems. In the case of Gentzen's system and slight extensions the well-ordering of the systems used is quite intuitive. Stronger ordinal notation systems are usually developed by using cardinals, large cardinals or their recursive analogues and the main intuition is developed from set theory. Therefore they are no longer as intuitively well-ordered as the weaker systems, an obstacle for the understanding of such systems for non-specialists.

    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 system is elementary, if the above condition can be verified in primitive arithmetic, and elementary ordinal systems reach all ordinals below the Bach-mann-Howard ordinal. In order to get beyond this bound, the analogue of cardinals in this approach is needed.

    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:

  • A. Setzer: An introduction to well-ordering proofs in Martin-Löf's type theory.
  • A. Setzer: Ordinal systems.
  • A. Setzer: Ordinal systems part 2: One inaccessible.

    Other Results

    Complexity Theory of Propositional Proof Systems

    This was research with P. Clote in Munich. We investigated Degen's extension of the pigeon\-hole-principle and succeeded in showing that the resulting hierarchy collapses. Further we could give another example (so called st-connectivity) for the fact that tree-like resolution does not polynomially simulate ordinary resolution.

    Extensionality vs. Intensionality

    We have shown that in (finitary) type theory extended by types for inductive definitions (corresponding to the ID_n) without equality the addition of an extensional equality yields a conservative extension. This is done by defining an extensional equality explicitly.

    Extracting programs from set theoretical proofs

    The well-ordering proofs I have given show transfinite induction up to large ordinals. This allows as well, to prove cut elimination for certain fragments of set theory. It is well-known, that from the existence of a cut free proofs of a Pi^0_2-sentence phi in Martin-Löf's Type Theory follows in principal phi. For the new technique for carrying out cut elimination - Buchholz' H-controlled derivations - it was not clear, how to achieve this result. A solution for this problem can be found in which should work for stronger sytems as well. (There is a different and very elegant approach by Buchholz). Therefore, all Pi^0_2-sentences provable in the corresponding classical set theory are provable in Martin-Löf's Type Theory.

    Free Algebras for Iterated Inductive Definitions.

    As part of the research of the group in Munich on proof assistants I have introduced a type theory without dependent types having the strength of finitely iterated inductive definitions. This was an extension of free algebras studied in computer science by allowing infinite branching. I have analysed it proof theoretically by giving an extremely simple well ordering proof. Further I was able to introduce an equality based on decidable prime formulas only and to show that its extensional version is for formulas of level $\leq 1$ conservative over the intensional one, extending an old result by R. Gandy. This allows the use of the machinery implemented in the theorem prover MINLOG in Munich for extracting programs from classical proofs for these theories with full extensionality.

    Bounds for provable recursive functions

    In my Diplomarbeit (MSc-thesis), which contains original work, I have analysed a denotation system for ordinals and used them together with a modified technique to get bounds for the provable Pi^0_2-sentences and therefore limits for all programs, for which we can prove termination in Peano Arithmetic.

    c) Current research

    Full analysis of the Pi_n and Pi^1_1-reflecting universes

    The Pi_n and Pi^1_1-reflecting universes are yet only partially analysed. We are working on proofs for this.

    A Pi^1_2-proof for Ordinal Systems beyond Pi_1^1-CA

    This is joint work with Herman Jervell, Oslo.

    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_omega). It was difficult to get an intuitive understanding of ordinal systems for this strength. We have recently found a proof for their well-ordering based on Girard's Pi^1_2-logic. This proof is relative intuitive.

    Extending type theory beyond Pi^1_1-reflection

    There is a substantial boundary for extending type theory beyond Pi^1_1-reflection. However, we have some approaches which seem to cross that border and are investigating, whether they will lead to extensions which go substantially byond it. The big current goal is currently to reach the strength of Pi^1_2-CA in predicatively justified type theory.

    Extending ordinal systems beyond Pi_3-reflection

    This is a natural extension of the above research. Unfortunately the literature in this area is not very well developed yet (Drafts by Toshiyasu Arai, Hiroshima and Michael Rathjen, Leeds).

    d) Publications and Drafts

    A list of publications and drafts can be found here.