Ein Verfahren in modalen und verwandten Logiken, das ein kanonisches Modell konstruiert, dessen Welten maximal konsistente Mengen (oder saturierte Theorien) von Formeln sind und dessen Zugangsrelationen aus syntaktischen Bedingungen definiert sind; verwendet, um Vollständigkeitssätze zu beweisen, indem ein Wahrheitslemma aufgebaut wird, das Formeln mit Mitgliedschaft in Welten verknüpft.

Prinzip

Verwenden Sie eine Lindenbaum-ähnliche Maximalerweiterung (oder Saturierung), um konsistente Mengen zu maximal konsistenten zu erweitern, definieren Sie Welten als diese Mengen und legen Sie Relationen so fest, dass modale Formeln erhalten bleiben; das Wahrheitslemma wird dann durch Induktion über die Formelnstruktur bewiesen und zeigt, dass eine Formel in einer Welt genau dann gilt, wenn sie zur maximal konsistenten Menge gehört.

Demonstration

Für die normale modale Logik K: Beginnen Sie mit einer konsistenten Menge Γ, erweitern Sie sie zu einer maximal K-konsistenten Menge w, nehmen Sie als kanonischen Rahmen alle solchen maximalen Mengen, definieren Sie wRv genau dann, wenn für jedes □φ ∈ w gilt, dass φ ∈ v, und beweisen Sie das Wahrheitslemma, um zu folgern, dass jede K-valide Formel im kanonischen Modell valide ist und somit Vollständigkeit gilt.

Fehlanwendung

Zu glauben, das kanonische Modell sei klein oder besitze gewünschte Rahmeneigenschaften (z. B. endlich, wohlgeordnet oder erfülle spezielle Rahmenbedingungen), ohne zu prüfen, dass die Axiome der Logik diese Eigenschaften erzwingen; die Konstruktion fälschlich auf nicht-normale Systeme anzuwenden, ohne die Definition der Zugangsrelation anzupassen.

Konsequenz

Ermöglicht Vollständigkeits- (und oft Korrespondenz-)Ergebnisse: Ist eine Formel nicht beweisbar, so ist ihre Negation konsistent und erweitert sich zu einer Welt im kanonischen Modell, die die Formel falsifiziert und so ein Gegenmodell liefert; klärt außerdem den Zusammenhang zwischen syntaktischen Axiomen und semantischen Rahmenbedingungen.

Umkehrung

Im Gegensatz zur direkten Modellkonstruktion oder Filtration: Kanonische Modelle sind syntaktisch geprägt und oft groß oder unendlich, während Filtration endliche Approximationen erzeugt, die die Wahrheit für eine begrenzte Sprache erhalten — das Wechseln zwischen beiden tauscht allgemeine Vollständigkeit gegen Endlichkeit oder Entscheidbarkeit ein.

Abgrenzung

Wirksam für normale modale Logiken und viele verwandte Systeme, in denen maximale konsistente Mengen und die definierte Zugangsrelation die erforderlichen Eigenschaften erfüllen; sie versagt oder benötigt Modifikationen für Logiken ohne anwendbares Maximierungslemma, für bestimmte nicht-normale Logiken oder wenn man die Endlichkeits-Eigenschaft ohne weitere Methoden haben möchte.

Semantische Spannung

Spannung zur Filtration und zu bisimulationsgenerierten Modellen: Kanonische Modelle sind maximal syntaktisch und oft nicht endlich; Filtration strebt endliche Modelle an, die bestimmte Formeln bewahren, und Bisimulation erfasst modale Invarianz — die Wahl hängt davon ab, ob man Vollständigkeit, Endlichkeit oder Invarianz benötigt.

Synthese

Die kanonische Modellkonstruktion verwandelt syntaktische Konsistenz in semantische Gegenbeispiele, indem sie maximal konsistente Mengen als Welten auffasst und modale Operatoren in Zugangsrelationen kodiert; das Wahrheitslemma verbindet dann Syntax und Semantik und liefert Vollständigkeit sowie Einsicht, wie Axiome Rahmenbedingungen erzwingen.