definability

Definability is a notion used in logic and mathematics to describe when an object, relation, or subset can be uniquely specified by a formula in a formal language inside a given structure. In model theory, a subset S of M^n is definable (over M) if there exists a first-order formula φ(x1, ..., xn) with possibly parameters from M such that S = {a ∈ M^n : M ⊨ φ(a)}. If no parameters are allowed, the subset is called parameter-free definable.

Examples help illustrate the idea. In the real field (R, +, ·, <), the singleton {0} is definable by x = 0, and the set of nonnegative numbers is definable by ∃y (x = y^2). A elements is definable over a subset A ⊆ M if there is a formula φ(x) with parameters from A such that M ⊨ φ(a) and for any b ≠ a, M ⊨ ¬φ(b). The definable closure of A in M consists of all elements of M that are definable over A.

Beyond model theory, definability appears in set theory. An ordinal-definable (OD) set is one that is definable in the language of set theory using ordinals as parameters. The class of such sets plays a role in the study of the constructible universe, where elements are built in stages by definability from earlier stages.

Definability is not a computability notion. A set can be definable by a formula yet be noncomputable, and conversely. It is also sensitive to the chosen language and structure, so definability is relative to the formal framework under consideration.