Endlichkeitssatz

Der Endlichkeitssatz, auch Kompaktheitssatz genannt, ist einer der wichtigsten Sätze der Aussagenlogik und der Prädikatenlogik erster Stufe. Er besagt: Eine (möglicherweise unendliche) Formelmenge X ist genau dann erfüllbar (d.h. hat ein Modell), wenn jede endliche Teilmenge von X erfüllbar ist. Für die Logik der 2. Stufe gilt dieser Satz nicht.

Eine wichtige Folgerung aus dem Kompaktheitssatz ist, dass jede (möglicherweise unendliche) Formelmenge X, die beliebig große Modelle hat, auch ein unendliches Modell hat. Mit dieser Folgerung ist häufig die Axiomatisierbarkeit von Klassen endlicher L-Strukturen widerlegbar.

Beweis

Für die Prädikatenlogik erster Stufe ergibt sich der Kompaktheitssatz als Korollar aus dem Gödel'schen Vollständigkeitssatz sowie als Folgerung aus dem Satz von Herbrand. Dementsprechend kurz gestaltet sich auch der Beweis:

„$\Rightarrow$“: Angenommen, X hat ein Modell. Dann ist dieses (trivialerweise) auch ein Modell einer jeden endlichen Teilmenge von X.

„$\Leftarrow$“: Angenommen, jede endliche Menge $X_\text{fin} \subseteq X$ besitzt ein Modell. Zur Erzeugung eines Widerspruchs wird angenommen, X habe kein Modell. Dann ist aus X in einem vollständigen und korrekten formalen System ein Widerspruch (z.B. $\exists x: x \neq x$) herleitbar (Vollständigkeitssatz). Da eine Herleitung in einem formalen System (nach Definition) endlich ist, können in dieser Herleitung auch nur endlich viele Formeln aus X verwendet worden sein. Also ist aus einer endlichen Teilmenge von X ein Widerspruch herleitbar, und diese besitzt somit kein Modell (Korrektheitssatz). Widerspruch. Also besitzt X doch ein Modell.

Im Kern des Beweises steht das folgende Ergebnis, das direkt aus dem Gödel'schen Vollständigkeitssatz folgt: Folgt eine Formel φ aus einer Formelmenge X, so gibt es eine endliche Menge $X_\text{fin} \subseteq X$, sodass φ aus X_fin folgt. ($X \models \varphi \Rightarrow$ es gibt endliches $X_\text{fin} \subseteq X$ mit $X_\text{fin}\models \varphi$).

Ein gänzlich anderer Beweis, der auf den Begriff der syntaktischen Herleitbarkeit und auch auf den Vollständigkeitssatz verzichtet, ergibt sich in der Modelltheorie aus dem Satz von Łoś.

Weblinks

Vorlesungsfolien zur Aussagenlogik der TU Dresden von Steffen Hölldobler (Endlichkeitssatz mit Beweis ab S.86)