Editing Constructive analysis (section)

==Formalization==
===Rational sequences===
A common approach is to identify the real numbers with non-volatile sequences in <math>{\mathbb Q}^{\mathbb N}</math>. The constant sequences correspond to rational numbers. Algebraic operations such as addition and multiplication can be defined component-wise, together with a systematic reindexing for speedup. The definition in terms of sequences furthermore enables the definition of a strict order "<math>></math>" fulfilling the desired axioms. Other relations discussed above may then be defined in terms of it. In particular, any number <math>x</math> apart from <math>0</math>, i.e. <math>x\# 0</math>, eventually has an index beyond which all its elements are invertible.<ref>Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editors), ''Handbook of Constructive Mathematics''; Studies in Logic and the Foundations of Mathematics; (2023) pp. 201-207</ref>
Various implications between the relations, as well as between sequences with various properties, may then be proven.

====Moduli====
As the [[Maximum and minimum|maximum]] on a finite set of rationals is decidable, an absolute value map on the reals may be defined and [[Cauchy sequence|Cauchy convergence]] and limits of sequences of reals can be defined as usual.

A [[modulus of convergence]] is often employed in the constructive study of Cauchy sequences of reals, meaning the association of any <math>\varepsilon > 0</math> to an appropriate index (beyond which the sequences are closer than <math>\varepsilon</math>) is required in the form of an explicit, strictly increasing function <math>\varepsilon\mapsto N(\varepsilon)</math>. Such a modulus may be considered for a sequence of reals, but it may also be considered for all the reals themselves, in which case one is really dealing with a sequence of pairs.

====Bounds and suprema====
Given such a model then enables the definition of more set theoretic notions. For any subset of reals, one may speak of an [[Upper and lower bounds|upper bound]] <math>b</math>, negatively characterized using <math>x\le b</math>. One may speak of least upper bounds with respect to "<math>\le</math>". A [[supremum]] is an upper bound given through a sequence of reals, positively characterized using "<math><</math>". If a subset with an upper bound is well-behaved with respect to "<math><</math>" (discussed below), it has a supremum.

====Bishop's formalization====
[[Errett Bishop|One formalization]] of constructive analysis, modeling the order properties described above, proves theorems for sequences of rationals <math>x</math> fulfilling the ''regularity'' condition <math>|x_n-x_m|\le \tfrac{1}{n}+\tfrac{1}{m}</math>. An alternative is using the tighter <math>2^{-n}</math> instead of <math>\tfrac{1}{n}</math>, and in the latter case non-zero indices ought to be used. No two of the rational entries in a regular sequence are more than <math>\tfrac{3}{2}</math> apart and so one may compute natural numbers exceeding any real. For the regular sequences, one defines the logically positive loose positivity property as <math>x > 0 \,:=\, \exists n. x_n > \tfrac{1}{n}</math>, where the relation on the right hand side is in terms of rational numbers. Formally, a positive real in this language is a regular sequence together with a natural witnessing positivity. Further, <math>x\cong y \,:=\, \forall n. |x_n-y_n| \le \tfrac{2}{n}</math>, which is logically equivalent to the negation <math>\neg\exists n. |x_n-y_n| > \tfrac{2}{n}</math>. This is provably transitive and in turn an [[equivalence relation]]. Via this predicate, the regular sequences in the band <math>|x_n| \le \tfrac{2}{n}</math> are deemed equivalent to the zero sequence. Such definitions are of course compatible with classical investigations and variations thereof were well studied also before. One has <math>y > x</math> as <math>(y - x) > 0</math>. Also, <math>x \ge 0</math> may be defined from a numerical non-negativity property, as <math>x_n \geq -\tfrac{1}{n}</math> for all <math>n</math>, but then shown to be equivalent of the logical negation of the former.<ref>Errett Bishop, ''Foundations of Constructive Analysis'', July 1967</ref><ref>{{cite journal|author=Stolzenberg, Gabriel|title=Review: Errett Bishop, ''Foundations of Constructive Analysis''|journal=[[Bull. Amer. Math. Soc.]]|year=1970|volume=76|issue=2|pages=301–323|url=http://projecteuclid.org/euclid.bams/1183531480|doi=10.1090/s0002-9904-1970-12455-7|doi-access=free}}</ref>

====Variations====
The above definition of <math>x\cong y</math> uses a common bound <math>\tfrac{2}{n}</math>. Other formalizations directly take as definition that for any fixed bound <math>\tfrac{2}{N}</math>, the numbers <math>x</math> and <math>y</math> must eventually be forever at least as close.
Exponentially falling bounds <math>2^{-n}</math> are also used, also say in a real number condition <math>\forall n. |x_n-x_{n+1}|<2^{-n}</math>, and likewise for the equality of two such reals. And also the sequences of rationals may be required to carry a modulus of convergence. Positivity properties may defined as being eventually forever apart by some rational.

[[axiom of non-choice|Function choice]] in <math>{\mathbb N}^{\mathbb N}</math> or stronger principles aid such frameworks.

====Coding====
It is worth noting that sequences in <math>{\mathbb Q}^{\mathbb N}</math> can be coded rather compactly, as they each may be mapped to a unique subclass of <math>{\mathbb N}</math>. A sequence rationals <math>i\mapsto \tfrac{n_i}{d_i}(-1)^{s_i}</math> may be encoded as set of quadruples <math>\langle i, n_i, d_i, s_i\rangle\in{\mathbb N}^4</math>. In turn, this can be encoded as unique naturals <math>2^i \cdot 3^{n_i}\cdot 5^{d_i}\cdot 7^{s_i}</math> using the [[fundamental theorem of arithmetic]]. There are more economic [[pairing function]]s as well, or extension encoding tags or metadata. For an example using this encoding, the sequence <math>i\mapsto {\textstyle\sum}_{k=0}^i\tfrac{1}{k}</math>, or <math>1,2,\tfrac{5}{2},\tfrac{8}{3},\dots</math>, may be used to compute [[Euler's number]] and with the above coding it maps to the subclass <math>\{ 15, 90, 24300, 6561000,\dots\}</math> of <math>{\mathbb N}</math>. While this example, an explicit sequence of sums, is a [[total recursive function]] to begin with, the encoding also means these objects are in scope of the quantifiers in second-order arithmetic.

===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>

===Category and type theory===
All these considerations may also be undertaken in a topos or appropriate dependent type theory.