---
tag: 9V71Q3SD1G
kind: concept
name: Type
msc: [03C07, 03C50]
sources:
  - url: https://en.wikipedia.org/wiki/Type_(model_theory)
same_as:
  wikidata: Q834884
  wikipedia: Type (model theory)
---

## Summary

In model theory, a type is a set of formulas in some free variables that is consistent with a theory.
It describes the possible behaviour of a tuple of elements.
A complete type gives a full first-order description of a tuple: every formula or its negation belongs to it.
A type is realized in a model when some tuple of the model satisfies all its formulas, and omitted otherwise.
Types are the basic tool for comparing models, and counting them leads to [[saturated models|RMTZ5J64FX]], categoricity and stability.

## Explanations

### L1 human

A type is a list of properties that an element could have, written in the language of the theory.
For example, take the ordered field of real numbers and the list "$x > 1$, $x > 2$, $x > 3$, and so on".
It is a type, because every finite part of it is satisfied by some real number.
No real number satisfies the whole list, so $\R$ omits this type.
In a nonstandard model of the reals the type is realized by an infinitely large element.
So types record which kinds of elements a model has and which it is missing.