Editing Constructive analysis (section)

===Set theory===
====Cauchy reals====
In some frameworks of analysis, the name ''real numbers'' is given to such well-behaved sequences or rationals, and relations such as <math>x\cong y</math> are called the ''equality or real numbers''. Note, however, that there are properties which can distinguish between two <math>\cong</math>-related reals.

In contrast, in a set theory that models the naturals <math>{\mathbb N}</math> and validates the existence of even classically uncountable function spaces (and certainly [[Constructive set theory#Constructive Zermelo–Fraenkel|say <math>{\mathsf{CZF}}</math>]] or even <math>{\mathsf{ZFC}}</math>) the numbers equivalent with respect to "<math>\cong</math>" in <math>{\mathbb Q}^{\mathbb N}</math> may be collected into a set and then this is called the ''[[Construction of the real numbers#Construction from Cauchy sequences|Cauchy real number]]''. In that language, regular rational sequences are degraded to a mere representative of a Cauchy real. Equality of those reals is then given by the equality of sets, which is governed by the set theoretical [[axiom of extensionality]]. An upshot is that the set theory will prove properties for the reals, i.e. for this class of sets, expressed using the logical equality. Constructive reals in the presence of appropriate choice axioms will be Cauchy-complete but not automatically order-complete.<ref>Robert S. Lubarsky, [https://arxiv.org/pdf/1510.00639.pdf ''On the Cauchy Completeness of the Constructive Cauchy Reals''], July 2015</ref>

====Dedekind reals====
In this context it may also be possible to model a theory or real numbers in terms of [[Construction of the real numbers#Construction by Dedekind cuts|Dedekind cuts]] of <math>{\mathbb Q}</math>. At least when assuming <math>{\mathrm{PEM}}</math> or dependent choice, these structures are isomorphic.

====Interval arithmetic====
Another approach is to define a real number as a certain subset of <math>{\mathbb Q}\times{\mathbb Q}</math>, holding pairs representing inhabited, pairwise intersecting intervals.

====Uncountability====
Recall that the preorder on [[cardinal number|cardinals]] "<math>\le</math>" in set theory is the primary notion defined as [[injective function|injection]] existence. As a result, the constructive theory of cardinal order can diverge substantially from the classical one. Here, sets like <math>{\mathbb Q}^{\mathbb N}</math> or some models of the reals can be taken to be [[Subcountability|subcountable]].

That said, [[Cantor's diagonal argument#In the absence of excluded middle|Cantors diagonal construction]] proving uncountability of powersets like <math>{\mathcal P}{\mathbb N}</math> and plain function spaces like <math>{\mathbb Q}^{\mathbb N}</math> is [[Intuitionistic logic|intuitionistically]] valid. Assuming <math>{\mathrm {PEM}}</math> or alternatively the [[countable choice]] axiom, models of <math>{\mathbb R}</math> are always uncountable also over a constructive framework.<ref>Bauer, A., Hanson, J. A. "The countable reals", 2022</ref> One variant of the diagonal construction relevant for the present context may be formulated as follows, proven using countable choice and for reals as sequences of rationals:<ref>See, e.g., Theorem 1 in Bishop, 1967, p. 25</ref>
:For any two pair of reals <math>a < b</math> and any sequence of reals <math>x_n</math>, there exists a real <math>z</math> with <math> a < z < b </math> and <math> \forall (n \in {\mathbb N}). x_n\, \#\, z</math>.
Formulations of the reals aided by explicit moduli permit separate treatments.

According to [[Akihiro Kanamori|Kanamori]], "a historical misrepresentation has been perpetuated that associates diagonalization with non-constructivity" and a constructive component of the [[Diagonal argument (proof technique)|diagonal argument]] already appeared in Cantor's work.<ref>[[Akihiro Kanamori]], "The Mathematical Development of Set Theory from Cantor to Cohen", ''[[Bulletin of Symbolic Logic]]'' / Volume 2 / Issue 01 / March 1996, pp 1-71</ref>