definable type

Let M be a first order structureMathworldPlanetmath. Let A and B be sets of parameters from M. Let p be a completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath n-type over B. Then we say that p is an A-definable type iff for every formulaMathworldPlanetmathPlanetmath ψ(x¯,y¯) with ln(x¯)=n, there is some formula dψ(y¯,z¯) and some parameters a¯ from A so that for any b¯ from B we have ψ(x¯,b¯)p iff Mdψ(b¯,a¯).

Note that if p is a type over the model M then this condition is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to showing that {b¯M:ψ(x¯,b¯)M} is an A-definable set.

For p a type over B, we say p is definable if it is B-definable.

If p is definable, we call dψ the defining formula for ψ, and the function ψdψ a defining scheme for p.

Title definable type
Canonical name DefinableType
Date of creation 2013-03-22 13:29:26
Last modified on 2013-03-22 13:29:26
Owner Timmy (1414)
Last modified by Timmy (1414)
Numerical id 4
Author Timmy (1414)
Entry type Definition
Classification msc 03C07
Classification msc 03C45
Related topic Type2
Defines definable type
Defines defining scheme