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 WeltbeschreibungDie in der Zirkumskriptionsformel zuund einem Prädikatszeichen
sei die Zirkumskriptionsformel für
in
definiert als
![]()
Die zugehörige Theorie ergibt sich dann als
![]()
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 giltWenn, wobei
![]()
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üglichInsbesondere sind solitäre Formeln also auch separabel bezüglichseparable Formel
ist induktiv wie folgt definiert.
- Enthält
kein positives Auftreten von
, dann ist sie separabel.
- Eine Formel der Gestalt
ist separabel, wenn
kein Auftreten von
enthält.
- Die Konjunktion und Disjunktion von separablen Teilformeln ist separabel.
schreiben läßt. Auch für separable Formeln reduziert sich die Zirkumskription auf die Prädikatenlogik erster Stufe [Lif85b].
SeiIn [Lif87, Rab89] werden noch allgemeinere Klassen von Formeln angegeben, für die das Zirkumskriptionsproblem in dieser Weise auf die erste Stufe reduzierbar ist.eine separable Formel, dann gilt für die Zirkumskription von P
![]()
wobei
![]()
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.
IstIm folgenden Unterabschnitt werden wir dann noch ein allgemeineres Resultat nennen.konsistent und bezüglich
separabel, so ist
konsistent.
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].
Christoph Quix, Thomas List, René Soiron