Type (model theory)

In model theory , a type denotes a set of first-order formulas in a language with free variables that do not imply a contradiction . To put it clearly, a type defines certain properties that an element should have. Such an element does not necessarily have to exist, but the properties must not contradict each other so that such an element can at least be found in a larger structure. A type also expresses which elements cannot be differentiated by first-level formulas. ${\displaystyle L}$ ${\displaystyle x_{1},x_{2},\ldots ,x_{n}}$

definition

Be a structure for a language and its universe. For all subsets denote the language that you made are obtained when each one constant symbol adds so . ${\displaystyle {\mathcal {M}}}$ ${\displaystyle L}$ ${\displaystyle M}$ ${\displaystyle A\subseteq M}$ ${\displaystyle L(A)}$ ${\displaystyle L}$ ${\displaystyle a\in A}$ ${\displaystyle c_{a}}$ ${\displaystyle L(A)=L\cup \{c_{a}\mid a\in A\}}$

The constant symbols are interpreted by the element ; this extended structure is also referred to with . ${\displaystyle c_{a}}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle a}$ ${\displaystyle M}$

A 1-type (of ) over is a set of formulas in with at most one free variable (hence 1-type), so that for every finite subset there is an element with , for which all formulas in in are satisfied if one for the Element sets in. ${\displaystyle {\mathcal {M}}}$ ${\displaystyle A}$ ${\displaystyle p(x)}$ ${\displaystyle L(A)}$ ${\displaystyle x}$ ${\displaystyle p_{0}(x)\subseteq p(x)}$ ${\displaystyle b\in M}$ ${\displaystyle {\mathcal {M}}\models p_{0}(b)}$ ${\displaystyle p_{0}(x)}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle x}$ ${\displaystyle b}$

Analog is a -type (of ) over a set of -formulas, so that for every finite subset there are elements with . ${\displaystyle n}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle A}$ ${\displaystyle p(x_{1},\ldots ,x_{n})=p({\overline {x}})}$ ${\displaystyle L(A)}$ ${\displaystyle p_{0}({\overline {x}})\subseteq p({\overline {x}})}$ ${\displaystyle b_{1},\ldots ,b_{n}\in M}$ ${\displaystyle {\mathcal {M}}\models p_{0}(b_{1},\ldots ,b_{n})}$

A type is called complete if it is maximal in terms of inclusion. For a complete type , either or applies to each . A type that is not complete is called a partial type. According to Lindenbaum's theorem (or Zorn's lemma ), partial types can always be added to complete types. ${\displaystyle p({\overline {x}})}$ ${\displaystyle \phi ({\overline {x}})\in L(A,{\overline {x}})}$ ${\displaystyle \phi ({\overline {x}})\in p({\overline {x}})}$ ${\displaystyle \lnot \phi ({\overline {x}})\in p({\overline {x}})}$

Terms

A type is implemented in, if there is an element with . According to the compactness theorem, there is an elementary extension of for every type in which such a realization exists. If a full type of in is realized, it is called , the full type of about . ${\displaystyle n}$ ${\displaystyle p({\overline {x}})}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle {\overline {b}}\in M^{n}}$ ${\displaystyle {\mathcal {M}}\models p({\overline {b}})}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle {\overline {b}}}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle tp_{n}^{\mathcal {M}}({\overline {b}}/A)}$ ${\displaystyle {\overline {b}}}$ ${\displaystyle A}$

One type is isolated by , if the formula for a is consistent with the underlying theory ( is therefore a (partial) type) and the other has the property of any formulas in imply to: . Since a realization has in, there is an element such that in holds, i.e. realizes the entire isolated type. In particular, isolated types have a realization in every elementary substructure or extension. ${\displaystyle p({\overline {x}})}$ ${\displaystyle \varphi }$ ${\displaystyle \varphi ({\overline {x}})}$ ${\displaystyle \{\varphi ({\overline {x}})\}}$ ${\displaystyle p({\overline {x}})}$ ${\displaystyle \forall \psi ({\overline {x}})\in p({\overline {x}})(\varphi ({\overline {x}})\rightarrow \psi ({\overline {x}}))}$ ${\displaystyle \varphi ({\overline {x}})}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle {\overline {b}}\in M^{n}}$ ${\displaystyle \varphi ({\overline {b}})}$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle {\overline {b}}}$

Examples

Infinitely large natural numbers

Let be a model of natural numbers with universe and language , interpreting as the ordinary order. Then there is a type of over : By definition, applies anyway . For a non-empty finite subset , we determine the greatest natural number that occurs in and is preserved . ${\displaystyle {\mathcal {N}}}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle L=\{\leq \}}$ ${\displaystyle \leq }$ ${\displaystyle p(x):=\{n\leq x\mid n\in \mathbb {N} \}}$ ${\displaystyle {\mathcal {N}}}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle {\mathcal {N}}\models \emptyset }$ ${\displaystyle p_{0}(x)\subseteq p(x)}$ ${\displaystyle m_{p_{0}}}$ ${\displaystyle p_{0}}$ ${\displaystyle {\mathcal {N}}\models p_{0}(m_{p_{0}})}$

The set is a partial type and says: “ is greater than any natural number.” There is no such element within the universe of , so the type cannot be realized in . However, there are structures in which it is realized: We can take as a universe, for example , with a too disjoint copy of and . So all numbers from are smaller than all numbers from and the usual order applies within the two sets. ${\displaystyle p(x)}$ ${\displaystyle x}$ ${\displaystyle {\mathcal {N}}}$ ${\displaystyle {\mathcal {N}}}$ ${\displaystyle {\mathcal {N}}^{*}}$ ${\displaystyle \mathbb {N} \cup \mathbb {Z} '}$ ${\displaystyle \mathbb {Z} '}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle {\leq ^{*}}:={\leq }\cup {\leq '}\cup (\mathbb {N} \times \mathbb {Z} ')}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {Z} '}$

${\displaystyle {\mathcal {N}}^{*}}$is an elementary extension of and . Hence, 0 'implements the type . The type cannot be isolated in either, otherwise it would already be isolated in the elementary substructure and would therefore have to be implemented there. ${\displaystyle {\mathcal {N}}}$ ${\displaystyle {\mathcal {N}}^{*}\models p(0')}$ ${\displaystyle p(x)}$ ${\displaystyle {\mathcal {N}}^{*}}$ ${\displaystyle p(x)}$ ${\displaystyle {\mathcal {N}}}$

We could have just one more element to add and make the biggest element of this. Also in this structure would have a realization. But in this case it would be isolated by. This extension cannot therefore be elementary. ${\displaystyle c\notin \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle p(x)}$ ${\displaystyle p(x)}$ ${\displaystyle \forall y(y\leq x)}$

Natural number type 2

The complete type of the number 2 over the empty set in the theory of natural numbers is the set of all formulas with at most one free variable that are true for. This amount includes formulas such as , , , and . This is an example of an isolated type because the formula implies all other formulas that apply to the number 2. ${\displaystyle x}$ ${\displaystyle x=2}$ ${\displaystyle x\neq 1+1+1}$ ${\displaystyle x\leq 1+1+1+1+1}$ ${\displaystyle \exists y(y<x)}$ ${\displaystyle x=1\lor 1=1}$ ${\displaystyle 1+1+1=1+1+1}$ ${\displaystyle x=1+1}$

Hyperreal numbers

The type is not realized within the real numbers according to the Archimedean axiom . An extension in which this type is realized are the hyper-real numbers . If this type is realized by, the type of infinitely small numbers is automatically realized by. ${\displaystyle \{x>1,x>1+1,x>1+1+1,\ldots \}}$ ${\displaystyle c}$ ${\displaystyle 1/c}$

Stone room

On the set of the complete types over can be a topology defined: ${\displaystyle S_{n}(A)}$ ${\displaystyle n}$ ${\displaystyle A}$

If we denote by the set of all complete types, the formula contained as an element, and stand and for a true or false statement, it shall ${\displaystyle [\varphi ]}$ ${\displaystyle n}$ ${\displaystyle \varphi }$ ${\displaystyle \top }$ ${\displaystyle \bot }$

1. ${\displaystyle S_{n}(A)=[\top ]}$, ${\displaystyle \emptyset =[\bot ]}$
2. ${\displaystyle [\varphi ]\cup [\psi ]=[\varphi \lor \psi ]}$
3. ${\displaystyle [\varphi ]\cap [\psi ]=[\varphi \land \psi ]}$
4. ${\displaystyle S_{n}(A)\setminus [\varphi ]=[\lnot \varphi ]}$

In particular, they form the basis of a topology. This provides the stone room. This is compact , Hausdorff-like and totally incoherent . Isolated types correspond to the isolated points . ${\displaystyle [\varphi ]}$

example

The complete theory of algebraically closed fields of the characteristic 0 has quantifier elimination , so that one can easily determine all 1-types (over the empty set):

• Types of algebraic numbers : These types are open points in Stone space. The isolating formula results from the minimal polynomial . Two algebraic numbers have the same type if and only if they are conjugated, i.e. if they have the same minimal polynomial.
• The type of the transcendent elements: This type is not open as a point in the Stone room. All transcendent elements have the same type, this means for every polynomial except the 0 polynomial that the element is not a zero of the polynomial.

Realizations of types in models

While isolated types have a realization in every model, it depends on the model for the other types whether they are realized or not. It is therefore obvious to examine models in which a particularly large number or a particularly few types are implemented.

A model that realizes all types over finite sets is called - saturated . More generally, the term can be defined for any infinite cardinal numbers : A model is called -saturated if all types are realized using sets with smaller cardinal numbers. A model is called saturated if it is -saturated. ${\displaystyle \omega }$ ${\displaystyle \kappa }$ ${\displaystyle \kappa }$ ${\displaystyle \kappa }$ ${\displaystyle {\mathcal {M}}}$ ${\displaystyle \mid {\mathcal {M}}\mid }$

Conversely, the Omitting Types Theorem (seldom also referred to as the type avoidance clause in German) states that there are models in which a given type has no implementation. The type is said to be omitted or avoided by the model: be a non-isolated type in a countable language. Then there is a countable model in which it is not realized. More generally one can also show that even a countable set of non-isolated types can be left out. ${\displaystyle p}$ ${\displaystyle p}$

literature

• Wilfrid Hodges : Model theory , Cambridge University Press, 1993, ISBN 0-521-30442-3 .

Web links

• Martin Ziegler: Script Model Theory 1 (PDF; 649 kB)