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: | |
---|---|
Weitere Beteiligte: | |
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.