From Constructive Mathematicsto Computable Analysisvia the Realizability InterpretationVom Fachbereich Mathematikder Technischen Universiatt Darmstadtzur Erlangung des akademischen Grades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigteDissertationvonDipl.-Math. Peter Lietzaus MainzReferent: Prof. Dr. Thomas StreicherKorreferent: Dr. Alex SimpsonTag der Einreichung: 22. Januar 2004Tag der mundlic hen Prufung: 11. Februar 2004Darmstadt 2004D17Hiermit versichere ich, dass ich diese Dissertation selbst andig verfasst und nur dieangegebenen Hilfsmittel verwendet habe.Peter LietzAbstractConstructive mathematics is mathematics without the use of the principle of theexcluded middle. There exists a wide array of models of constructive logic. Oneparticular interpretation of constructive mathematics is the realizability interpreta-tion. It is utilized as a metamathematical tool in order to derive admissible rules ofdeduction for systems of constructive logic or to demonstrate the equiconsistency ofextensions of constructive logic. In this thesis, we employ various realizability mod-els in order to logically separate several statements about continuity in constructivemathematics.A trademark of some constructive formalisms is predicativity. Predicative logicdoes not allow the de nition of a set by quantifying over a collection of sets that theset to be de ned is a member of.