- Typ (Modelltheorie)
-
In der Modelltheorie bezeichnet ein Typ eine Menge erst-stufiger Formeln in einer Sprache L mit freien Variablen
, die keinen Widerspruch implizieren. Anschaulich gesprochen legt ein Typ bestimmte Eigenschaften fest, die ein Element haben soll. Ein solches Element muss nicht unbedingt existieren, aber die Eigenschaften dürfen nicht im Widerspruch zueinander stehen, damit zumindest in einer größeren Struktur ein solches Element gefunden werden kann. Auch drückt ein Typ aus, welche Elemente sich nicht durch erst-stufige Formeln unterscheiden lassen.
Inhaltsverzeichnis
Definition
Sei
eine Struktur für eine Sprache L und M ihr Universum. Für alle Teilmengen
bezeichne L(A) die Sprache, die man aus L erhält, wenn man für jedes
ein Konstantensymbol ca hinzufügt, also
.
Ein 1-Typ (von
) über A ist eine Menge p(x) von Formeln in L(A) mit höchstens einer freien Variablen x (daher 1-Typ), sodass für jede endliche Teilmenge
ein Element
existiert mit
, für das also alle Formeln in p0(x) in
erfüllt werden, wenn man für x das Element b einsetzt.
Analog ist ein n-Typ (von
) über A eine Menge
von L(A)-Formeln, sodass zu jeder endlichen Teilmenge
Elemente
existieren mit
.
Ein Typ heißt vollständig, falls er maximal bezüglich der Inklusion ist. Für einen vollständigen Typ
gilt also für jedes
entweder
oder
. Ein Typ, der nicht vollständig ist, heißt partieller Typ. Partielle Typen können nach dem Lemma von Zorn immer zu vollständigen Typen ergänzt werden.
Begriffe
Ein n-Typ
wird in
realisiert, falls es ein Element
gibt mit
. Nach dem Kompaktheitssatz gibt es zu jedem Typ eine elementare Erweiterung von
, in der eine solche Realisierung existiert. Wird ein vollständiger Typ von
in
realisiert, so bezeichnet man ihn als
, den vollständigen Typ von
über A.
Ein Typ
wird isoliert durch φ, falls die Formel
zum einen konsistent mit der zugrundeliegenden Theorie ist (
ist also ein (partieller) Typ) und zum anderen die Eigenschaft hat, alle Formeln in
zu implizieren:
. Da
eine Realisierung in
besitzt, gibt es ein Element
, sodass
in
gilt, also realisiert
den gesamten isolierten Typ. Insbesondere haben isolierte Typen in jeder elementaren Unterstruktur oder Erweiterung eine Realisierung.
Beispiele
Unendlich große natürliche Zahlen
Sei
ein Modell der natürlichen Zahlen mit Universum
und der Sprache
, wobei
als die gewöhnliche Ordnung interpretiert wird. Dann ist
ein Typ von
über
: Nach Definition gilt ohnehin
. Für eine nichtleere endliche Teilmenge
bestimmen wir die größte natürliche Zahl
, die in p0 vorkommt und erhalten
.
Die Menge p(x) ist ein partieller Typ und sagt: „x ist größer als jede beliebige natürliche Zahl.“ Innerhalb des Universums von
existiert kein solches Element, der Typ ist also nicht realisierbar in
. Es gibt jedoch Strukturen
, in denen er realisiert wird: Wir können etwa
als Universum nehmen, wobei
eine disjunkte Kopie von
ist, und
, also alle Zahlen aus
kleiner sind als alle Zahlen aus
und innerhalb der beiden Mengen die übliche Ordnung gilt.
ist eine elementare Erweiterung von
und
. Daher realisiert 0' den Typ p(x). Auch in
kann der Typ p(x) nicht isoliert werden, denn sonst wäre er bereits in der elementaren Unterstruktur
isoliert und müsste somit dort realisiert werden.
Wir hätten auch einfach ein weiteres Element
zu
hinzufügen können und dieses zum größten Element machen können. Auch in dieser Struktur hätte p(x) eine Realisierung. Aber in diesem Fall würde p(x) durch
isoliert. Damit kann diese Erweiterung nicht elementar sein.
Typ der natürlichen Zahl 2
Der vollständige Typ der Zahl 2 über der leeren Menge in der Theorie der natürlichen Zahlen ist die Menge aller Formeln mit höchstens einer freien Variablen x, die für x = 2 wahr sind. Diese Menge enthält Formeln wie
,
,
,
und 1 + 1 + 1 = 1 + 1 + 1. Dies ist ein Beispiel für einen isolierten Typ, da die Formel x = 1 + 1 alle anderen Formeln impliziert, die für die Zahl 2 gelten.
Wurzel aus 2
In der Theorie geordneter Körper können die beiden Formeln
und
0 \and y^2 > 2) \implies y > x)" border="0"> zu einem vollständigen Typ ergänzt werden. Dieser Typ wird in den rationalen Zahlen nicht realisiert, wohl aber in den reellen Zahlen (durch
).
Hyperreelle Zahlen
Der Typ
1, x > 1 + 1, x > 1 + 1 + 1, \ldots\}" border="0"> wird innerhalb der reellen Zahlen nach dem archimedischen Axiom nicht realisiert. Eine Erweiterung, in der dieser Typ realisiert wird, bilden die hyperreellen Zahlen. Nimmt man zusätzlich alle positiven reellen Zahlen als Parameter hinzu, so kann man den Typ
angeben, der von infinitesimalen Elementen realisiert wird.
Stone-Raum
Auf der Menge Sn(A) der vollständigen n-Typen über A lässt sich eine Topologie definieren:
Bezeichnet man mit [φ] die Menge aller vollständigen n-Typen, die die Formel φ als Element enthalten, und stehen
und
für eine wahre bzw. falsche Aussage, so gilt
,
Insbesondere bilden die
die Basis einer Topologie. Dies liefert den Stone-Raum. Dieser ist kompakt, hausdorffsch und total unzusammenhängend. Isolierte Typen entsprechen dabei gerade den isolierten Punkten.
Beispiel
Die vollständige Theorie algebraisch abgeschlossener Körper der Charakteristik 0 besitzt Quantorenelimination, sodass man leicht alle Typen bestimmen kann:
- Typen algebraischer Zahlen: Diese Typen sind offene Punkte im Stone-Raum. Die isolierende Formel ergibt sich aus dem Minimalpolynom. Zwei algebraische Zahlen haben genau dann den gleichen Typ, wenn sie konjungiert sind, also das gleiche Minimalpolynom besitzen.
- Der Typ der transzendenten Elemente: Dieser Typ ist als Punkt im Stone-Raum nicht offen. Alle transzendenten Elemente haben den selben Typ, dieser besagt für jedes Polynom außer dem 0-Polynom, dass das Element keine Nullstelle des Polynoms ist.
Realisierungen von Typen in Modellen
Während isolierte Typen in jedem Modell eine Realisierung besitzen, hängt es bei den anderen Typen vom Modell ab, ob sie realisiert werden oder nicht. Es ist daher naheliegend Modelle zu untersuchen, in denen besonders viele oder besonders wenige Typen realisiert werden.
Ein Modell, das alle Typen über endlichen Mengen realisiert, heißt ω-saturiert. Allgemeiner kann man den Begriff für beliebige unendliche Kardinalzahlen κ definieren: Ein Modell heißt κ-saturiert, falls alle Typen über Mengen mit Mächtigkeit kleiner κ realisiert werden. Ein Modell
heißt saturiert, falls es
-saturiert ist.
Umgekehrt macht das Omitting Types Theorem (im Deutschen selten auch als Typenvermeidungssatz bezeichnet) die Aussage, dass es Modelle gibt, in denen ein vorgegebener Typ keine Realisierung besitzt. Man sagt, dass der Typ vom Modell ausgelassen oder vermieden wird: Sei p ein nicht isolierter Typ in einer abzählbaren Sprache. Dann gibt es ein abzählbares Modell, in dem p nicht realisiert wird. Allgemeiner kann man auch zeigen, dass sogar eine ganze unendliche Folge nicht isolierter Typen ausgelassen werden kann.
Literatur
- Wilfrid Hodges: Model theory, Cambridge University Press, 1993, ISBN 0-521-30442-3.
Weblinks
- Martin Ziegler: Skript Modelltheorie 1 (PDF)
Wikimedia Foundation.