Die formale Relation |= (oder ⊧) zwischen einer Struktur (oder Modell), einer Variablenzuweisung (falls anwendbar) und einer Formel, die genau dann gilt, wenn die Formel in dieser Struktur unter jener Zuweisung gemäß den semantischen Regeln der Sprache wahr ist.

Prinzip

Erfüllung wird induktiv über die Formstruktur definiert: atomare Formeln werden durch Anwendung der Interpretation der Struktur auf Terme und Relationen ausgewertet; boolesche Junktoren kombinieren Wahrheitswerte auf übliche Weise; Quantoren quantifizieren über Elemente des Trägers mittels Zuweisungsupdates; modale und andere Operatoren verwenden die jeweiligen semantischen Primitiven (z. B. Zugänglichkeit bei Kripke‑Semantik).

Demonstration

In der Prädikatenlogik: Für Struktur M und Zuweisung g gilt M,g |= ∃x P(x) genau dann, wenn es ein Element a in der Domäne von M gibt mit M,g[x↦a] |= P(x). In der propositionalen Kripke‑Semantik gilt M,w |= □φ genau dann, wenn für alle v mit wRv gilt M,v |= φ.

Fehlanwendung

Die Erfüllungsrelation mit syntaktischer Beweisbarkeit verwechseln (|= mit ⊢), die Rolle von Zuweisungen für freie Variablen ignorieren oder Erfüllungsklauseln einer Logik auf eine andere anwenden, ohne die semantischen Primitiven anzupassen.

Konsequenz

Die Erfüllungsrelation bildet die Grundlage modelltheoretischer Begriffe wie logische Folge, Konsequenz, Gültigkeit, elementare Äquivalenz und Eigenschaftsübertragungen zwischen Strukturen; sie ist die formale Brücke zwischen Syntax und semantischer Wahrheit.

Umkehrung

Beweisbarkeit (⊢) ist die Umkehr: eine syntaktische Relation zwischen Formeln (und ggf. Prämissen) und Konklusionen innerhalb eines deduktiven Systems, nicht eine Auswertung in Modellen und Zuweisungen; Vollständigkeitssätze verknüpfen die beiden, doch sie bleiben unterschiedliche Konzepte.

Abgrenzung

Gilt nur, wenn eine präzise semantische Interpretation definiert ist (Strukturen, Bewertungen, Träger); deckt keine informellen Wahrheitsbegriffe, pragmatische Interpretationen oder Beweissuchprozesse ab, sofern diese nicht als Strukturen und Relationen formalisiert sind.

Semantische Spannung

Spannung zwischen modelltheoretischer Erfüllung und proof‑theoretischer Folgerung: Erfüllung ist semantisch und referenzerhaltend, Beweisbarkeit ist syntaktisch und regelbasiert; praktisch entstehen Verwirrungen, wenn Werkzeuge Wahrheit in einem Modell mit dem Beweis eines Theorems gleichsetzen.

Synthese

Die Erfüllungsrelation ist das induktiv definierte semantische Prädikat, das genau angibt, wann eine Formel in einer Struktur unter einer Zuweisung erfüllt ist; sie bildet die Grundlage der Modelltheorie und präziser Aussagen über Wahrheit, Konsequenz und Äquivalenz.