4.9 Der Endlichkeitssatz

© 1999 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.

Beweis:

Da abzählbar ist und es somit insgesamt nur abzählbar viele -Formeln gibt, ist S abzählbar unendlich.

Nach Satz 3.8.22 gibt es eine Erweiterung _sko von um abzählbar viele Funktionssymbole und eine abzählbar unendliche Menge S_sko von universellen geschlossenen _sko-Formeln, so dass S genau dann ein Modell hat, wenn S_sko ein Modell hat. Zu jeder Formel F∈S sei F_sko∈S_sko die eineindeutig zugeordnete universelle Formel. Sei o.B.d.A. jedes F_sko in Pränexform.

Zu jedem F∈S sei F* die Menge der Grundinstanzen von F_sko. Sei S* die Vereinigung all dieser Mengen. Nach Satz 3.8.16 ist S_sko und damit S genau dann erfüllbar, wenn S* ein Herbrand-Modell besitzt. Wie im Beweis von Satz 4.6.1 können wir S* als aussagenlogische Formelmenge ansehen.

Mit diesen Vorbereitungen zeigen wir jetzt die Kontraposition der Behauptung. Sei also S unerfüllbar. Dann ist S* unerfüllbar. Nach dem Endlichkeitssatz für die Aussagenlogik (Satz 3.3.9) gibt es eine unerfüllbare endliche Teilmenge {G₁,...,G_n}⊆S*.

Zu jeder der Formeln G_i sei F_i∈S eine Formel mit G_i∈F_i*. Es gibt zu jedem G_i mindestens eine solche Formel (es kann auch beliebig viele geben). Nun ist {F₁,...,F_n} eine Formelmenge, deren Menge von Grundinstanzen F₁*∪ ... ∪F_n* die unerfüllbare Teilmenge {G₁,...,G_n} enthält und damit selbst unerfüllbar ist. Nach Satz 3.8.16 ist {F₁,...,F_n} unerfüllbar, und es ist eine endliche Teilmenge von S.

Wie bereits in Kapitel 3 erwähnt, bezieht sich der Name ,,Kompaktheitssatz`` auf einen Beweis des Satzes, der auf der Kompaktheit eines topologischen Raums beruht. Eine andere verbreitete Technik zum Beweis des Endlichkeitssatzes setzt eine Beweismethode voraus. Zum Beispiel ist die PUHR-Tableau-Beweismethode vollständig bezüglich der Unerfüllbarkeit auch unendlicher bereichsbeschränkter Klauselmengen. Da jedes geschlossene PUHR-Tableau endlich ist, wird darin die PUHR-Regel nur mit endlich vielen Klauseln angewandt, und die entsprechende endliche Teilmenge von Klauseln ist unerfüllbar. Damit ist der Endlichkeitssatz für bereichsbeschränkte Klauseln eine einfache Folge aus diesem Vollständigkeitsergebnis.

Der Satz gilt auch für die Prädikatenlogik erster Stufe mit Gleichheit:

Beweis:

Hat jede endliche Teilmenge von S ein normales Modell, hat nach Satz 3.6.6 (1) auch jede endliche Teilmenge von S∪ ein Modell.

Nach dem Endlichkeitssatz besitzt folglich auch S∪ ein Modell M, also nach Satz 3.6.6 (2) auch ein normales Modell M'. Da S⊆S∪ , ist M' ein normales Modell von S.

Beweis:

Unmittelbare Folgerung aus Satz 4.9.1.

Mit dem Endlichkeits-/Kompaktheitssatz lassen sich viele bemerkenswerte Resultate beweisen. Es folgen einige Beispiele davon.

Ein gerichteter Graph ist ein Paar bestehend aus eine Menge von Knoten und einer zweistelligen Relation über der Knotenmenge. Die Paare von Knoten in dieser Relation nennt man Kanten. Ein Pfad ist eine endliche Folge N₀ ... N_n von Knoten, so dass (N_i-1,N_i) für 1≤i≤n eine Kante ist. Die Anzahl n der Kanten nennt man die Länge des Pfads. Ein gerichteter Graph heißt zusammenhängend, wenn es zu jedem Paar N,N' von Knoten einen Pfad gibt, der mit N beginnt und mit N' endet.

Beweis:

Sei ein Sprache der PL1S mit Gleichheit mit zwei Konstanten a und b und einem zweistelligen Relationssymbol k. Jede normale -Interpretation M entspricht einem Graph mit dem Universum von M als Knotenmenge und k^M als Kantenrelation. Alle Terme, insbesondere a und b, repräsentieren also Knoten. Offensichtlich entspricht jeder Graph einer solchen Interpretation.

Angenommen, es gäbe eine Menge Z von Formeln der PL1S, die den Zusammenhang ausdrückt. Genauer heißt das, dass eine normale -Interpretation genau dann ein Modell von Z ist, wenn sie einem Graph entspricht, in dem es einen Pfad gibt von dem Knoten, den a repräsentiert, zu dem Knoten, den b repräsentiert.

Nun betrachten wir folgende Formeln.

F₀	:=	¬(ab)
F₁	:=	¬k(a,b)
F₂	:=	¬∃x₁∧*(k(a,x₁,k(x₁,b))
F₃	:=	¬∃x₁∃x₂∧*(k(a, x₁),k(x₁,x₂),k(x₂,b))
F₄	:=	¬∃x₁∃x₂∃x₃∧*(k(a,x₁),k(x₁,x₂),k(x₂,x₃),k(x₃,b))
...
F_n	:=	¬∃x₁...∃x_n-1 ∧*(k(a,x₁),k(x₁,x₂),...,k(x_n-1 ,b))
...

Sei S₀:=F₀ und S_n+1:=S_n∪F_n+1 für alle n∈ und S*:=∪_{_n∈} S_n.

Erfüllt eine normale -Interpretation die Formel F_n, entspricht sie einem Graphen, in dem es keinen Pfad der Länge n zwischen den durch a und b repräsentierten Knoten gibt. Erfüllt sie die Formelmenge S_n, gibt es zwischen diesen Knoten keinen Pfad einer Länge ≤n. Erfüllt sie S*, gibt es keinen Pfad zwischen diesen Knoten.

Für jedes n∈ ist Z∪S_n erfüllbar: Jeder Graph, in dem es zwischen den betrachteten Knoten einen Pfad einer Länge >n gibt, entspricht einem normalen Modell. Damit hat auch jede endliche Teilmenge von Z∪S_n ein normales Modell, und somit auch jede endliche Teilmenge von Z∪S*.

Nach dem Endlichkeitssatz gibt es ein normales Modell von Z∪S*. In dem Graphen, der dieser Interpretation entspricht, gibt es aber keinen Pfad von dem Knoten, den a repräsentiert, zu dem Knoten, den b repräsentiert, im Widerspruch zu der Annahme über Z.

Beweis:

Sei ⁺ =\{0}. Sei eine Sprache der PL1S ohne Gleichheit mit abzählbar vielen einstelligen Relationssymbolen {p_i | i∈⁺}.

Angenommen, es gäbe eine Menge E von -Formeln, die die Endlichkeit ausdrückt. Das heißt, dass E von -Interpretation genau dann erfüllt wird, wenn diese Interpretation ein endliches Universum hat. Wir nehmen o.B.d.A. an, dass die Relationssymbole p_i nicht in E vorkommen.

Für alle n∈⁺ und für i∈{1, ..., n} sei
F_n:=∃x₁...∃x_n ∧*(G₁,G₂,...,G_n)
G_i:=∧*(¬p₁(x_i), ..., ¬p_i-1(x_i),p_i(x_i), ¬p_i+1(x_i), ..., ¬p_n(x_i))

Für jedes n∈⁺ wird F_n offensichtlich nur von Interpretationen erfüllt, deren Universen mindestens n Elemente enthalten.
S₁:={F₁} und S_n+1:=S_n∪{F_n+1} für n∈⁺ und S*:=∪_{n∈
⁺}S_n.
Offensichtlich wird S* nur von Interpretationen erfüllt, deren Universen unendlich sind.

Für jedes n∈

ist E∪S_n erfüllbar: Nach Annahme über E ist jede

-Interpretation, deren Universum endlich ist und mindestens n Elemente hat, ein Modell von E∪S_n . Damit hat auch jede endliche Teilmenge von E∪S* ein Modell, und somit auch jede endliche Teilmenge von E∪S*.

Nach dem Endlichkeitssatz gibt es ein Modell von E∪S*, was zusammen mit 2. der Annahme über E widerspricht.

In der Hoffnung, Satz 4.9.6 zu widerlegen, könnte man versuchen, folgendermaßen zu argumentieren: Für n∈⁺ sei

F_n=∀x₁ ... ∀ x_n+1∨*x_n+1 ...= x₁, x_n+1 ...= x₂, ..., x_n+1 ...= x_n)

Für jedes n∈

⁺ wird F_n offensichtlich nur von Interpretationen erfüllt, deren Universen höchstens n Elemente enthalten.

Die unendliche Disjunktion aller F_n für n∈⁺ würde die Endlichkeit ausdrücken, wenn sie eine Formel wäre. Aber das ist sie nicht.

Hier zeigt sich eine Asymmetrie in der PL1S: Eine unendliche Menge von Formeln ist ein Ersatz für die (nicht zulässige) unendliche Konjunktion aller dieser Formeln. Es gibt aber kein ähnliches Gegenstück zu einer unendlichen Disjunktion. Der Existenzquantor entspricht lediglich Disjunktionen unbestimmter, endlicher oder unendlicher, Länge.