Nächste Seite: 3.5.2 Allgemeinere Formen der Vorige Seite: 3.5 Zirkumskription

3.5.1 Prädikatszirkumskription

In diesem ersten Unterabschnitt betrachten wir die natürlichste und einfachste Form der Zirkumskription, in der die Extension eines der auftretenden Prädikate mittels einer pauschalen Formel minimiert wird. Schon dieser einfache Fall wird das Prinzip der Zirkumskription als einer logischen Minimierung verdeutlichen. Zur besseren Lesbarkeit beginnen wir mit ein paar notationellen Vereinbarungen.

Im folgenden werden immer Prädikatszeichen mit beliebig vielen Stellen zugelassen. Wir fassen jedoch alle Argumente zu einem einzigen (Vektor-) Argument zusammen und schreiben also zB. anstelle von . In Abschnitt 2.6.4 haben wir bereits als Abkürzung für eingeführt, die bei den Vererbungsnetzen gebräuchlich ist. Bei der Zirkumskription hat sich für genau das Gleiche die Schreibweise eingebürgert. Der Grund für diese Notation liegt in der semantischen Überlegung, daß nämlich beim Vorliegen dieser Formel die Extension von in der von in jedem Modell enthalten sein muß. ist eine Abkürzung für , und eine für . bezeichnet diejenige Formel, die aus (der endlichen Formel) durch Substitution von durch hervorgeht. In solchen Fällen nehmen wir immer stillschweigend an, daß der resultierende Ausdruck wieder eine Formel ist, was insbesondere die gleiche Stelligkeit beider Prädikatszeichen erforderlich macht. Mit dieser Notation ergibt sich nun die entscheidende Definition [McC80].

Zu einer gegebenen Weltbeschreibung und einem Prädikatszeichen sei die Zirkumskriptionsformel für in definiert als

Die zugehörige Theorie ergibt sich dann als

Die in der Zirkumskriptionsformel zu hinzugefügte Formel drückt wörtlich aus, daß es kein Prädikat geben soll, für das alles in Gesagte gilt und dessen Extension jedoch noch echt kleiner ist als die von . Mit anderen Worten, erfüllt die Vorgaben von auf die denkbar sparsamste Weise. Dies entspricht, hier eingeschränkt auf ein einziges Prädikat, genau der im Vorspann dieses Abschnitts ausgeführten Motivation. Das, was über in gesagt ist, umfaßt alles Relevante und sollte durch nichts ergänzt werden. Die dabei erforderliche Quantifizierung über Prädikatszeichen führt uns in die Logik zweiter Stufe (siehe [Bib92]).

Im weiteren Verlauf werden wir noch weitere Zirkumskriptionsformeln kennenlernen. Im Vergleich werden wir eine dann als stärker\ indexZirkumskriptionsformel als die andere ansehen, wenn sie noch mehr minimiert. Sie führen alle zu einem nichtmonotonen Verhalten, da die Hinzufügung weiterer Informationen bezüglich der auftretenden Prädikate natürlich auch einen Einfluß auf den durch die (sich mitverändernde) Zirkumskriptionsformel verursachten Minimierungsprozeß haben können.

Damit haben wir die Grundidee der Zirkumskription kennengelernt. Neben den uns bereits aus den letzten beiden Abschnitten vertrauten Fragestellungen, wie der nach der Behandlung von mehr als einem Prädikat sowie nach der Konsistenz, werden wir uns hier auch mit der Frage befassen müssen, inwieweit sich die hier auftauchende Formel zweiter Stufe im Rahmen eines Deduktionsverfahrens behandeln läßt. Zunächst jedoch geben wir zwei alternative, äquivalente Formulierungen an.

Die Äquivalenz der somit drei verschiedenen Formulierungen der Zirkumskription eines Prädikats sieht man leicht über die semantische Bedeutung dieser Formeln ein. Sie läßt sich natürlich auch syntaktisch beweisen.

Um den Leser nicht allzusehr mit Manipulationen an Formeln zweiter Stufe zu traktieren, steuern wir als erstes zwei Ergebnisse an, mit denen die Zirkumskription in wichtigen Fällen zu einer Formel der Logik erster Stufe führt. Dazu erinnern wir an die Definition 3.3 einer in solitären Klauselmenge. Eine solch solitäre Klausel läßt sich mit unserer Notation jetzt in der Form schreiben. Wir verallgemeinern diese Definition unter Verwendung dieser Form auf beliebige Formeln (also nicht nur Klauseln).

Eine Formel heißt solitär in , wenn sie sich in der Form schreiben läßt. ist hierbei eine beliebige Formel mit nur negativem Auftreten von , während kein Auftreten von enthält.

Für solche solitären Formeln erhalten wir das folgende Resultat [Lif85b].

Es gilt , wobei

Wenn aus einer Konjunktion von Literalen besteht, dann läßt sich auch als eine Klausel lesen (im Sinne von PROLOG ist es sogar eine Klausel). Diese Klausel ist dann auch solitär im Sinne der Definition 3.3. Hat man mehrere Klauseln dieser Gestalt, so lassen sie sich durch Faktorisierung des Kopfes zu einer Formel der Gestalt zusammenfassen. Solitäre Klauseln können also als Spezialfall der solitären Formeln aufgefaßt werden. In diesem Spezialfall von solitären Klauseln stimmt die Zirkumskription mit der Prädikatsvervollständigung offensichtlich voll überein. Insbesondere kollabiert hier die Zirkumskriptionsformel also zu einer Formel erster Stufe. Die Anwendung dieses Satzes auf die zu Beginn dieses Abschnitts genannte Formel , die sich äquivalent auch als schreiben läßt, ergibt . Dies ist genau das gewünschte Resultat. Es wird aber nur mit dem Trick erzielt, daß die Zirkumskription ohne den Existenzquantor durchgeführt wird; ein stärkeres Verfahren, das auch ohne einen solchen Trick auskommt, werden wir in Abschnitt 3.5.3 kennenlernen.

Daß wir mit der Prädikatszirkumskription noch nicht in allen Fällen das gewünschte Ergebnis erzielen, zeigt die Anwendung auf unser vertrautes Beipiel 3.2 der Eiscreme-liebenden Kinder. Die Zirkumskription des Prädikats ``Abnormal'' darin ergibt aufgrund unseres Satzes das Ergebnis , aber nicht die gewünschte Aussage über Larissa. Hieraus können wir schließen, daß die Prädikatszirkumskription in der bis jetzt besprochenen Form noch keine befriedigende Lösung offeriert. Eine in dieser Hinsicht verbesserte Form werden wir im nächsten Unterabschnitt kennenlernen. Zunächst jedoch verallgemeinern wir unser Resultat auf die folgende Formelklasse.

Eine bezüglich separable Formel ist induktiv wie folgt definiert.

1. Enthält kein positives Auftreten von , dann ist sie separabel.
2. Eine Formel der Gestalt ist separabel, wenn kein Auftreten von enthält.
3. Die Konjunktion und Disjunktion von separablen Teilformeln ist separabel.

Insbesondere sind solitäre Formeln also auch separabel bezüglich . Man kann leicht zeigen, daß sich, unter Benutzung der oben eingeführten Notation, jede separable Formel in der Form

schreiben läßt. Auch für separable Formeln reduziert sich die Zirkumskription auf die Prädikatenlogik erster Stufe [Lif85b].

Sei eine separable Formel, dann gilt für die Zirkumskription von P

wobei

In [Lif87, Rab89] werden noch allgemeinere Klassen von Formeln angegeben, für die das Zirkumskriptionsproblem in dieser Weise auf die erste Stufe reduzierbar ist.

Nicht für alle Formeln läßt sich die Prädikatszirkumskription auf die erste Stufe reduzieren. Ein Beispiel ist die Formel

Die Formel besagt, daß den transitiven Abschluß von umfaßt. Die Zirkumskription von würde also besagen, daß sogar genau diesen Abschluß darstellt, was beweisbar nicht in der Logik erster Stufe formuliert werden kann.

Wir kommen nun zu der Frage der Konsistenz der aus der Zirkumskription resultierenden Theorie. Wieder (wie in den beiden vorangegangenen Abschnitten) ist dies nicht trivial. Betrachten wir nämlich die Definition der natürlichen Zahlen (worin den Nachfolger von bezeichnet),

so führt die Zirkumskription von zu einer inkonsistenten Theorie. Dies hängt damit zusammen, daß es keine -minimalen Modelle (dh. Modelle, bei denen die Extension von minimal ist) für die natürlichen Zahlen gibt [Dav80]. Es sind aber eine Reihe von hinreichenden Bedingungen bekannt, die die Konsistenz garantieren [Lif86a]. Wir nennen daraus das folgende Resultat, das unsere bisherigen Ergebnisse abrundet.

Ist konsistent und bezüglich separabel, so ist konsistent.

Im folgenden Unterabschnitt werden wir dann noch ein allgemeineres Resultat nennen.

Die Zirkumskription ist verwandt mit der impliziten Definierbarkeit , wie sie aus der mathematischen Logik seit langem bekannt ist [Doy85], die besagt, daß eine Formel eine eindeutige Interpretation für ein Prädikat erzwingt. Formal definiert dieses Prädikat implizit, wenn die Formel für jeden Ausdruck gültig ist. Es gilt: Wenn eine Formel ein Prädikat implizit definiert, so auch explizit [Bet53].