Definition:Type
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Contents
Definition
Let $\mathcal M$ be an $\mathcal L$-structure.
Let $A$ be a subset of the universe of $\mathcal M$.
Let $\mathcal L_A$ be the language consisting of $\mathcal L$ along with constant symbols for each element of $A$.
Viewing $\mathcal M$ as an $\mathcal L_A$-structure by interpreting each new constant as the element for which it is named, let $\operatorname{Th}_A \left({\mathcal M}\right)$ be the set of $\mathcal L_A$-sentences satisfied by $\mathcal M$.
An $n$-type over $A$ is a set $p$ of $\mathcal L_A$-formulas in $n$ free variables such that $p \cup \operatorname{Th}_A \left({\mathcal M}\right)$ is satisfiable by some $\mathcal L_A$-structure.
If you are familiar with this area of mathematics, you may be able to help improve $\mathsf{Pr} \infty \mathsf{fWiki}$ by determining the precise term which is to be used.
To discuss it in more detail, feel free to use the talk page.
When this has been done, {{Disambiguate}} should be removed from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Complete Type
We say that an $n$-type $p$ is complete (over $A$) if and only if:
- for every $\mathcal L_A$-formula $\phi$ in $n$ free variables, either $\phi \in p$ or $\phi \notin p$.
The set of complete $n$-types over $A$ is often denoted by $S_n^\mathcal M \left({A}\right)$.
Given an $n$-tuple $\bar b$ of elements from $\mathcal M$, the type of $\bar b$ over $A$ is the complete $n$-type consisting of those $\mathcal L_A$-formulas $\phi \left({x_1, \dotsc, x_n}\right)$ such that $\mathcal M \models \phi \left({\bar b}\right)$.
It is often denoted by $\operatorname{tp}^\mathcal M \left({\bar b / A}\right)$.
Realization
Given an $\mathcal L_A$-structure $\mathcal N$, a type $p$ is realized by an element $\bar b$ of $\mathcal N$ if and only if:
- $\forall \phi \in p: \mathcal N \models \phi \left({\bar b}\right)$.
Such an element $\bar b$ of $\mathcal N$ is a realization of $p$.
Omission
We say that $\mathcal N$ omits $p$ if $p$ is not realized in $\mathcal N$.
Then $p$ is an omission from $\mathcal N$.
Definition without respect to a structure
Let $T$ be an $\mathcal L$-theory.
An $n$-type of $T$ is a set $p$ of $\mathcal L_A$-formulas such that $p \cup T$ is satisfiable.
The set of complete $n$-types over $T$ is often denoted $S_n^T$ or $S_n \left({T}\right)$.
Note that this extends the definitions above, since, for example, $S_n^\mathcal M \left({A}\right) = S_n^{\operatorname{Th}_A \left({\mathcal M}\right)}$.
Note on comma-separated or juxtaposed parameters
Since it is often of interest to discuss types over sets such as $A \cup \left\{ {c}\right\}$ where $b$ is an additional parameter not in $A$, it is conventional to simplify notation by writing the parameter set as $A, c$ or just $A c$.
For example:
- $\operatorname{tp} \left({b / A \cup \cup \left\{ {c}\right\} }\right) = \operatorname{tp} \left({b / A, c}\right) = \operatorname{tp} \left({b / A c}\right)$
