Generalized inductive definitions

Der Mu-Kalkül ist ein System positiver und damit monotoner induktiver Definitionen, welches auch in der Informatik weite Verbreitung gefunden hat. Man kann ihn als natürliche Erweiterung von Kreisels Theorie erststufiger positiver induktiver Definitionen auffassen. Seine beweistheoretische Stärke wa...

Author: Möllerfeld, Michael
Further contributors: Pohlers, Wolfram (Thesis advisor)
Division/Institute:FB 10: Mathematik und Informatik
Document types:Doctoral thesis
Media types:Text
Publication date:2002
Date of publication on miami:11.02.2003
Modification date:14.12.2015
Edition statement:[Electronic ed.]
Subjects:Proof Theory; Generalized Recursion Theory
DDC Subject:510: Mathematik
License:InC 1.0
Language:English
Format:application/postscript
URN:urn:nbn:de:hbz:6-85659549572
Permalink:https://nbn-resolving.de/urn:nbn:de:hbz:6-85659549572
Digital documents:diss.ps

Der Mu-Kalkül ist ein System positiver und damit monotoner induktiver Definitionen, welches auch in der Informatik weite Verbreitung gefunden hat. Man kann ihn als natürliche Erweiterung von Kreisels Theorie erststufiger positiver induktiver Definitionen auffassen. Seine beweistheoretische Stärke war bisher nicht bekannt. Es stellt sich heraus, dass der Mu-Kalkül beweistheoretisch äquivalent ist zum einem Teilsystem der Zahlentheorie zweiter Stufe, welches Pi-1-2-Komprehensionen erlaubt. Im Laufe einer aufwendigen wechselseitigen Reduktion zeigen wir weiter die Aquivalenz des Mu-Kalküls mit seinem nicht-monotonen Analogon, mit einer Theorie iterierter Spielquantoren, mit einem System infinitärer Logik und mit verschiedenen Systemen der Mengenlehre basierend auf Gap-Reflexion und Stabilität. Ein Kernresultat hierfür ist, dass der Mu-Kalkül die Existenz von induktiv generierten Fixpunkten beliebiger auch nicht monotoner Operatoren beweist.