Editing Constructive analysis (section)

==Introduction==
The name of the subject contrasts with ''classical analysis'', which in this context means analysis done according to the more common principles of classical mathematics. However, there are various schools of thought and many different formalizations of constructive analysis.<ref>Troelstra, A. S., van Dalen D., ''Constructivism in mathematics: an introduction 1''; Studies in Logic and the Foundations of Mathematics; Springer, 1988;</ref> Whether classical or constructive in some fashion, any such framework of analysis axiomatizes the [[real number line]] by some means, a collection extending the [[rationals]] and with an [[apartness relation]] definable from an asymmetric order structure. Center stage takes a positivity predicate, here denoted <math>x > 0</math>, which governs an equality-to-zero <math>x\cong 0</math>. The members of the collection are generally just called the ''real numbers''. While this term is thus overloaded in the subject, all the frameworks share a broad common core of results that are also theorems of classical analysis.

Constructive frameworks for its formulation are extensions of [[Heyting arithmetic]] by types including <math>{\mathbb N}^{\mathbb N}</math>, constructive [[second-order arithmetic]], or strong enough [[topos theory|topos]]-, [[dependent type theory|type]]- or [[constructive set theory#Analysis|constructive set theories]] such as <math>{\mathsf{CZF}}</math>, a constructive counter-part of <math>{\mathsf{ZF}}</math>. Of course, a [[Tarski's axiomatization of the reals|direct axiomatization]] may be studied as well.