Let
be a first order language. Let be an
-structure. Denote
by and
by , and suppose
is a formula from
, and
is some sequence from .
Then we write
to denote
. We say that
is -definable. More generally if is some set and
, and there is some from so that is -definable then we say that is -definable.
In particular we say that a set is -definable or zero definable iff it is the solution set of some formula without parameters.
Let be a function, then we say is -definable iff the graph of (i.e.
) is a -definable set.
If is -definable then any automorphism of that fixes pointwise, fixes setwise.
A set or function is definable iff it is -definable for some parameters .
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 theory it is not actually very important what language one is using, but merely what the definable sets are, or what the definability relation is.
In proof theory, given a theory in the language
, for a function
to be definable in the theory , we have two conditions:
(i) There is a formula in the language
s.t. is definable over the model , as in the above definition; i.e., its graph is definable in the language
over the model , by some formula
.
(ii) The theory proves that is indeed a function, that is
.
For example: the graph of exponentiation function is definable by the language of the theory (a subsystem of PA, with induction axiom restricted to bounded formulas only), however the function itself is not definable in this theory.
|