Definable number

A definable number is a real number which can be unambiguously defined by some mathematical statement. Formally, a real number a is called definable if there is some logical formula φ(x) in set theory which contains a single free variable x and such that one can prove from the Zermelo-Fraenkel-Choice set theory axioms that a is the unique real number which makes the statement φ(a) true.

The definable numbers form a field containing all numbers that have ever been or can be unambiguously described. In particular, it contains all mathematical constants and all algebraic numbers (and therefore all rational numbers). There are however many real numbers which are not definable: the set of all definable numbers is countable (because the set of all logical formulas is) while the set of real numbers is not (see Cantor's diagonal argument).

The field of definable numbers is not complete; there exist convergent sequences of definable numbers whose limit is not definable (since every real number is the limit of a sequence of rational numbers). However, if the sequence itself is definable in the sense that we can specify a single formula for all its terms, then its limit will necessarily be a definable number. In fact, all theorems of calculus remain true if the field of real numbers is replaced by the field of definable numbers, sequences are replaced by definable sequences, sets are replaced by definable sets and functions by definable functions.

While every computable number is definable, the converse is not true: Chaitin's constant is definable (otherwise we couldn't talk about it) but not computable.

One may also talk about definable complex numbers: complex numbers which are uniquely defined by a logical formula. A complex number is definable if and only if both its real part and its imaginary part are definable. The definable complex numbers also form a field.