0.1 Definable sets and functions

0.1.1 Definability In Model Theory

Let be a first order language. Let M be an -structureMathworldPlanetmath. Denote x1,,xn by x and y1,,ym by y, and suppose ϕ(x,y) is a formulaMathworldPlanetmath from , and b1,,bm is some sequencePlanetmathPlanetmath from M.

Then we write ϕ(Mn,b) to denote {aMn:Mϕ(a,b)}. We say that ϕ(Mn,b) is b-definable. More generally if S is some set and BM, and there is some b from B so that S is b-definable then we say that S is B-definable.

In particular we say that a set S is -definable or zero definable iff it is the solution set of some formula without parameters.

Let f be a function, then we say f is B-definable iff the graph of f (i.e. {(x,y):f(x)=y}) is a B-definable set.

If S is B-definable then any automorphismPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of M that fixes B pointwise, fixes S setwise.

A set or function is definable iff it is B-definable for some parameters B.

Some authors use the term definable to mean what we have called -definable here. If this is the convention of a paper, then the term parameter definable will refer to sets that are definable over some parameters.

Sometimes in model theoryMathworldPlanetmath it is not actually very important what languagePlanetmathPlanetmath one is using, but merely what the definable sets are, or what the definability relationMathworldPlanetmathPlanetmathPlanetmath is.

0.1.2 Definability of functions in Proof Theory

In proof theory, given a theory T in the language , for a function f:MM to be definable in the theory T, we have two conditions:

(i) There is a formula in the language s.t. f is definable over the model M, as in the above definition; i.e., its graph is definable in the language over the model M, by some formula ϕ(x,y).

(ii) The theory T proves that f is indeed a function, that is Tx!y.ϕ(x,y).

For example: the graph of exponentiationMathworldPlanetmathPlanetmath function xy=z is definable by the language of the theory IΔ0 (a subsystem of PA, with induction axiomMathworldPlanetmath restricted to bounded formulas only), however the function itself is not definable in this theory.

Title definable
Canonical name Definable
Date of creation 2013-03-22 13:26:52
Last modified on 2013-03-22 13:26:52
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 17
Author CWoo (3771)
Entry type Definition
Classification msc 03C07
Classification msc 03F03
Defines definable set
Defines definable function
Defines definable relation