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...

Verfasser: Möllerfeld, Michael
Weitere Beteiligte: Pohlers, Wolfram (Gutachter)
FB/Einrichtung:FB 10: Mathematik und Informatik
Dokumenttypen:Dissertation/Habilitation
Medientypen:Text
Erscheinungsdatum:2002
Publikation in MIAMI:11.02.2003
Datum der letzten Änderung:14.12.2015
Angaben zur Ausgabe:[Electronic ed.]
Schlagwörter:Proof Theory; Generalized Recursion Theory
Fachgebiet (DDC):510: Mathematik
Lizenz:InC 1.0
Sprache:English
Format:application/postscript
URN:urn:nbn:de:hbz:6-85659549572
Permalink:https://nbn-resolving.de/urn:nbn:de:hbz:6-85659549572
Onlinezugriff: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.