Ein Satz, der Voraussetzungen angibt, unter denen eine abzählbare konsistente erste‑Ordnungstheorie ein Modell besitzt, das eine angegebene Menge von nicht‑prinzipiellen (nicht isolierten) Typen auslässt; klassisch formuliert für abzählbare Sprachen und abzählbare Familien solcher Typen.

Prinzip

Bei abzählbarer Sprache und konsistenter Theorie kann man, sofern die auszulassenden Typen nicht‑prinzipiell und die Familie abzählbar ist, ein Modell konstruieren, das jede Typen in der Familie nicht realisiert; dies geschieht durch Henkin‑Konstruktionen oder Baire‑Kategorie/Topologie‑Argumente im Typenraum.

Demonstration

Sei T eine abzählbare konsistente Theorie und {p_n(x)} eine abzählbare Folge nicht‑prinzipieller 1‑Typen. Durch Erweiterung von T um Henkin‑Konstanten und schrittweises Sicherstellen der Nichtrealisierung jedes p_n (oder durch Konstruktion einer komagre Menge von Komplettierungen im Stone‑Raum, die alle p_n auslassen) erhält man ein abzählbares Modell von T, das keinen der p_n realisiert.

Fehlanwendung

Die Behauptung, der Satz gelte für überabzählbare Sprachen oder für überabzählbare Typenmengen oder dass er prinzipielle Typen auslassen könne, ist irreführend; Kompaktheit und Kardinalitätsgründe können Realisierung erzwingen.

Konsequenz

Ermöglicht präzise Kontrolle bei Modellkonstruktionen: Existenz von Modellen mit vorgegebenen Auslassungen; nützlich zur Herstellung von Modellen mit bestimmten algebraischen oder kombinatorischen Eigenschaften und zur Trennung von Modellklassen nach den realisierten Typen.

Umkehrung

Die invertierte Lage ist, dass Kompaktheit bewirken kann, dass bestimmte Typen in jedem Modell realisiert werden (z. B. prinzipielle Typen durch endliche Diagramme), also statt Auslassung die Unvermeidbarkeit der Realisierung vorliegt.

Abgrenzung

Gilt hauptsächlich für erste‑Ordnungstheorien in abzählbaren Sprachen und für nicht‑prinzipielle Typen (häufig ebenfalls abzählbar). Der Satz lässt sich nicht ohne Weiteres auf beliebige Kardinalitäten oder auf Typenfamilien ausdehnen, deren Nichtrealisierung die Kompaktheit verletzen würde.

Semantische Spannung

Spannung zwischen diesem Satz und der Kompaktheit: Kompaktheit fördert lokale Konsistenz und damit Realisierungen, während Auslassungsargumente globalen Aufbau nutzen; ferner Konflikt mit stärkeren Konzepten wie dem Auslassen von Hyper‑Imaginären, wo der klassische Satz nicht ausreicht.

Synthese

Der Satz über das Auslassen von Typen liefert eine abzählbarkeitsbasierte Methode, Modelle zu konstruieren, die bestimmte nicht‑prinzipielle Typen nicht realisieren, und balanciert Kompaktheitszwänge gegen konstruktive oder topologische Mittel zur selektiven Auslassung.