Ein vollständiger Typ (auch vollständiger n-Typ) ist eine maximale konsistente Menge von Erster-Ordnung-Formeln mit Parametern in einer gegebenen Struktur oder über einer Parameterbasis, für ein festes Tupel von Variablen; er enthält für jede Formel in diesen Variablen entweder die Formel oder ihre Negation und beschreibt somit alle Erster-Ordnung-Eigenschaften, die ein Tupel relativ zur Parameterbasis erfüllen kann.

Prinzip

Maximale Konsistenz: Ein vollständiger Typ ist konsistent und enthält für jede relevante Formel mit Parametern eine Entscheidung (Formel oder Negation). Die Maximalität sorgt dafür, dass eine Erweiterung ohne Widerspruch nicht möglich ist und der Typ syntaktisch präzise das Verhalten des Tupels festlegt.

Demonstration

In einem algebraisch abgeschlossenen Körper K enthält der vollständige 1-Typ über der leeren Menge eines transzendenten Elements Formeln, die ausdrücken, dass x transzendent über dem Primkörper ist, und für jedes nichtverschwindende Polynom p die Formel 'p(x) ≠ 0'; diese Menge ist maximal konsistent und charakterisiert das transzendente Element.

Fehlanwendung

Ein konsistentes, aber nicht maximales Formularbündel als vollständigen Typ zu behandeln (Verwechslung mit partiellem Typ) oder anzunehmen, ein vollständiger Typ müsse in jedem Modell realisiert sein, obwohl er in manchen Modellen ausgelassen werden kann.

Konsequenz

Vollständige Typen entsprechen Punkten im Typraum (Stone-Raum); ihre Realisierbarkeit in einem Modell steuert modelltheoretische Phänomene wie Gesättigtheit, Auslassung von Typen und Klassifikationseigenschaften von Theorien.

Umkehrung

Ein partieller Typ ist eine nicht-maximale konsistente Formelmenge, die einige Formeln offenlässt; durch Umkehr der Maximalität entstehen mehrere kompatible Fortsetzungen statt einer eindeutigen Entscheidung.

Abgrenzung

Beschränkt auf Erster-Ordnung-Formeln in einer festen Sprache und ein gewähltes Variablen-Tupel; Vollständigkeit bezieht sich auf syntaktische Maximalität über einer bestimmten Parameterbasis und sagt nichts über die Realisierbarkeit in einem konkreten Modell oder über höherstufige Logiken aus.

Semantische Spannung

Spannung zwischen syntaktischer Maximalität (der Typ entscheidet jede Formel) und semantischer Realisierbarkeit (ob ein Modell ein Tupel enthält, das diese Menge erfüllt); ein syntaktisch vollständiger Typ kann in bestimmten Strukturen unerfüllt bleiben.

Synthese

Ein vollständiger Typ ist die maximale syntaktische Beschreibung der Erster-Ordnung-Eigenschaften eines potentiellen Tupels über einer Parameterbasis: er liefert eine eindeutige, konsistente Entscheidung zu jeder Formel in den gewählten Variablen und bildet zusammen mit Realisierung und topologischer Struktur die Grundlage vieler modelltheoretischer Konstruktionen.