• Pränexform und universelle Formeln
• Herbrand-Interpretationen
• Skolemisierung

Die Folgerungsbeziehung und andere semantische Begriffe sind mit den bisherigen Definitionen zwar formal präzise charakterisiert, aber auf eine Art, die keine Grundlage für eine algorithmische Behandlung bietet. Betrachten wir zum Beispiel die Frage, ob zwischen zwei -Formeln F und G die Folgerungsbeziehung besteht. Nach Definition besteht sie genau dann, wenn jede Interpretation, die F erfüllt, auch G erfüllt. Eine Interpretation wiederum basiert auf einer beliebigen nichtleeren Menge als Universum. Es gibt also mindestens so viele Interpretationen wie es Mengen gibt, und für jede davon wäre zu überprüfen, ob sie, wenn sie F erfüllt, auch G erfüllt. Darauf lässt sich kein Algorithmus aufbauen.

Damit liegt die Frage nahe, ob man vielleicht gewisse ,,Referenzinterpretationen`` auszeichnen kann, so dass man zum Nachweis der Folgerungsbeziehung die genannte Überprüfung nicht für jede überhaupt mögliche Interpretation durchführen muss, sondern nur für diese Referenzinterpretationen. Das wäre ein wichtiger Zwischenschritt in Richtung Algorithmisierung.

Tatsächlich haben wir im Zusammenhang mit der Gleichheit bereits etwas ähnliches kennengelernt. In Satz 3.6.6 wurde die Folgerungsbeziehung ja auf die Beziehung zurückgeführt. Wenn die Gleichheitsaxiome beteiligt sind, braucht man zum Nachweis der Folgerungsbeziehung die Überprüfung also nicht für sämtliche Interpretationen durchzuführen, sondern kann sich auf die normalen Interpretationen beschränken.

Natürlich nützt die Beschränkung auf normale Interpretationen nicht viel im Hinblick auf die Algorithmisierbarkeit, da ja auch die normalen Interpretationen jede beliebige nichtleere Menge als Universum benutzen können, doch zeigt das Ergebnis immerhin, dass die Idee der Referenzinterpretationen nicht von vornherein aussichtslos ist. Die angestrebten Referenzinterpretationen sollten aber in erster Linie bewirken, dass weniger Universen betrachtet werden müssen.

Genau das ist für Herbrand-Interpretationen der Fall. Alle Herbrand-Interpretationen basieren auf einem einzigen ausgezeichneten Universum, dem sogenannten Herbrand-Universum.

Wenn die beteiligten Formeln eine bestimmte syntaktische Eigenschaft haben, nämlich universell sind, reicht es tatsächlich aus, zum Nachweis der Folgerungsbeziehung die Überprüfung nur für Herbrand-Interpretationen durchzuführen statt für sämtliche Interpretationen. Zudem können Formeln, die nicht universell sind, mit Hilfe der Skolemisierung in universelle Formeln transformiert werden, die in einem gewissen Sinn äquivalent zu den ursprünglichen Formeln sind. Insgesamt wird das angestrebte Ziel damit für alle Formeln erreicht.

Im folgenden werden wir zunächst universelle Formeln behandeln, danach Herbrand-Interpretationen und schließlich die Skolemisierung.

Eigenschaften von Formeln der Prädikatenlogik erster Stufe, insbesondere im Zusammenhang mit Herbrand-Interpretationen, hängen oft davon ab, welche Quantoren in den Formeln vorkommen und wo sie relativ zu Negationsjunktoren stehen. Sei zum Beispiel F die Formel ¬(∃x p(x)∨¬∀y q(y)). Es gilt:

F	=	¬(∃x p(x)∨¬∀y q(y))
		(¬∃x p(x)∧¬¬∀y q(y))	de Morgan'sche Regel (Satz 3.3.7)
		(¬∃x p(x)∧∀y q(y))	Regel der doppelten Negation(3.3.7)
		(∀x ¬p(x)∧∀y q(y))	Regel der negierten Quantoren(3.5.13)

Dieses ,,eigentlich`` wird durch die sogenannte Polarität formalisiert. Die Teilformel ∃x p(x) hat negative Polarität in F, weil die Teilformel in F im Bereich einer Negation steht. Die Teilformel ∀y q(y) hat dagegen positive Polarität in F, weil sie im Bereich von zwei Negationen steht, die einander ja aufheben. Existenzquantoren mit negativer Polarität in einer Formel wirken wie Allquantoren mit positiver Polarität.

Für Informatiker ist diese Definition am einfachsten dadurch zu veranschaulichen, dass sie sich die Formel F durch ihren Syntaxbaum dargestellt denken, also einen Baum, dessen Blätter die Vorkommen von atomaren Teilformeln von F sind und dessen innere Knoten mit Junktoren und Quantoren beschriftet sind. Die Wurzel dieses Baums wird wegen 1. als positiv markiert. Der Rest der Definition gibt an, wie das Vorzeichen auf alle Nachfolgerknoten bis hin zu den Blättern propagiert wird.

Bei dieser Propagation wechselt das Vorzeichen bei jedem Negationsjunktor. Sei zum Beispiel F die Formel ¬¬¬p, dann haben ¬¬¬p und ¬p positive Polarität in F, während ¬¬p und p negative Polarität in F haben. Die Polarität eines Vorkommens einer Teilformel drückt aus, ob dieses Vorkommen im Bereich einer geraden oder einer ungeraden Anzahl von Negationen steht, ob diese Negationen einander also aufheben oder nicht.

Das Vorzeichen wechselt außerdem auf der linken Seite des Implikationsjunktors ⇒. Nach Satz 3.5.13 und Satz 3.3.7 gilt (G₁⇒G₂) (¬G₁∨G₂). Die linke Teilformel G₁ steht also ,,eigentlich`` im Bereich einer impliziten Negation, die bei der Definition der Polarität mit berücksichtigt wird.

Ist F eine Formel, in der der Äquivalenzjunktor ⇔ nicht auftritt, so ist jedes Vorkommen einer Teilformel von F eindeutig als ein Vorkommen positiver oder negativer Polarität klassifiziert.

Dagegen haben alle Teilformeln, die im Syntaxbaum unterhalb eines Äquivalenzjunktors vorkommen, sowohl positive als auch negative Polarität. Die Begründung dafür liefert die Regel zur Auflösung des Äquivalenzjunktors nach Satz 3.5.13 und Satz 3.3.7: (G₁⇔G₂) ((¬G₁∨G₂)∧(G₁∨¬G₂)). Jede der beiden unmittelbaren Teilformeln von (G₁⇔G₂) kommt also ,,eigentlich`` einmal negiert und einmal unnegiert vor. Das gleiche gilt mit der zweiten Regel (G₁⇔G₂) ((G₁∧G₂)∨(¬G₁∧¬G₂)).

Tritt eine Teilformel mehrfach in einer Formel auf, so können verschiedene Vorkommen der Teilformel unterschiedliche Polaritäten haben. Ist zum Beispiel F die Formel (p ∨ ¬p), hat das erste Vorkommen von p positive Polarität in F und das zweite negative.

Beispiel: Für F=¬(∃x₁ p(x₁)∨ ¬∀x₂ q(x₂)) ist F'=¬(p(x₁)∨ ¬q(x₂)), und es gilt F ∀x₁∀x₂¬(p(x₁)∨ ¬q(x₂)).

Wegen der Regel zur Auflösung des Äquivalenzjunktors (Satz 3.5.13 und Satz 3.3.7) ist jede geschlossene -Formel logisch äquivalent zu einer geschlossenen -Formel, in der der Äquivalenzjunktor ⇔ nicht vorkommt. Mit den Variablenumbenennungsregeln (Satz 3.5.13) kann außerdem stets erreicht werden, dass die quantifizierten Variablen in einer Formel paarweise verschieden und verschieden von den Variablen sind, die frei in der Formel vorkommen. Insgesamt erhalten wir damit:

Aus der Definition der Polarität ergibt sich unmittelbar, dass eine Formel, die einen Quantor in einer mit ⇔ gebildeten Teilformel enthält, nicht universell sein kann.

Wenn Herbrand-Interpretationen, wie in der Einleitung erläutert, auf einem ausgezeichneten Universum basieren, stellt sich die Frage, woraus so ein ausgezeichnetes Universum überhaupt bestehen kann. Da es stellvertretend für alle denkbaren Universen stehen soll, müsste es ,,Universal`` enthalten in dem Sinn, dass Objekte jeglicher anderer Universen damit repräsentiert werden können. Ob es so ein ,,Universaluniversum`` überhaupt gibt, erscheint auf den ersten Blick äußerst fraglich.

Bei näherer Betrachtung sind uns solche ,,Universalobjekte`` aber längst wohlvertraut. Wir benutzen doch ständig die syntaktischen Terme einer Sprache der Prädikatenlogik erster Stufe, um damit die Objekte beliebiger Universen zu repräsentieren. Mit anderen Worten, die Menge aller Terme, oder vielleicht die Menge gewisser Terme, einer Sprache der Prädikatenlogik erster Stufe wäre doch ein naheliegender Kandidat für das angestrebte ausgezeichnete Universum.

Dieser Gedanke kann natürlich Verwirrung stiften. Bisher haben wir Syntax und Semantik sorgfältig auseinandergehalten. Wenn die Grundlage aller semantischen Begriffe, das Universum, jetzt aus Termen bestehen soll, also aus syntaktischen Elementen, ist eine gewisse Vermischung von Syntax und Semantik unvermeidlich. Diese begriffliche Verwirrung ist sicherlich ein Nachteil des Ansatzes.

Andererseits kennen wir aus der Informatik analoge Fälle von scheinbarer begrifflicher Verwirrung, die sich als äußerst vorteilhaft erweisen. Zum Beispiel muss man bei einem Übersetzer Quellsprache, Zielsprache und Implementierungssprache sorgfältig auseinanderhalten. Wenn man dann Übersetzer betrachtet, deren Implementierungssprache gleich ihrer Quellsprache ist, wirkt dies zunächst verwirrend oder sogar unsinnig. Dabei stellt sich aber heraus, dass solche Übersetzer sogar besonders nützliche Eigenschaften haben. In ähnlicher Weise erweist sich die Vermischung von Syntax und Semantik in der Logik als nützlich.

Zur Realisierung des Ansatzes bleibt noch zu klären, ob das ausgezeichnete Universum aus allen Termen der Sprache bestehen soll oder nur aus bestimmten Termen. Diese Entscheidung führt zu technischen Unterschieden, aber keinen prinzipiellen. Herbrand-Interpretationen benutzen als Universum die Menge aller Grundterme, also der variablenfreien Terme.

Das Herbrand-Universum einer Sprache der Prädikatenlogik erster Stufe ist die Menge aller Grundterme der Sprache. Wir erinnern an eine Voraussetzung in der Definition von (Definition 2.3.1): ,,Es wird vorausgesetzt, dass mindestens eine Konstante enthält.`` Dank dieser Voraussetzung ist die Menge der Grundterme nicht leer und kann daher als Universum dienen. (Das war der einzige Grund für die Voraussetzung.)

Von den Bestandteilen einer Interpretation ist für Herbrand-Interpretationen also der überwiegende Teil von vornherein vorgegeben. Das Universum ist immer die Menge der Grundterme. Die Funktion Ab ist für Konstanten und Funktionssymbole immer so festgelegt, dass jeder Grundterm ,,mit sich selbst`` interpretiert wird. Das einzige, was einer Herbrand-Interpretation überhaupt noch an eigenen Definitionsmöglichkeiten offensteht, ist die relativ uninteressante Umgebung sowie die Definition der Funktion Ab für Relationssymbole.

Um letztere zu definieren, muss die Herbrand-Interpretation festlegen, welche Relation, also welche Menge von Tupeln von Grundtermen, jedem Relationssymbol zugeordnet ist. Wenn man vor ein Tupel von Grundtermen das Relationssymbol schreibt, erhält man ein Grundatom. Das, was eine Herbrand-Interpretation neben der Umgebung überhaupt noch festlegen muss, lässt sich damit bequem durch eine Menge B von Grundatomen repräsentieren, also eine Teilmenge der Herbrandbasis HB.

Ist M die von B repräsentierte Herbrand-Interpretation mit einer beliebigen Umgebung U, gilt mit dieser Definition für jedes Grundatom A, dass MA gdw. A∈B. Somit erfüllt M also genau die Grundatome in B und falsifiziert alle anderen Grundatome. Für jede andere Formel ist aufgrund der Definition der Modellbeziehung dann ebenfalls festgelegt, ob M die Formel erfüllt oder falsifiziert.

Da wir Herbrand-Interpretationen nur im Zusammenhang mit geschlossenen Formeln betrachten werden, spielt die Umgebung nach dem Koinzidenzsatz 3.5.10 keine Rolle. Durch Vorgabe der festen Umgebung U_c (die auch anders hätte gewählt sein können und die für geschlossene Formeln sowieso irrelevant ist) ist für jedes B⊆HB die Herbrand-Interpretation eindeutig bestimmt. Umgekehrt bestimmt jede Herbrand-Interpretation M eindeutig eine Teilmenge B_M={A∈HB | MA}⊆HB . Wegen dieser eineindeutigen Entsprechung bezeichnet man gelegentlich eine Menge von Grundatomen sogar selbst als eine Herbrand-Interpretation bzw. ein Herbrand-Modell.

Für beliebige Interpretationen übersetzt der Substitutionssatz zwischen einer Umgebung, die einer Variablen semantisch ein Objekt des Universums zuordnet, und einer Substitution, die eine Variable syntaktisch durch einen Term ersetzt. Der obige Satz zeigt, dass für Herbrand-Interpretationen, wo die Objekte des Universums Terme sind, Umgebungen und Substitutionen zusammenfallen. Die Vermischung von Syntax und Semantik bei Herbrand-Interpretationen ist hier also günstig, weil sie eine Vereinfachung bewirkt.

Der Satz 3.8.10 gilt für Nicht-Herbrand-Interpretationen im allgemeinen nicht. Wir betrachten zwei Gegenbeispiele.

Beispiel 3.8.11.   Die Sprache bestehe aus einer Konstanten a und einem einstelligen Relationssymbol p und sonst keinen Symbolen.
Sei M=({1,2},Ab,U) mit Ab(a)=1 und Ab(p)={1}.
Es gilt Mp(a) und M[1/x]p(x) und M[2/x]nichtp(x).
Der einzige Grundterm ist a.

1. Für jeden Grundterm t gilt Mp(x)[t/x], aber Mnicht∀x p(x).
2. M∃x ¬p(x), aber es gibt keinen Grundterm t mit M¬p(x)[t/x].

Hier ist der Satz deshalb verletzt, weil es nur einen einzigen Grundterm gibt, aber zwei Objekte im Universum, so dass das Objekt 2 des Universums durch gar keinen Grundterm repräsentiert ist. Man könnte vermuten, dass dieses Phänomen leicht zu vermeiden sei, sobald die Sprache Funktionssymbole enthält, denn dann gibt es ja unendlich viele Grundterme. Das nächste Beispiel zeigt aber, dass das Phänomen prinzipiell nicht vermeidbar ist.

Beispiel 3.8.12.   Die Sprache bestehe aus abzählbar unendlich vielen Konstanten und zu jeder Stelligkeit abzählbar unendlich vielen Funktionssymbolen sowie aus einem einstelligen Relationssymbol p.
ℜ bezeichne die Menge der reellen Zahlen. Sei M=(ℜ,Ab,U) mit Ab(p)={t^M | t Grundterm. Da es nur abzählbar viele Grundterme gibt, gibt es d∈ℜ mit d∉Ab(p), so dass .

1. Für jeden Grundterm t gilt Mp(x)[t/x], aber .
2. , aber es gibt keinen Grundterm t mit M¬p(x)[t/x].

Man kann zu jeder beliebigen Interpretation M auf natürliche Weise eine Herbrand-Interpretation konstruieren, die M weitgehend nachbildet.

Es mag verwundern, dass der zweite Teil dieses Satzes nur mit ,,wenn dann`` formuliert ist und nicht mit ,,genau dann wenn``. Tatsächlich gilt die Gegenrichtung im allgemeinen nicht. Der Grund sind genau die obigen Beispiele 3.8.11 und 3.8.12. Für die darin angegebene Interpretation M gilt jeweils ∀x p(x), aber .

Die Beispiele zeigen außerdem die Notwendigkeit der Voraussetzung, dass F universell ist. In den Beispielen gilt jeweils M∃x ¬p(x), aber nicht∃x ¬p(x).

Der Zusammenhang zwischen der Erfüllung einer Formel durch eine beliebige Interpretation und der Erfüllung der Formel durch die aus der Interpretation konstruierte Herbrand-Interpretation ist also nicht sehr stark. Trotzdem hat er weitreichende Konsequenzen.

Für die Formeln und Formelmengen mit den angegebenen syntaktischen Eigenschaften ist damit das eingangs motivierte Ziel erreicht. Zum Nachweis der Folgerungsbeziehung reicht es wegen der letzten beiden Ergebnisse aus, die Überprüfung auf Herbrand-Interpretationen und damit auf ein einziges Universum zu beschränken.

Übrigens hätte die Motivation in der Einleitung zu Abschnitt 3.8 nicht unbedingt auf der Folgerungsbeziehung aufgebaut werden müssen. Eine analoge Motivation wäre auch mit der Erfüllbarkeit oder einem anderen der semantischen Begriffe möglich gewesen. Die ersten Ergebnisse des Satzes zeigen, dass das Ziel auch für diese anderen semantischen Begriffe jetzt erreicht ist: zum Nachweis der jeweiligen semantischen Eigenschaft müssen nicht mehr sämtliche Interpretationen betrachtet werden, sondern nur noch die Herbrand-Interpretationen, jedenfalls für Formeln und Formelmengen mit den angegebenen syntaktischen Eigenschaften.

Aus Satz 3.8.10 folgt unter Zuhilfenahme von Satz 3.8.14 unmittelbar ein weiteres Ergebnis mit sehr weitreichenden Konsequenzen, auf die Kapitel 4 näher eingehen wird.

In diesem Abschnitt zeigen wir, dass zu jeder endlichen Menge S von (beliebigen) geschlossenen Formeln eine Menge S* von universellen geschlossenen Formeln konstruiert werden kann, so dass S* genau dann ein Modell hat, wenn S ein Modell hat. Dieses Ergebnis reicht aus, um die Folgerungsbeziehung für beliebige Formeln durch die Überprüfung von Herbrand-Interpretationen nachweisen zu können. Das Verfahren, mit dem S* aus S konstruiert wird, nennt man Skolemisierung.

Der genaue Zusammenhang zwischen S und S ist allerdings etwas komplizierter. Die Menge S enthält -Formeln für eine gegebene Sprache der Prädikatenlogik erster Stufe. Diese Sprache wird zunächst um zusätzliche Funktionssymbole erweitert zu einer Sprache *. Die Menge S besteht dann aus *-Formeln. Man muss deshalb auch zwischen -Interpretationen und *-Interpretationen unterscheiden. Das ist der wesentliche Grund, dass S und S nicht einfach logisch äquivalent sind. Aber die Beziehung zwischen den Modellen von S (bezüglich ) und den Modellen von S (bezüglich *) wird sich als sehr viel enger erweisen, als es für das obengenannte Gesamtergebnis erforderlich ist.

Um die Grundidee der Skolemisierung informell zu verstehen, betrachten wir noch einmal die Axiome einer Boole'schen Algebra nach Definition 3.2.1.

Das erste Axiom verlangt unter anderem, dass es ein neutrales Element für die Operation gibt. Die unmittelbare Übersetzung dieser Forderung ergäbe folgende Formel der Prädikatenlogik erster Stufe: ∃y∀x (yx x). Tatsächlich wurde das Axiom aber so formuliert, dass die entsprechende Formel der Prädikatenlogik erster Stufe lautet: ∀x(1x x). Das als existent geforderte Element wurde also durch eine Konstante repräsentiert statt durch eine existentiell quantifizierte Variable.

Das letzte Axiom verlangt unter anderem, dass es zu jedem Element ein komplementäres Element bezüglich der Operation + gibt. Diese Forderung lässt sich darstellen durch die Formel ∀x∃y (x+y1), aber auch durch die Formel ∀x (x+‾x1). Dabei ist ‾ ein Funktionssymbol, das für eine Funktion stehen soll, die zu jedem x ein komplementäres Element liefert.

Ein als existent gefordertes Objekt kann also statt durch eine existentiell quantifizierte Variable auch durch einen Term repräsentiert werden, der mit einem Funktionssymbol gebildet ist. Die Unterterme in diesem Term repräsentieren Objekte, von denen das als existent geforderte abhängt. Im ersten Beispiel bestand so eine Abhängigkeit nicht, so dass der Term mit einem nullstelligen Funktionssymbol, also einer Konstanten, gebildet wurde.

Die Skolemisierung benutzt dieses Prinzip, um systematisch alle Existenzquantoren positiver Polarität und Allquantoren negativer Polarität zu beseitigen und dadurch zu universellen Formeln zu gelangen.

Um die entsprechenden Ergebnisse beweisen zu können, benötigen wir als Hilfsmittel einige Varianten des Ersetzungssatzes.

Bei Ersetzung eines Vorkommens einer Teilformel überträgt sich also die Folgerungsbeziehung von der Teilformel auf die Gesamtformel, sofern das Vorkommen positive Polarität hat. Hat das Vorkommen negative Polarität, überträgt sich die Folgerungsbeziehung in entgegengesetzter Richtung auf die Gesamtformel. Hat ein Vorkommen sowohl positive als auch negative Polarität, überträgt sich die Folgerungsbeziehung im allgemeinen weder in die eine noch in die andere Richtung. Sei zum Beispiel G₁=(p∧q) und G₂=(p∨q), dann gilt G₁G₂. Sei F=((p∧q)⇔¬q), dann ist F⟨G₂, V_G1⟩=((p∨q)⇔¬q). Man rechnet leicht nach, dass sowohl F als auch F⟨G₂, V_G1⟩ ein Modell haben, dass aber keine Interpretation beide Formeln erfüllt, so dass die Folgerungsbeziehung in keiner Richtung besteht.

Der Ersetzungssatz 3.3.6 und 3.5.13 ist ein Spezialfall dieses allgemeineren Ersetzungssatzes für Folgerungen.

Wofür ist diese Verallgemeinerung erforderlich? Insgesamt wird es darum gehen, dass eine ,,große`` Formel F gegeben ist. Darin kommt eine ,,kleine`` Teilformel vor, die mit einem störenden Quantor beginnt. Wenn man diese Teilformel durch eine andere ,,kleine`` Formel ersetzt, in der der störende Quantor beseitigt ist, entsteht die ,,große`` Formel F'.

F = (... QxG ...)
        ∇
F' = (... G' ...)

Ein späterer Satz (Satz 3.8.20) wird belegen, dass zwischen den Formeln QxG und G' Folgerungsbeziehungen bestehen, die von den Polaritäten abhängen. Der Ersetzungssatz für Folgerungen dient dazu, diese Folgerungsbeziehungen von den Teilformeln auf die ,,großen`` Formeln zu übertragen wie folgt.

Wenn die Teilformel QxG positiv in F ist, hat sie die Gestalt ∃xG.

Satz 3.8.20 (2) garantiert:

Wenn die Teilformel QxG negativ in F ist, hat sie die Gestalt ∀xG.

Satz 3.8.20 (3) garantiert:

In beiden Fällen gilt also F'F. Wird ein Existenzquantor positiver Polarität oder ein Allquantor negativer Polarität durch Skolemisierung beseitigt, so folgt in jedem Fall die ursprüngliche Formel F aus der neuen Formel F' - wenn Satz 3.8.20 bewiesen ist. (Es ist übrigens Absicht, dass gemeinsam benutzte Unterfälle der beiden Sätze jeweils die gleiche Nummer (2) bzw. (3) haben. Das gilt auch für die weiteren Sätze mit Unterfällen.)

Die Gegenrichtung FF' gilt nicht. Wir streben eine abgeschwächte Gegenrichtung an: dass man zu jedem M mit MF ein M' konstruieren kann mit M'F und M'F'.

Als Vorbereitung für diese abgeschwächte Gegenrichtung zunächst eine Betrachtung zur Folgerungsbeziehung. Für zwei Formeln G₁ und G₂ gilt G₁G₂ gdw. für jedes M gilt M (G₁ ⇒ G₂). Das ergibt sich direkt aus den Definitionen. Wenn M(G₁ ⇒ G₂) nicht für jedes M gilt, sondern nur für gewisse M, kann man von einer Art schwacher Folgerungsbeziehung sprechen.

Bei der obigen Ersetzung gilt in der Gegenrichtung nicht die Folgerungsbeziehung zwischen QxG und G'. Man kann aber zu jedem Modell M von F ein anderes Modell M' von F so konstruieren, dass diese schwache Folgerungsbeziehung zwischen QxG und G' besteht.

Betrachten wir zunächst nur den Fall, dass die Teilformel positiv in F ist.

		M'		M'
M		F	= (...	∃xG+	...)
		F'	= (...	G'	...)

Das nächste Ziel ist jetzt, diese schwache Folgerungsbeziehung von den Teilformeln auf die ,,großen`` Formeln zu übertragen. Wenn man aus der obigen Situation schließen kann, dass auch M'(F⇒F') gilt, dann gilt auch M'F'. Insgesamt hätte man damit die angestrebte Aussage, dass zu jedem Modell M von F ein Modell M' von F' konstruiert werden kann, das auch ein Modell von F' ist.

Leider lässt sich diese schwache Folgerungsbeziehung nicht für völlig beliebige M' von den Teilformeln auf die ,,großen`` Formeln übertragen. Wenn die Beziehung M'(∃xG⇒G') davon abhängt, welche Umgebung die Interpretation benutzt, dann gilt nicht immer auch M'(F⇒F').

Die Übertragung klappt aber für Interpretationen, die völlig unabhängig von den Umgebungen sind. Dafür brauchen wir eine Schreibweise.

Die nächste, noch allgemeinere, Variante des Ersetzungssatzes erlaubt die angestrebte Übertragung auf die ,,große`` Formel, wenn M' so ist, dass für jede Umgebung U gilt M'[U](∃xG⇒G'). Dann gilt auch für jedes U, dass M'[U] (F⇒F').

Auch für die schwache Folgerungsbeziehung dreht sich also die Richtung um, wenn sie von einer Teilformel negativer Polarität auf die ,,große`` Formel übertragen wird.

Hier noch ein Gegenbeispiel zum interpretationsspezifischen Ersetzungssatz, wenn die Modellbeziehung von der Umgebung abhängt:
Sei G = p(x,x) und G' = p(x,y)
Sei F = ∀x ∀y p(x,x) und F' = F[G'/G] = ∀x ∀y p(x,y).

Es gibt eine Interpretation M = (D,Ab,U) mit M (G ⇒ G'), nämlich D=N und Ab(p)=≤_N und U(x)=U(y)=5. Die schwache Folgerungsbeziehung zwischen G und i>G' besteht also nur deswegen, weil x und y in der Umgebung U denselben Wert haben. Aber für dieses M gilt , da M∀x ∀y p(x,y) aber . Die schwache Folgerungsbeziehung überträgt sich also nicht auf die ,,großen`` Formeln.

Die Interpretationen, die mit Satz 3.8.20 konstruiert werden, hängen nicht von der Umgebung ab, deshalb kann Satz 3.8.19 darauf angewandt werden.

Das Gesamtbild für die noch offene Gegenrichtung ist wie folgt.

Satz 3.8.20 (1) garantiert:

für jede Umgebung U gilt

Satz 3.8.19 (1) sagt, dass daraus folgt:

für jede Umgebung U gilt

Satz 3.8.20 (4) garantiert:

für jede Umgebung U gilt

Satz 3.8.19 (4) sagt, dass daraus folgt:

für jede Umgebung U gilt

[U] MF = (... ∀XG‾ ...) ⇓       F' = (... G' ...)

In beiden Fällen bedeutet die Übertragung, dass für jede Umgebung U gilt. Also gilt auch . Wie oben erläutert, ist damit aus dem Modell M von F ein Modell M' von F und auch von F' konstruiert.

Nun aber zu dem angekündigten Satz, von dem alle obigen Schemata abhängen.

Die Formeln ∃xG und G' (bzw. G' und ∀xG) sind also nicht logisch äquivalent, aber fast. In der einen Richtung gilt die Folgerungsbeziehung immer. In der anderen gilt sie nicht immer, weil manche Interpretationen das Funktionssymbol f mit einer ,,unpassenden`` Funktion interpretieren können. Da nach Voraussetzung f nicht in G vorkommt, kann man in diesen Fällen aber immer eine ,,passende`` Definition für f angeben, ohne irgend etwas anderes an der Interpretation zu ändern, so dass die Folgerungsbeziehung bezüglich dieser ,,angepassten`` Interpretationen auch in der Gegenrichtung gilt.

Bei der Skolemisierung einer Formel nach der Konstruktion in diesem Beweis werden falsch quantifizierte Variablen der Reihe nach durch Terme ersetzt, die mit neu eingeführten Funktionssymbolen, sogenannten Skolem-Funktionssymbolen, gebildet werden. Eine aus F durch Skolemisierung gewonnene universelle Formel nennt man eine Skolemform von F. Die mit den Skolem-Funktionssymbolen gebildeten Terme kann man als eine Umbenennung der Objekte auffassen, deren Existenz in der Formel gefordert wird.

Die Skolemform ist nicht eindeutig, da sie von der Reihenfolge abhängt, in der die Quantoren falscher Polarität ersetzt werden. Zum Beispiel sei F die geschlossene Formel ∀u ∃v ∃w p(u,v,w). Ersetzen wir zuerst ∃v und dann ∃w, entsteht zuerst ∀u ∃w p(u,f(u),w) und dann ∀u p(u,f(u),g(u)). Letzteres ist eine Skolemform von F. In der anderen Reihenfolge entsteht erst ∀u ∃v p(u,v,h(u,v)), dann ∀u p(u,k(u),h(u,k(u))). Letzteres ist auch eine Skolemform von F.

Es gibt verschiedene Verfahren, um eine Skolemform aus einer Formel zu gewinnen. Neben der Festlegung der Reihenfolge der Ersetzungen kann man auch festlegen, dass vor den Ersetzungen zunächst die Quantoren in der Formel verschoben werden. Am einfachsten zu verstehen ist die Skolemisierung, wenn man die Formel zunächst in eine Pränexform umwandelt. Um die Komplexität der neuen Terme gering zu halten, ist es dagegen günstiger, die Quantoren zunächst möglichst weit nach innen zu ziehen und eine sogenannte Antipränexform oder Miniscope-Form herzustellen.

Die Voraussetzung des obigen Satzes, dass jedes Quantorvorkommen eine eindeutige Polarität hat, lässt sich mit der Regel zur Auflösung des Äquivalenzjunktors (Satz 3.5.13 und Satz 3.3.7) immer herstellen. Also gilt:

Kombiniert mit Satz 3.8.14 ergibt sich daraus die Lösung für das Gesamtziel dieses Abschnitts: alle semantischen Begriffe auf Herbrand-Interpretationen zurückzuführen.

Aus Satz 3.8.21 folgt ein klassisches Ergebnis.