Fachbereich Informatik - Aktuell


Disputation Stephan Alexander Spahn

am Donnerstag, 25. Oktober 2018, um 12:30 Uhr in Raum A 104, Sand 1

Axiomatisations of Compositional Inductive-Recursive Definitions

Berichterstatter 1: Prof. Dr. Peter Schroeder-Heister
Berichterstatter 2: Dr. Anton Setzer

Martin-Löf type theory is a foundational theory of intuitionistic mathematics. It is formulated in natural deduction style, and thus every type is defined by several rules describing for example how it is introduced and what constitutes a proof of properties of this type. While in the original version of this theory every type had a separate collection of defining rules specific to it, it had been recog-nised by the eponymous author himself that all of these separate sets of rules follow a common schema and that it should be possible to give a single set of rules that can define all types.
To give such a single set of rules had been achieved by P. Dybjer and A. Setzer. This formalism axiomatises inductive-recursive definitions which cover not only inductive definitions of single types but also definitions of families which consist of a type defined by induction, and a function simultaneously defined by recursion on this type; this is realised by defining a (large) set (DS) of codes whose members each define one inductive-recursively defined family. A main and motivating example of a family is a universe à la Tarski. Universes had been introduced into type theory (and set theory) already much earlier to prevent paradoxes like Russell's paradox which indicates the importance of the concept, but the extension of Martin-Löf type theory by induction-recursion does not only provide a reorganisation of the theory, but also increases its proof-theoretic strength.
The dissertation focuses on the notion of compositionality of codes for inductive-recursive definitions. One perceived difference between the theory of inductive definitions and the more general theory of inductive-recursive definitions is that two inductive definitions always can be composed to form a new inductive definition while it has been unclear for some time whether – or under which conditions – the same holds true for inductive-recursive definitions.
The discussion of this problem is partitioned into three developments: Firstly, a criterion that reformulates the property of compositionality in terms of power-obejcts of codes by sets is given by showing that codes in DS are composable if and only if such powers exist for all codes. Since it remained unknown whether DS posses these powers, two new axiomatisations of induction-recursion were defined in this dissertation for which it is shown that any two codes in either of these are composable. The first new system UF can be translated into a subsystem of DS whose codes satisfy an additional uniformity condition which can also be regarded as a condition formalising which codes in DS are definable. This system is derived from the observation that certain codes in DS satisfying an uniformity condition are composable. The second new system PN contains all of DS. It is derived from a systematic analysis of the obstructions to compositionality, or equivalently of the incapacity of DS to contain powers for all codes. Consistency of both systems is shown by providing set-theoretic models in ZFC extended by suitable large cardinals.
Der Dekan