Logik höherer Stufe

Jan Burse, erstellt 08. Feb 2010 Nachdem wir nun alles bereit haben, das Verkaufssystem, die Einrichtungsprogramme und das Produkt, ist der Punkt gekommen wo wir daran denken sollten, die Dokumentation für das Produkt zu schreiben. Benutzerhandbücher, Referenzdokumente, Datenblätter und Fachartikel stehen auf dem Plan. Das bedeutet noch einmal genauer auf die Grundlagen des Produktes, den Kontext des Produktes und die Absicht des Produktes einzugehen. Die Idee war einfach, wir wollten der Arbeitsweise eines Prolog Interpreters eine frische Grundlage verpassen. Das Ergebnis war fatal. Es lief darauf heraus dass ich einige nicht verrechenbare Monate verbracht habe. Als eine Regel bleibt Grundlagenforschung unbezahlt. Was war die Stimme, die mich hier gerufen hat? Es war die Versuchung von Produktverbesserungen und neuen Richtungen der Produktentwicklung. Es führte dazu dass ich mich in das Dunkel der nicht klassischen Logiken und der Logiken höherer Ordnung begab. Geistige Vorbehalte dass kein Nutzen aus solchen Logiken gezogen werden kann waren da. Was kann schon vorliegen, das nicht schon mit Prädikatenlogik erster Ordnung erreicht werden kann? Aber wir wollten auf der einen Seite tiefere Einsichten in Parakonsistenz und auf der anderen Seite in Alternativen zur Mengentheorie gewinnen. Deshalb konnten wir der Versuchung nicht widerstehen. Langsam wichen die geistigen Vorbehalte Methoden um mit nicht klassischen und Logiken höherer Ordnung umzugehen. Wir können Nichtstandardlogiken als schwächere Formen der entsprechenden Standardlogiken oder Standardtheorien betrachten. Typischerweise bedeutet das, dass die Nichtstandardlogiken über einen weitere Menge an Modellen verfügen. Weil nun Gültigkeit bedeutet dass eine Formel in jedem Model erfüllt wird, können wir folgenden Schluss ziehen. Wenn wir mit Gültigkeit arbeiten können wir sicher von Nichtstandardlogik zu Standardlogik und/oder Standardtheorie über gehen, aber nicht notwendigerweise umgekehrt. Das bedeutet dass eine konservative Formel die in Nichtstandardlogik gültig ist, auch in der Standardlogik und/oder Standardtheorie gültig ist. Wir dürfen aber nicht der Täuschung verfallen und erwarten dass eine in der Standardlogik und/oder Standardtheorie gültige Formel auch in der Nichtstandardlogik gültig ist. Also liefen wir los, indem wir zuerst eine Arbeit vervollständigten die wir schon drei Jahre zuvor begonnen hatten. Diese Arbeit war über nicht klassische Prädikatenlogiken, und sie zeigte einen netten Rahmen um verschiedene Logiken basierend auf Minimallogik zu studieren. Wir konnten schon parakonsistente Logik, paravollständige Logik und klassische Logik in Beziehung setzen. Leider war das verwendet Fragment in Bezug auf seine Konnektiven und Quantoren sehr arm. Es verfügte nur über Implikation und Füralle. Deshalb verwendeten wir etwas Zeit dazu um eine Fusion und einen Existentiellentyp hinzufügen. Jede Prolog Anfrage ist eine existentielle Frage an eine Fusion von Zielen. Wir mussten deshalb recherchieren. Als nächstes begannen wir damit den Begriff eines Prologterms zu erweitern. Wieso soll man nicht Variablen in der Position eines Funktors erlauben? Die Antwort kam schnell, wir müssen vorsichtig sein, wenn wir z.B. Terme wie F(F) formen, Russells Paradox lauert. Deshalb mussten wir unseren Rahmen in Richtung Typentheorie erweitern, indem wir Gattungen einführten, die für Familien von Formeln stehen. Entsprechende Formierungsregeln können dann Russells Paradox ausschliessen. Wenn wir ausserdem Lambdaausdrücke und neue Inferenzregeln erlauben, dann bekommen wir Aussonderung umsonst. Ein guter Moment war gekommen, um inne zu halten und um unsere Ergebnisse mit etwas in Beziehung zu setzen was wir schon 15 Jahre zuvor erkundet hatten. Zu dieser Zeit haben wir gezeigt dass hierarchische Logikprogramme ein Model haben. Unser Ergebnis machte freien Gebrauch der Mengentheorie ohne darauf zu achten welche Teiltheorie genau benutzt wird und ob diese Konsistent ist. Diesmal können wir auf sicher sagen dass hierarchische Logikprogramme konsistent sind und wir wissen auch dass ein wichtiger Begriff die Aussonderung ist. Dieser Begriff steht auch in nicht klassischen und Logiken höherer Ordnung zur Verfügung. Unglücklicherweise werden wir wieder und wieder laufen müssen da hierarchische Logikprogramme nur der Anfang sind.

Kommentare