Eine modelltheoretische Konstruktion in der modalen Logik, die ein (möglicherweise unendliches) Kripke‑Modell durch eine aus einer endlichen Formelmenge definierte Äquivalenz quotien­tiert, so dass das resultierende endliche Quotientenmodell (die Filtration) die Wahrheit jeder Formel in dieser endlichen Menge erhält und so Argumente über endliche Modelle für Erfüllbarkeit und Vollständigkeit ermöglicht.

Prinzip

Zustände nach ihren Bewertungen auf der relevanten endlichen Menge von Unterformeln partitionieren und äquivalente Zustände zu Äquivalenzklassen zusammenschrumpfen, dabei Nachfolgerrelationen zwischen Klassen so definieren, dass die Erfüllbarkeit der gewählten Formeln erhalten bleibt und die Modellgröße reduziert wird.

Demonstration

Um die Endlichkeits­eigenschaft für eine normale modale Logik auf einer eingeschränkten Klasse von Rahmen zu zeigen, nimmt man ein Modell, das eine Formel erfüllt, sammelt die endliche Menge der Unterformeln, konstruiert die Filtrationsäquivalenz über Zustände, die in diesen Unterformeln übereinstimmen, und bildet das Quotientenmodell, das endlich ist und die ursprüngliche Formel weiterhin erfüllt.

Fehlanwendung

Anzunehmen, eine Filtration erhalte die Wahrheit von Formeln außerhalb der gewählten Unterformelmenge, oder die Standardfiltration anzuwenden, ohne Rahmenbedingungen (z. B. Transitivität oder Symmetrie) zu berücksichtigen, die das Quotient verletzen könnte, was zu falschen Vollständigkeits‑ oder Rahmen­erhaltungsbehauptungen führt.

Konsequenz

Gilt die Filtration, liefert sie für erfüllbare Formeln endliche Modelle (Endlichkeits­eigenschaft), vereinfacht Vollständigkeitsbeweise durch Reduktion kanonischer Modelle auf endliche Quotienten und liefert algorithmische endliche Zeugen für Erfüllbarkeit in vielen modalen Systemen.

Umkehrung

Das Gegenstück ist das Aufrollen (Unravelling) in einen baumartigen Aufbau, das ein Modell in eine baumartige Struktur verwandelt, lokale Wahrheiten erhält, es aber möglicherweise erweitert; diese Umkehr beleuchtet den Trade‑off zwischen Kollaps zur Endlichkeit und Expansion zur baumartigen Regularität.

Abgrenzung

Filtration ist an eine gewählte endliche Formelmenge gebunden und an Logiken, bei denen Unterformel‑Erhalt und Rahmeneigenschaften mit Quotientbildung kompatibel sind; sie kann fehlschlagen oder Modifikation erfordern bei Logiken mit globalen Modalitäten, Fixpunktoperatoren, Hybridfeatures oder wenn Rahmenbedingungen nicht durch den Quotienten erhalten bleiben.

Semantische Spannung

Es besteht Spannung zwischen Filtration zur Erzeugung kleiner kanonischer Modelle und automaten‑theoretischen oder algebraischen Methoden, die Modellkollaps vermeiden; ebenso zwischen syntaktischer Unterformelerhaltung und dem Verlust anderer semantischer Rahmenbeschränkungen im Quotienten.

Synthese

Die Filtrationsmethode kollabiert ein Modell entlang der durch eine endliche Formelmenge induzierten Äquivalenz, um ein kleineres Modell zu erzeugen, das die Wahrheit dieser Formeln erhält; sie ist eine konkrete semantische Technik zur Erzielung von Endlichkeitsresultaten und konstruktiven Erfüllbarkeitszeugen, wobei Rahmenbedingungen und Sprachmerkmale sorgfältig zu behandeln sind.