# definable type

Let $M$ be a first order structure^{}.
Let $A$ and $B$ be sets of parameters from $M$.
Let $p$ be a complete^{} $n$-type over $B$.
Then we say that $p$ is an $A$-definable type iff
for every formula^{} $\psi (\overline{x},\overline{y})$ with ln$(\overline{x})=n$,
there is some formula $d\psi (\overline{y},\overline{z})$ and some parameters $\overline{a}$ from $A$ so that
for any $\overline{b}$ from $B$ we have $\psi (\overline{x},\overline{b})\in p$ iff $M\vDash d\psi (\overline{b},\overline{a})$.

Note that if $p$ is a type over the model $M$ then this condition is equivalent^{} to showing that $\{\overline{b}\in M:\psi (\overline{x},\overline{b})\in 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\psi $ the defining formula for $\psi $, and the function $\psi \mapsto d\psi $ 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 |