Editing Constructive analysis (section)

==Principles==
For practical mathematics, the [[axiom of dependent choice]] is adopted in various schools.

[[Markov's principle#In constructive analysis|Markov's principle]] is adopted in the Russian school of recursive mathematics. This principle strengthens the impact of proven negation of strict equality. A so-called analytical form of it grants <math>\neg(x\le 0)\to x>0</math> or <math>\neg(x\cong 0)\to x\# 0</math>. Weaker forms may be formulated.

The [[L. E. J. Brouwer|Brouwerian]] school reasons in terms of [[Spread (intuitionism)|spreads]] and adopts the classically valid [[bar induction]].

=== Anti-classical schools ===
Through the optional adoption of further consistent axioms, the negation of decidability may be provable. For example, equality-to-zero is rejected to be decidable when adopting Brouwerian continuity principles or [[Church's thesis (constructive mathematics)|Church's thesis]] in recursive mathematics.<ref>{{Cite arXiv|eprint=1804.05495|title=Constructive Reverse Mathematics
|class=math.LO|last1=Diener|first1=Hannes|year=2020}}</ref> The weak continuity principle as well as <math>{\mathrm{CT}_0}</math> even refute <math>x\ge 0 \or 0\ge x</math>. The existence of a [[Specker sequence]] is proven from <math>{\mathrm{CT}_0}</math>. Such phenomena also occur in [[Effective topos#Realizability topoi|realizability topoi]]. Notably, there are two anti-classical schools as incompatible with one-another. This article discusses principles compatible with the classical theory and choice is made explicit.