Type (model theory)

In model theory and related areas of mathematics, a type is an object that describes how a (real or possible) element or finite collection of elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x1, x2,..., xn that are true of a set of n-tuples of an L-structure

M

{\displaystyle {\mathcal {M}}}

. Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure

M

{\displaystyle {\mathcal {M}}}

. The question of which types represent actual (tuples of) elements of

M

{\displaystyle {\mathcal {M}}}

leads to the ideas of saturated models and omitting types.

Definitions

Consider a structure

M

{\displaystyle {\mathcal {M}}}

for a language L. Let M be the universe of the structure. For every A ⊆ M, let L(A) be the language obtained from L by adding a constant ca for every a ∈ A. In other words,

L

(

A

)

=

L

∪

{

c

a

:

a

∈

A

}

.

{\displaystyle L(A)=L\cup \{c_{a}:a\in A\}.}

A 1-type (of

M

{\displaystyle {\mathcal {M}}}

) over A is a set p(x) of formulas in L(A) with at most one free variable x, such that for every finite subset p0(x) ⊆ p(x) there is some b ∈ M, depending on p0(x), with

M

⊨

p

0

(

b

)

{\displaystyle {\mathcal {M}}\models p_{0}(b)}

. In other words,

M

⊨

∃

x

(

⋀

p

0

(

x

)

)

{\displaystyle {\mathcal {M}}\models \exists x\left(\bigwedge p_{0}(x)\right)}

More generally, an n-type (of

M

{\displaystyle {\mathcal {M}}}

) over A is defined to be a set p(x1,...,xn) = p(x) of formulas in L(A), each having its free variables occurring only among the given n free variables x1,...,xn, such that for every finite subset p0(x) ⊆ p(x) there are some elements b1,...,bn ∈ M with

M

⊨

p

0

(

b

1

,

…

,

b

n

)

{\displaystyle {\mathcal {M}}\models p_{0}(b_{1},\ldots ,b_{n})}

.

A complete type of

M

{\displaystyle {\mathcal {M}}}

over A is one that is maximal with respect to inclusion. Equivalently, for every

ϕ

(

x

)

∈

L

(

A

,

x

)

{\displaystyle \phi ({\boldsymbol {x}})\in L(A,{\boldsymbol {x}})}

either

ϕ

(

x

)

∈

p

(

x

)

{\displaystyle \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})}

or

¬

ϕ

(

x

)

∈

p

(

x

)

{\displaystyle \lnot \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})}

.