Definable real number

The description may be expressed as a construction or as a formula of a formal language.

For example, the positive square root of 2,

, can be defined as the unique positive solution to the equation

Different choices of a formal language or its interpretation give rise to different notions of definability.

Because formal languages can have only countably many formulas, every notion of definable numbers has at most countably many definable real numbers.

using a compass and straightedge, beginning with a fixed line segment of length 1.

The positive square root of 2 is constructible.

is called a real algebraic number if there is a polynomial

There are numbers such as the cube root of 2 which are algebraic but not constructible.

This nonconstructive proof that not all real numbers are algebraic was first published by Georg Cantor in his 1874 paper "On a Property of the Collection of All Real Algebraic Numbers".

, produces a decimal expansion for the number accurate to

This notion was introduced by Alan Turing in 1936.

Specific examples of noncomputable real numbers include the limits of Specker sequences, and algorithmically random real numbers such as Chaitin's Ω numbers.

The language of arithmetic has symbols for 0, 1, the successor operation, addition, and multiplication, intended to be interpreted in the usual way over the natural numbers.

Because no variables of this language range over the real numbers, a different sort of definability is needed to refer to real numbers.

is definable in the language of arithmetic (or arithmetical) if its Dedekind cut can be defined as a predicate in that language; that is, if there is a first-order formula

The second-order language of arithmetic is the same as the first-order language, except that variables and quantifiers are allowed to range over sets of naturals.

A real that is second-order definable in the language of arithmetic is called analytical.

For example, the limit of a Specker sequence is an arithmetical number that is not computable.

The definitions of arithmetical and analytical reals can be stratified into the arithmetical hierarchy and analytical hierarchy.

In general, a real is computable if and only if its Dedekind cut is at level

of the arithmetical hierarchy, one of the lowest levels.

Similarly, the reals with arithmetical Dedekind cuts form the lowest level of the analytical hierarchy.

is first-order definable in the language of set theory, without parameters, if there is a formula

in the language of set theory, with one free variable, such that

[2] This notion cannot be expressed as a formula in the language of set theory.

Thus the real numbers definable in the language of set theory include all familiar real numbers such as 0, 1,

Assuming that they form a set in the model, the real numbers definable in the language of set theory over a particular model of ZFC form a field.

This argument becomes more problematic if it is applied to class models of ZFC, such as the von Neumann universe.

[3][4] Similarly, the question of whether the von Neumann universe contains real numbers that it cannot define cannot be expressed as a sentence in the language of ZFC.