Editing Constructive analysis (section)

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