Im letzten Unterabschnitt haben wir die Axiome einer Logik des Wissens und des Glaubens besprochen. Damit ist es möglich, Aussagen über den Wissenstand eines Akteurs in einer solchen Logik abzuleiten und damit als gültig nachzuweisen.
In einer Reihe von Anwendungen möchte man nicht nur Aussagen über den Wissensstand, sondern auch Aussagen über logische Beziehungen verschiedenen Wissens, dh. über Ableitungen in einem logischen Kalkül treffen. So könnte beim Bau eines Deduktionssystems eine Option erwünscht sein, die verschiedene Ableitungen einer Aussage auf ihre Länge hin prüft und ggf. dem Anwender nur den kürzesten Beweis liefert. Die Länge ist nur das einfachste von einer Vielfalt von Vergleichsmaßen, die hierbei Verwendung finden könnten. So können in einem deduktiven Planungssystem (siehe Abschnitt 4.7) die einzelnen Aktionen unterschiedliche Kosten verursachen, die sich zudem möglicherweise aus verschiedensten Komponenten zusammensetzen. Gesucht ist dann der kostengünstigste Plan unter einer Reihe alternativer Pläne.
Ableitungen in einem Kalkül sind, aus der Sicht der Metaebene, Objekte, über die man (Meta-) Aussagen treffen, voraussetzen und erschließen kann. Hierzu muß man den Begriff einer Ableitung und alle damit zusammenhängenden Begriffe in der formalen Sprache der Metaebene definieren. Jedem Programmierer ist geläufig, wovon wir hier sprechen. Denn jedes Programm, das irgendein System realisiert, ist eine Beschreibung dieses Systems und seines Verhaltens in einer formalen Sprache auf der Metaebene, nämlich der betreffenden Programmiersprache. Statt einer Programmiersprache wollen wir als Metasprache entsprechend der in diesem Buch verfolgten Philosophie die Prädikatenlogik ins Auge fassen.
Betrachten wir der Einfachheit halber einen (Gentzen-Hilbert)
Kalkül,
der aus einer Menge logischer Axiome und dem modus ponens
als einziger Regel besteht. Daß eine Ableitung der Formel
ist, läßt sich mit einem zweistelligen Prädikatszeichen
Abl als
auf der Metaebene beschreiben.
Wie in jeder Theorie muß auch in dieser Metatheorie des betrachteten
Kalküls das Prädikat Abl mittels entsprechender Axiome
charakterisiert werden, die hier wie folgt lauten.
Diese beiden Axiomen genügen allerdings nicht für eine vollständige
Charakterisierung, da wir weiter festlegen müssen, wann zutreffen soll. Dessen Charakterisierung erfordert zudem eine
axiomatische Charakterisierung des Formelbegriffs und also auch der dafür
erforderlichen Begriffe Term, Variable, Funktions- und Prädikatszeichen.
Wir wollen die entsprechenden Axiome nicht im einzelnen aufschreiben. Die
beiden angegebenen Axiome sollten dem Leser deutlich gemacht haben, wie man
hier im Detail vorzugehen hat. Sie sollten auch illustriert haben, daß
eine solche Formalisierung reine Routinearbeit darstellt, da wir dabei nichts
anderes tun, als die üblichen, von Logiklehrbüchern bekannten Definitionen
von deren Formulierung in halbnatürlicher Form in logische Form zu
übertragen, was wegen der Natürlichkeit des Logikformalismus nach einiger
Übung spielerisch
von der Hand geht.
Wir gehen nun also davon aus, daß das Prädikat Abl
vollständig axiomatisch charakterisiert sei. In gleicher Weise können wir
annehmen, daß zB. der Begriff der Länge einer Ableitung ,
sagen wir, in Form einer Funktion
definiert sei. Dann ist
es in einfacher Weise möglich, die eingangs erwähnte Option für ein
Beweisverfahren wie folgt zu verwirklichen.
Hierbei haben wir Print als ein eingebautes Prädikat angenommen. Dieses kleine Beispiel sollte lediglich demonstrieren, in welch einfacher Weise es möglich ist, auf der Metaebene über Ableitungen Aussagen zu formulieren und daraus Schlüsse zu ziehen.
Es gibt mehrere Anwendungen für das soeben eingeführte Prädikat Abl. In [KK91] wird dieses Prädikat als Wissens- und Glaubensoperator innerhalb von PROLOG verwandt. Die wichtigste Anwendung des so demonstrierten Schließens auf der Metaebene ist jedoch die zur Verwirklichung der bereits in der Einleitung zu diesem Abschnitt genannten Selbstreflexivität. Sie besagt, daß man im Denken und Handeln von Zeit zu Zeit innehält und über das bisher Erreichte reflektiert. In diesem Sinne möchte man auch ein Inferenzsystem so konzipieren, daß es sein eigenes Verhalten beobachtet und für das weitere Vorgehen daraus Schlüsse zieht.
Ein solches System wird auf zwei Ebenen operieren. Einerseits ist es ein System, das in der üblichen Weise Schlüsse aus dem gegebenen Wissen zieht. Systeme von dieser Art haben wir, jedenfalls im Hinblick auf ihre zugrundeliegenden Mechanismen, in diesem Buch eine ganze Reihe kennengelernt. Zusätzlich nehmen wir nach dem eben Gesagten nun noch an, daß das System auch Aussagen über die von ihm gemachten Ableitungen machen und diese dann im weiteren Verlauf entsprechend steuern kann. Mit anderen Worten, es muß die vorher demonstrierte Formalisierung von Ableitungen auf der Metaebene im System integriert sein.
Ein Ableitungsschritt auf der Objektebene und die entsprechende Instantiierung der Axiomatisierung des gleichen Schrittes auf der Metaebene, wie wir sie vorher für den Fall des modus ponens gezeigt haben, sind natürlich zwei verschiedene Beschreibungen ein und derselben Sache. Da Maschinen nichts von selbst wissen können, muß auch dies einem solchen System explizit gesagt werden, was unter der Bezeichnung Reflexionsprinizip bekannt ist. Hinsichtlich der Formalisierung dieses Prinzips verweisen wir auf die entsprechende Spezialliteratur [Wey80, BK82, Kow91].
Bei dieser Form der Reflexion muß man einige Sorgfalt walten lassen, um
nicht in widersprüchliche Systeme zu geraten. Betrachten wir zB. ein
Literal, sagen wir , dann ließe sich der dadurch zum Ausdruck
gebrachte Sachverhalt auf der Metaebene auch als
hat_die_Eigenschaft(c,``P'') zum Ausdruck bringen. Das genannte
Reflexionsprinzip erfordert hierzu den folgenden Zusammenhang.
In dieser Form spricht man auch vom
Komprehensionsaxiom. Dieser
Zusammenhang erscheint so natürlich, daß er schon von G. Frege vor
über hundert Jahren formuliert worden ist. Erst Jahrzehnte später ist von
B. Russel gezeigt worden, daß ein unkontrollierter Ansatz dieser Art
zu Widersprüchen führt. Grob gesagt, definierte er ein Prädikat
durch
und
instantiierte die Variable
mit ``R''. Dies besagt dann, daß
genau dann gilt, wenn es nicht gilt, wodurch der Widerspruch
auf der Hand liegt. In jüngerer Zeit ist jedoch gezeigt worden, daß nur
eine unerhebliche Einschränkung genügt, um einen solchen Widerspruch zu
vermeiden [Fef84, Per85].
Die soeben besprochene Amalgamierung von Objekt- und Metaebene ist zur Realisierung des Ziels der Selbstreflexivität nicht zwingend erforderlich. Die Alternative hierzu ist, alles gleich auf der Metaebene zu beschreiben (und diese dadurch zur Objektebene zu machen). Ein solcher Ansatz ist bislang als in bezug auf Effizienz wenig aussichtsreich eingeschätzt worden. Mit Techniken wie der partiellen Vorauswertung (engl. partial evaluation) kann solchen Bedenken aber begegnet werden, so daß reine Metasysteme in letzter Zeit im Kommen zu sein scheinen [GT91, Pau89, CAB+86].
Christoph Quix, Thomas List, René Soiron