Editing Definable real number (section)

== Definability in models of ZFC ==
A real number <math>a</math> is '''first-order definable in the language of set theory, without parameters''', if there is a formula <math>\varphi</math> in the language of [[set theory]], with one [[free variable]], such that <math>a</math> is the unique real number such that <math>\varphi(a)</math> holds.{{r|kunen}}  This notion cannot be expressed as a formula in the language of set theory.

All analytical numbers, and in particular all computable numbers, are definable in the language of set theory. Thus the real numbers definable in the language of set theory include all familiar real numbers such as [[Zero|0]], [[One|1]], <math>\pi</math>, <math>e</math>, et cetera, along with all algebraic numbers. Assuming that they form a set in the model, the real numbers definable in the language of set theory over a particular model of [[Zermelo–Fraenkel set theory|ZFC]] form a field. 
 
Each set [[Model theory|model]] <math>M</math> of ZFC set theory that contains uncountably many real numbers must contain real numbers that are not definable within <math>M</math> (without parameters). This follows from the fact that there are only countably many formulas, and so only countably many elements of <math>M</math> can be definable over <math>M</math>.  Thus, if <math>M</math> has uncountably many real numbers, one can prove from "outside" <math>M</math> that not every real number of <math>M</math> is definable over <math>M</math>.  
 
This argument becomes more problematic if it is applied to [[class (set theory)|class]] models of ZFC, such as the [[von Neumann universe]]. The assertion "the real number <math>x</math> is definable over the ''class'' model <math>N</math>" cannot be expressed as a formula of ZFC.{{r|hlr|tsirelson}} 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. Moreover, there are countable models of ZFC in which all real numbers, all sets of real numbers, functions on the reals, etc. are definable.{{r|hlr|tsirelson}}