Let L be a first order language. Let M be an http://planetmath.org/node/3384L-structureMathworldPlanetmath. Let BM, and let aMn. Then we define the type of a over B to be the set of L-formulasMathworldPlanetmath ϕ(x,b¯) with parameters b¯ from B so that Mϕ(a,b¯). A collectionMathworldPlanetmath of L-formulas is a completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath n-type over B iff it is of the above form for some B,M and aMn.

We call any consistent collection of formulas p in n variables with parameters from B a partial n-type over B. (See criterion for consistency of sets of formulas.)

Note that a complete n-type p over B is consistent so is in particular a partial type over B. Also p is maximal in the sense that for every formula ψ(x,b¯) over B we have either ψ(x,b¯)p or ¬ψ(x,b¯)p. In fact, for every collection of formulas p in n variables the following are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath:

  • p is the type of some sequence of n elements a over B in some model NM

  • p is a maximal consistent set of formulas.

For nω we define Sn(B) to be the set of complete n-types over B.

Some authors define a collection of formulas p to be a n-type iff p is a partial n-type. Others define p to be a type iff p is a complete n-type.

A type (resp. partial type/complete type) is any n-type (resp. partial type/complete type) for some nω.

Title type
Canonical name Type
Date of creation 2013-03-22 13:22:45
Last modified on 2013-03-22 13:22:45
Owner ratboy (4018)
Last modified by ratboy (4018)
Numerical id 6
Author ratboy (4018)
Entry type Definition
Classification msc 03C07
Related topic Formula
Related topic DefinableType
Related topic TermsAndFormulas
Defines type
Defines complete type
Defines partial type