definable (original) (raw)

0.1 Definable sets and functions

0.1.1 Definability In Model Theory

Let ℒ be a first order language. Let M be an ℒ-structure. Denote x1,…,xn by x→ and y1,…,ym by y→, and suppose ϕ⁢(x→,y→) is a formula from ℒ, and b1,…,bm is some sequence from M.

Then we write ϕ⁢(Mn,b→) to denote {a→∈Mn:M⊧ϕ⁢(a→,b→)}. We say that ϕ⁢(Mn,b→) is b→-definable. More generally if S is some set and B⊆M, 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 automorphism 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 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.

0.1.2 Definability of functions in Proof Theory

In proof theory, given a theory T in the language ℒ, for a function f:M→M 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 T⊢∀x→∃!y.ϕ(x→,y).

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