Definable number

A definable number is a real number which can be unambigously defined by some mathematical statement. Formally, one calls a real number a 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 unambigously described. In particular, it contains all mathematical constants. 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 Cantors Diagonal argument).

The field of definable numbers is not complete?; there exist convergent sequences of definable numbers whose limit is not definable. 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.

---

/Talk