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). However, most real numbers are not definable: the set of all definable numbers is countably infinite (because the set of all logical formulas is) while the set of real numbers is uncountably infinite (see Cantor's diagonal argument). As a result, most real numbers have no description (in the same sense that most real numbers are not rational).

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.