Editing Constructive analysis (section)

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