Quelltext der Seite Typ (Modelltheorie)

In der [[Modelltheorie]] bezeichnet ein '''Typ''' eine Menge [[Prädikatenlogik erster Stufe|erst-stufiger]] [[Logische Formel|Formeln]] in einer Sprache <math>L</math> mit [[Freie Variable|freien Variablen]] <math>x_1, x_2, \ldots, x_n</math>, die keinen [[Widerspruchsfreiheit|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.

== Definition ==
Sei <math>\mathcal{M}</math> eine [[Struktur (erste Stufe)|Struktur]] für eine [[Elementare Sprache|Sprache]] <math>L</math> und <math>M</math> ihr Universum. Für alle Teilmengen <math>A \subseteq M</math> bezeichne <math>L(A)</math> die Sprache, die man aus <math>L</math> erhält, wenn man für jedes <math>a \in A</math> ein [[Konstante (Logik)|Konstantensymbol]] <math>c_a</math> hinzufügt, also <math>L(A) = L \cup \{c_a \mid a \in A\}</math>.

Die Konstantensymbole <math>c_a</math> werden in <math>\mathcal{M}</math> durch das Element <math>a</math> interpretiert, auch diese erweiterte Struktur werde mit <math>M</math> bezeichnet.

Ein 1-Typ (von <math>\mathcal{M}</math>) über <math>A</math> ist eine Menge <math>p(x)</math> von Formeln in <math>L(A)</math> mit höchstens einer freien Variablen <math>x</math> (daher 1-Typ), sodass für jede endliche Teilmenge <math>p_0(x) \subseteq p(x)</math> ein Element <math>b \in M</math> existiert mit <math>\mathcal{M} \models p_0(b) </math>, für das also alle Formeln in <math>p_0(x)</math> in <math>\mathcal{M}</math> erfüllt werden, wenn man für <math>x</math> das Element <math>b</math> einsetzt.

Analog ist ein <math>n</math>-Typ (von <math>\mathcal{M}</math>) über <math>A</math> eine Menge <math>p(x_1, \ldots, x_n) = p(\overline{x})</math> von <math>L(A)</math>-Formeln, sodass zu jeder endlichen Teilmenge <math>p_0(\overline{x}) \subseteq p(\overline{x})</math> Elemente <math>b_1, \ldots, b_n \in M</math> existieren mit <math>\mathcal{M}\models p_0(b_1, \ldots, b_n)</math>.

Ein Typ heißt '''vollständig''', falls er maximal bezüglich der Inklusion ist. Für einen vollständigen Typ <math>p(\overline{x})</math> gilt also für jedes <math>\phi(\overline{x}) \in L(A, \overline{x})</math> entweder <math>\phi(\overline{x}) \in p(\overline{x})</math> oder <math>\lnot\phi(\overline{x}) \in p(\overline{x})</math>. Ein Typ, der nicht vollständig ist, heißt partieller Typ. Partielle Typen können nach dem [[Satz von Lindenbaum]] (bzw. dem [[Lemma von Zorn]]) immer zu vollständigen Typen ergänzt werden.

== Begriffe ==
Ein <math>n</math>-Typ <math>p(\overline{x})</math> wird in <math>\mathcal{M}</math> realisiert, falls es ein Element <math>\overline{b} \in M^n</math> gibt mit <math>\mathcal{M} \models p(\overline{b})</math>. Nach dem [[Kompaktheitssatz (Logik)|Kompaktheitssatz]] gibt es zu jedem Typ eine [[elementare Erweiterung]] von <math>\mathcal{M}</math>, in der eine solche Realisierung existiert.
Wird ein vollständiger Typ von <math>\overline{b}</math> in <math>\mathcal{M}</math> realisiert, so bezeichnet man ihn als <math>tp_n^{\mathcal{M}}(\overline{b}/A)</math>, den vollständigen Typ von <math>\overline{b}</math> über <math>A</math>.

Ein Typ <math>p(\overline{x})</math> wird isoliert durch <math>\varphi</math>, falls die Formel <math>\varphi(\overline{x})</math> zum einen konsistent mit der zugrundeliegenden Theorie ist (<math>\{\varphi(\overline{x})\}</math> ist also ein (partieller) Typ) und zum anderen die Eigenschaft hat, alle Formeln in <math>p(\overline{x})</math> zu implizieren: <math>\forall \psi(\overline{x}) \in p(\overline{x}) (\varphi(\overline{x}) \rightarrow \psi(\overline{x}))</math>. Da <math>\varphi(\overline{x})</math> eine Realisierung in <math>\mathcal{M}</math> besitzt, gibt es ein Element <math>\overline{b} \in M^n</math>, sodass <math>\varphi(\overline{b})</math> in <math>\mathcal{M}</math> gilt, also realisiert <math>\overline{b}</math> den gesamten isolierten Typ. Insbesondere haben isolierte Typen in jeder elementaren Unterstruktur oder Erweiterung eine Realisierung.

== Beispiele ==
=== Unendlich große natürliche Zahlen ===
Sei <math>\mathcal{N}</math> ein Modell der natürlichen Zahlen mit Universum <math>\mathbb{N}</math> und der Sprache <math>L = \{\leq\}</math>, wobei <math>\leq</math> als die gewöhnliche Ordnung interpretiert wird. Dann ist <math>p(x) := \{ n \leq x \mid n \in \mathbb{N}\}</math> ein Typ von <math>\mathcal{N}</math> über <math>\mathbb{N}</math>: Nach Definition gilt ohnehin <math>\mathcal{N} \models \emptyset</math>. Für eine nichtleere endliche Teilmenge <math>p_0(x) \subseteq p(x)</math> bestimmen wir die größte natürliche Zahl <math>m_{p_0}</math>, die in <math>p_0</math> vorkommt und erhalten <math>\mathcal{N}\models p_0(m_{p_0})</math>.

Die Menge <math>p(x)</math> ist ein partieller Typ und sagt: „<math>x</math> ist größer als jede beliebige natürliche Zahl.“ Innerhalb des Universums von <math>\mathcal{N}</math> existiert kein solches Element, der Typ ist also nicht realisierbar in <math>\mathcal{N}</math>. Es gibt jedoch Strukturen <math>\mathcal{N}^*</math>, in denen er realisiert wird: Wir können etwa <math>\mathbb{N}\cup\mathbb{Z}'</math> als Universum nehmen, wobei <math>\mathbb{Z}'</math> eine zu <math>\mathbb{N}</math> disjunkte Kopie von <math>\mathbb{Z}</math> ist und <math>{\leq^*} := {\leq} \cup {\leq'} \cup (\mathbb{N} \times \mathbb{Z}')</math>. Also sind alle Zahlen aus <math>\mathbb{N}</math> kleiner als alle Zahlen aus <math>\mathbb{Z}'</math> und innerhalb der beiden Mengen gilt die übliche Ordnung.

<math>\mathcal{N}^*</math> ist eine elementare Erweiterung von <math>\mathcal{N}</math> und <math>\mathcal{N}^* \models p(0')</math>. Daher realisiert 0' den Typ <math>p(x)</math>. Auch in <math>\mathcal{N}^*</math> kann der Typ <math>p(x)</math> nicht isoliert werden, denn sonst wäre er bereits in der elementaren Unterstruktur <math>\mathcal{N}</math> isoliert und müsste somit dort realisiert werden.

Wir hätten auch einfach ein weiteres Element <math>c \notin \mathbb{N}</math> zu <math>\mathbb{N}</math> hinzufügen können und dieses zum größten Element machen können. Auch in dieser Struktur hätte <math>p(x)</math> eine Realisierung. Aber in diesem Fall würde <math>p(x)</math> durch <math>\forall y (y \leq x)</math> 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 <math>x</math>, die für <math>x = 2</math> wahr sind. Diese Menge enthält Formeln wie <math>x \ne 1 + 1 + 1</math>, <math>x \le 1 + 1 + 1 + 1 + 1</math>, <math>\exists y (y < x)</math>, <math>x = 1 \lor 1 = 1</math> und <math>1 + 1 + 1 = 1 + 1 + 1</math>. Dies ist ein Beispiel für einen isolierten Typ, da die Formel <math>x = 1 + 1</math> alle anderen Formeln impliziert, die für die Zahl 2 gelten.

=== Hyperreelle Zahlen ===
Der Typ <math>\{x > 1, x > 1 + 1, x > 1 + 1 + 1, \ldots\}</math> wird innerhalb der reellen Zahlen nach dem [[Archimedisches Axiom|archimedischen Axiom]] nicht realisiert. Eine Erweiterung, in der dieser Typ realisiert wird, bilden die [[Hyperreelle Zahl|hyperreellen Zahlen]]. Wenn dieser Typ durch <math>c</math> realisiert wird, wird automatisch der Typ der unendlich kleinen Zahlen durch <math>1/c</math> realisiert.

== Stone-Raum ==
Auf der Menge <math>S_n(A)</math> der vollständigen <math>n</math>-Typen über <math>A</math> lässt sich eine [[Topologischer Raum|Topologie]] definieren:

Bezeichnet man mit <math>[\varphi]</math> die Menge aller vollständigen <math>n</math>-Typen, die die Formel <math>\varphi</math> als Element enthalten, und stehen <math>\top</math> und <math>\bot</math> für eine wahre bzw. falsche Aussage, so gilt
# <math>S_n(A) = [\top]</math>, <math>\emptyset = [\bot]</math>
# <math>[\varphi] \cup [\psi] = [\varphi \lor \psi]</math>
# <math>[\varphi] \cap [\psi] = [\varphi \land \psi]</math>
# <math>S_n(A) \setminus [\varphi] = [\lnot\varphi]</math>
Insbesondere bilden die <math>[\varphi]</math> die [[Basis (Topologie)|Basis]] einer Topologie. Dies liefert den Stone-Raum. Dieser ist [[Kompakter Raum|kompakt]], [[Hausdorff-Raum|hausdorffsch]] und [[Total unzusammenhängender Raum|total unzusammenhängend]]. Isolierte Typen entsprechen dabei gerade den [[Isolierter Punkt|isolierten Punkten]].

=== Beispiel ===
Die vollständige Theorie [[Algebraischer Abschluss|algebraisch abgeschlossener Körper]] der [[Charakteristik (Algebra)|Charakteristik]] 0 besitzt [[Quantorenelimination]], sodass man leicht alle 1-Typen (über der leeren Menge) bestimmen kann:
* Typen [[Algebraische Zahl|algebraischer Zahlen]]: Diese Typen sind offene Punkte im Stone-Raum. Die isolierende Formel ergibt sich aus dem [[Minimalpolynom (Körpertheorie)|Minimalpolynom]]. Zwei algebraische Zahlen haben genau dann den gleichen Typ, wenn sie [[Algebraisch konjugiert|konjugiert]] 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 denselben 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 <math>\omega</math>-[[Saturiertheit (Modelltheorie)|saturiert]]. Allgemeiner kann man den Begriff für beliebige unendliche Kardinalzahlen <math>\kappa</math> definieren: Ein Modell heißt <math>\kappa</math>-saturiert, falls alle Typen über Mengen mit Mächtigkeit kleiner <math>\kappa</math> realisiert werden. Ein Modell <math>\mathcal{M}</math> heißt saturiert, falls es <math>\mid\mathcal{M}\mid</math>-saturiert ist.

Umgekehrt macht das {{lang|en|''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 <math>p</math> ein nicht isolierter Typ in einer abzählbaren Sprache. Dann gibt es ein abzählbares Modell, in dem <math>p</math> nicht realisiert wird. Allgemeiner kann man auch zeigen, dass sogar eine abzählbare Menge nicht isolierter Typen ausgelassen werden kann.

== Literatur ==
* [[Wilfrid Hodges]]: ''Model theory'', Cambridge University Press, 1993, ISBN 0-521-30442-3.

== Weblinks ==
* Martin Ziegler: [http://home.mathematik.uni-freiburg.de/ziegler/skripte/modell1.pdf Skript Modelltheorie 1] (PDF; 649&nbsp;kB)

[[Kategorie:Modelltheorie]]