Definable real 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) which contains a single free variable x and such that one can prove that a is the unique real number which makes the statement φ(a) true. The formula φ(x) is not restricted to first-order statements.

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 be a definable number.

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