On the constructive content of proofs [Elektronische Ressource] / vorgelegt von Monika Seisenberger

On the Constructive Content of ProofsMonika SeisenbergerMun¨ chen 2003On the Constructive Content of ProofsMonika SeisenbergerDissertationan der Fakult¨at fur¨ Mathematik und Informatikder Ludwig–Maximilians–Universit¨at Munc¨ henvorgelegt vonMonika SeisenbergerM¨arz 2003Erstgutachter: Prof. Dr. H. SchwichtenbergZweitgutachter: Prof. Dr. W. BuchholzTag der mundlic¨ hen Prufung:¨ 10. Juli 2003AbstractThis thesis aims at exploring the scopes and limits of techniques for extract-ing programs from proofs. We focus on constructive theories of inductivedefinitions and classical systems allowing choice principles. Special emphasisis put on optimizations that allow for the extraction of realistic programs.Our main field of application is infinitary combinatorics. Higman’s Lemma,having an elegant non-constructive proof due to Nash-Williams, constitutesan interesting case for the problem of discovering the constructive contentbehind a classical proof. We give two distinct solutions to this problem. First,we present a proof of Higman’s Lemma for an arbitrary alphabet in a theoryof inductive definitions. This proof may be considered as a constructivecounterpart to Nash-Williams’ minimal-bad-sequence proof. Secondly, usinga refinedA-translation method, we directly transform the classical proof intoa constructive one and extract a program.