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.
- Preliminary version. The
final (slightly changed) version has appeared in Annals of Pure and applied
Logic, 92 (1998), 113 -- 159.
A. Setzer:
An upper bound for the proof theoretical strength of
Martin-Löf Type Theory with W-type and one Universe , 33pp, 1996.
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.
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.
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 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.
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.
- In: G. Sambin and J. Smith (Ed.):
Twenty-five years of constructive type theory,
Clarendon Press, Oxford, pp. 245 - 263.
- Postscript-version
A. Setzer: Ordinal systems.
- 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:
A. Setzer:
Ordinal systems part 2: One inaccessible.
- 22p.
- To appear in the Proceedings of Logic Colloquium 1998,
edited by Pavel Pudlak and Sam Buss, Springer Lecture Notes in Logic.
-
Postscript version
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.
- 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.
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
- 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.
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).
A list of publications and drafts can be found
here.
