Editing Constructive analysis

{{Short description|Mathematical analysis}}
In [[mathematics]], '''constructive analysis''' is [[mathematical analysis]] done according to some principles of [[constructive mathematics]].

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

==Logical preliminaries==
The base logic of constructive analysis is [[intuitionistic logic]], which means that the [[principle of excluded middle]] <math>{\mathrm {PEM}}</math> is not automatically assumed for every [[proposition]]. If a proposition <math>\neg\neg\exists x.\theta(x)</math> is provable, this exactly means that the non-existence claim <math>\neg\exists x.\theta(x)</math> being provable would be absurd, and so the latter cannot also be provable in a consistent theory. The double-negated existence claim is a logically negative statement and implied by, but generally not equivalent to the existence claim itself. Much of the intricacies of constructive analysis can be framed in terms of the weakness of propositions of the logically negative form <math>\neg\neg\phi</math>, which is generally weaker than <math>\phi</math>. In turn, also an implication <math>\big(\exists x.\theta(x)\big)\to \neg\forall x.\neg\theta(x)</math> can generally be not reversed.

While a constructive theory proves fewer theorems than its classical counter-part in its classical presentation, it may exhibit attractive meta-logical properties. For example, if a theory <math>{\mathsf {T}}</math> exhibits the [[disjunction property]], then if it proves a disjunction <math>{\mathsf {T}}\vdash \phi\lor \psi</math> then also <math>{\mathsf {T}}\vdash \phi</math> or <math>{\mathsf {T}}\vdash \psi</math>. Already in classical arithmetic, this is violated for the most basic propositions about sequences of numbers - as demonstrated next.

===Undecidable predicates===
A common strategy of formalization of real numbers is in terms of sequences or rationals, <math>{\mathbb Q}^{\mathbb N}</math> and so we draw motivation and examples in terms of those. So to define terms, consider a [[decidable problem|decidable]] predicate on the naturals, which in the constructive vernacular means <math>\forall n. \big( Q(n)\lor\neg Q(n) \big)</math> is provable, and let <math>\chi_Q\colon{\mathbb N}\to\{0, 1\}</math> be the characteristic function defined to equal <math>0</math> exactly where <math>Q</math> is true. 
The associated sequence <math>q_n\,:=\,{\textstyle\sum}_{k=0}^n \chi_Q(n) / 2^{k+1}</math> is monotone, with values non-strictly growing between the bounds <math>0</math> and <math>1</math>. 
Here, for the sake of demonstration, defining an extensional equality to the zero sequence <math>(q\cong_\mathrm{ext} 0)\,:=\,\forall n. q_n=0</math>, it follows that <math>q\cong_\mathrm{ext} 0 \leftrightarrow\forall n. Q(n)</math>. Note that the symbol "<math>0</math>" is used in several contexts here. For any theory capturing arithmetic, there are many yet undecided and even provenly independent such statements <math>\forall n. Q(n)</math>. Two <math>\Pi_1^0</math>-examples are the [[Goldbach conjecture]] and the [[Rosser's trick|Rosser sentence]] of a theory. 

Consider any theory <math>{\mathsf{T}}</math> with quantifiers ranging over [[primitive recursive]], rational-valued sequences. Already [[minimal logic]] proves the non-contradiction claim for any proposition, and that the negation of excluded middle for any given proposition would be absurd. This also means there is no consistent theory (even if anti-classical) rejecting the excluded middle disjunction for any given proposition. Indeed, it holds that
:<math>{\mathsf{T}}\,\,\,\vdash\,\,\,\forall(x\in{\mathbb Q}^{\mathbb N}).\,\neg\neg\big((x\cong_\mathrm{ext} 0)\lor\neg(x\cong_\mathrm{ext} 0)\big)</math>
This theorem is [[Intuitionistic logic#Non-interdefinability of operators|logically equivalent]] to the non-existence claim of a sequence for which the excluded middle disjunction about equality-to-zero would be disprovable. No sequence with that disjunction being rejected can be exhibited.
Assume the theories at hand are [[consistency|consistent]] and arithmetically sound. Now [[Gödel's theorems]] mean that there is an explicit sequence <math>g\in{\mathbb Q}^{\mathbb N}</math> such that, for any fixed precision, <math>{\mathsf{T}}</math> proves the zero-sequence to be a good approximation to <math>g</math>, but it can also meta-logically be established that <math>{\mathsf{T}}\,\nvdash\,(g\cong_\mathrm{ext} 0)</math> as well as <math>{\mathsf{T}}\,\nvdash\,\neg(g\cong_\mathrm{ext} 0)</math>.<ref>{{cite book |last1=Smith |first1=Peter |title=An introduction to Gödel's Theorems |date=2007 |url=http://www.godelbook.net/ |publisher=Cambridge University Press |location=Cambridge, U.K. |isbn=978-0-521-67453-9 |mr=2384958}}</ref> Here this proposition <math>g\cong_\mathrm{ext} 0</math> again amounts to the proposition of universally quantified form.
Trivially
:<math>{\mathsf{T}}+{\mathrm{PEM}}\,\,\,\vdash\,\,\,\forall(x\in{\mathbb Q}^{\mathbb N}).\,(x\cong_\mathrm{ext} 0)\lor\neg(x\cong_\mathrm{ext} 0)</math>
even if these disjunction claims here do not carry any information. In the absence of further axioms breaking the meta-logical properties, constructive entailment instead generally reflects provability. Taboo statements that ought not be decidable (if the aim is to respect the provability interpretation of constructive claims) can be designed for definitions of a custom equivalence "<math>\cong</math>" in formalizations below as well. For implications of disjunctions of yet not proven or disproven propositions, one speaks of [[Constructive proof#Brouwerian counterexamples|weak Brouwerian counterexamples]].

===Order vs. disjunctions===
The theory of the [[real closed field]] may be axiomatized such that all the non-logical axioms are in accordance with constructive principles. This concerns a [[commutative ring]] with postulates for a positivity predicate <math>x>0</math>, with a positive unit and non-positive zero, i.e., <math>1>0</math> and <math>\neg(0>0)</math>. In any such ring, one may define <math>y > x\,:=\,(y - x > 0)</math>, which constitutes a strict total order in its constructive formulation (also called linear order or, to be explicit about the context, a [[pseudo-order]]). As is usual, <math>x < 0</math> is defined as <math>0 > x</math>.

This [[first-order logic|first-order]] theory is relevant as the structures discussed below are model thereof.<ref>Erik Palmgren, ''An Intuitionistic Axiomatisation of Real Closed Fields'', Mathematical Logic Quarterly, Volume 48, Issue 2, Pages: 163-320, February 2002</ref> However, this section thus does not concern aspects akin to [[topology]] and relevant arithmetic substructures are not [[Definable set|definable]] therein.

As explained, various predicates will fail to be decidable in a constructive formulation, such as these formed from order-theoretical relations. This includes "<math>\cong</math>", which will be rendered equivalent to a negation. Crucial disjunctions are now discussed explicitly.

====Trichotomy====
In intuitonistic logic, the [[disjunctive syllogism]] in the form <math>(\phi\lor\psi)\to(\neg\phi\to\psi)</math> generally really only goes in the <math>\to</math>-direction. In a pseudo-order, one has
:<math>\neg(x>0 \lor 0>x) \to x\cong 0</math>
and indeed at most one of the three can hold at once. But the stronger, ''logically positive'' '''[[law of trichotomy]] disjunction does not hold in general''', i.e. it is not provable that for all reals,
:<math>(x>0 \lor 0>x) \lor x\cong 0</math>
See [[limited principle of omniscience|analytical <math>{\mathrm {LPO}}</math>]]. Other disjunctions are however implied based on other positivity results, e.g. <math>(x + y > 0) \to (x>0 \lor y>0)</math>. Likewise, the asymmetric order in the theory ought to fulfill the weak linearity property <math>(y > x) \to (y > t \lor t > x)</math> for all <math>t</math>, related to locatedness of the reals.

The theory shall validate further axioms concerning the relation between the positivity predicate <math>x > 0</math> and the algebraic operations including multiplicative inversion, as well as the [[intermediate value theorem]] for polynomials. 
In this theory, between any two separated numbers, other numbers exist.

====Apartness====
In the context of analysis, the auxiliary '''logically positive''' predicate
:<math>x\# y\,:=\,(x > y\lor y > x)</math>
may be independently defined and constitutes an ''[[apartness relation]]''. With it, the substitute of the principles above give tightness
:<math>\neg(x\# 0)\leftrightarrow(x\cong 0)</math>
Thus, apartness can also function as a definition of "<math>\cong</math>", rendering it a negation. All negations are stable in intuitionistic logic, and therefore
:<math>\neg\neg(x\cong y)\leftrightarrow(x\cong y)</math>
The elusive trichotomy disjunction itself then reads
:<math>(x\# 0) \lor \neg(x\# 0)</math>
Importantly, a '''proof of the disjunction <math>x\# y</math> carries positive information''', in both senses of the word. Via <math>(\phi\to\neg\psi)\leftrightarrow(\psi\to\neg\phi)</math> it also follows that <math>x\# 0\to\neg(x\cong 0)</math>. In words: A demonstration that a number is somehow apart from zero is also a demonstration that this number is non-zero. But constructively it does not follow that the doubly negative statement <math>\neg(x\cong 0)</math> would imply <math>x\# 0</math>. Consequently, many classically equivalent statements bifurcate into distinct statement. For example, for a fixed polynomial <math>p\in {\mathbb R}[x]</math> and fixed <math>k\in {\mathbb N}</math>, the statement that the <math>k</math>'th coefficient <math>a_k</math> of <math>p</math> is apart from zero is stronger than the mere statement that it is non-zero. A demonstration of former explicates how <math>a_k</math> and zero are related, with respect to the ordering predicate on the reals, while a demonstration of the latter shows how negation of such conditions would imply to a contradiction. In turn, there is then also a strong and a looser notion of, e.g., being a third-order polynomial.

So the excluded middle for <math>x\# 0</math> is apriori stronger than that for <math>x\cong 0</math>. However, see the discussion of possible further axiomatic principles regarding the strength of "<math>\cong</math>" below.

====Non-strict partial order====
Lastly, the relation <math>0\ge x</math> may be defined by or proven equivalent to the '''logically negative''' statement <math>\neg(x > 0)</math>, and then <math>x \le 0</math> is defined as <math>0 \ge x</math>. Decidability of positivity may thus be expressed as <math>x > 0\lor 0\ge x</math>, which as noted will not be provable in general. But neither will the totality disjunction <math>x\ge 0 \lor 0\ge x</math>, see also [[limited principle of omniscience|analytical <math>{\mathrm {LLPO}}</math>]].

By a valid [[De Morgan's laws#In intuitionistic logic|De Morgan's law]], the conjunction of such statements is also rendered a negation of apartness, and so
:<math>(x\ge y \land y\ge x)\leftrightarrow (x\cong y)</math>
The disjunction <math>x > y \lor x\cong y</math> implies <math>x\ge y</math>, but the other direction is also not provable in general. In a constructive real closed field, '''the relation "<math>\ge</math>" is a negation and is not equivalent to the disjunction in general'''.

====Variations====
Demanding good order properties as above but strong completeness properties at the same time implies <math>{\mathrm {PEM}}</math>. Notably, the [[Dedekind–MacNeille completion|MacNeille completion]] has better completeness properties as a collection, but a more intricate theory of its order-relation and, in turn, worse locatedness properties. While less commonly employed, also this construction simplifies to the classical real numbers when assuming <math>{\mathrm {PEM}}</math>.

===Invertibility===
In the commutative ring of real numbers, a provably non-invertible element equals zero. This and the most basic locality structure is abstracted in the theory of [[Heyting field|Heyting fields]].

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

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

==Theorems==
Many classical theorems can only be proven in a formulation that is [[logically equivalent]], over [[classical logic]]. Generally speaking, theorem formulation in constructive analysis mirrors the classical theory closest in [[separable space]]s. Some theorems can only be formulated in terms of [[approximation]]s.

===The intermediate value theorem===
For a simple example, consider the [[intermediate value theorem]] (IVT).
In classical analysis, IVT implies that, given any [[continuous function]] ''f'' from a [[closed interval]] [''a'',''b''] to the [[real line]] ''R'', if ''f''(''a'') is [[negative number|negative]] while ''f''(''b'') is [[positive number|positive]], then there exists a [[real number]] ''c'' in the interval such that ''f''(''c'') is exactly [[0 (number)|zero]].
In constructive analysis, this does not hold, because the constructive interpretation of [[existential quantification]] ("there exists") requires one to be able to ''construct'' the real number ''c'' (in the sense that it can be approximated to any desired precision by a [[rational number]]).
But if ''f'' hovers near zero during a stretch along its domain, then this cannot necessarily be done.

However, constructive analysis provides several alternative formulations of IVT, all of which are equivalent to the usual form in classical analysis, but not in constructive analysis.
For example, under the same conditions on ''f'' as in the classical theorem, given any [[natural number]] ''n'' (no matter how large), there exists (that is, we can construct) a real number ''c''<sub>''n''</sub> in the interval such that the [[absolute value]] of ''f''(''c''<sub>''n''</sub>) is less than 1/''n''.
That is, we can get as close to zero as we like, even if we can't construct a ''c'' that gives us ''exactly'' zero.

Alternatively, we can keep the same conclusion as in the classical IVT—a single ''c'' such that ''f''(''c'') is exactly zero—while strengthening the conditions on ''f''.
We require that ''f'' be ''locally non-zero'', meaning that given any point ''x'' in the interval [''a'',''b''] and any natural number ''m'', there exists (we can construct) a real number ''y'' in the interval such that |''y'' - ''x''| < 1/''m'' and |''f''(''y'')| > 0.
In this case, the desired number ''c'' can be constructed.
This is a complicated condition, but there are several other conditions that imply it and that are commonly met; for example, every [[analytic function]] is locally non-zero (assuming that it already satisfies ''f''(''a'') < 0 and ''f''(''b'') > 0).

For another way to view this example, notice that according to [[classical logic]], if the ''locally non-zero'' condition fails, then it must fail at some specific point ''x''; and then ''f''(''x'') will equal 0, so that IVT is valid automatically.
Thus in classical analysis, which uses classical logic, in order to prove the full IVT, it is sufficient to prove the constructive version. From this perspective, the full IVT fails in constructive analysis simply because constructive analysis does not accept classical logic. Conversely, one may argue that the true meaning of IVT, even in classical mathematics, is the constructive version involving the ''locally non-zero'' condition, with the full IVT following by "pure logic" afterwards.
Some logicians, while accepting that classical mathematics is correct, still believe that the constructive approach gives a better insight into the true meaning of theorems, in much this way.

===The least-upper-bound principle and compact sets===
Another difference between classical and constructive analysis is that constructive analysis does not prove the [[least-upper-bound principle]], i.e. that any [[subset]] of the real line '''R''' would have a [[least upper bound]] (or supremum), possibly infinite.
However, as with the intermediate value theorem, an alternative version survives; in constructive analysis, any ''located'' subset of the real line has a supremum.
(Here a subset ''S'' of '''R''' is ''located'' if, whenever ''x'' < ''y'' are real numbers, either there exists an element ''s'' of ''S'' such that ''x'' < ''s'', [[logical disjunction|or]] ''y'' is an [[upper bound]] of ''S''.)
Again, this is classically equivalent to the full least upper bound principle, since every set is located in classical mathematics.
And again, while the definition of located set is complicated, nevertheless it is satisfied by many commonly studied sets, including all [[Interval (mathematics)|intervals]] and all [[compact set]]s.

Closely related to this, in constructive mathematics, fewer characterisations of [[compact space]]s are constructively valid—or from another point of view, there are several different concepts that are classically equivalent but not constructively equivalent.
Indeed, if the interval [''a'',''b''] were [[sequentially compact]] in constructive analysis, then the classical IVT would follow from the first constructive version in the example; one could find ''c'' as a [[cluster point]] of the [[infinite sequence]] (''c''<sub>''n''</sub>)<sub>''n''∈'''N'''</sub>.

==See also==
{{Portal|Mathematics}}
* [[Computable analysis]]
* [[Constructive nonstandard analysis]]
* [[Heyting field]]
* [[Indecomposability (constructive mathematics)]]
* [[Pseudo-order]]

==References==
{{reflist}}

==Further reading==
*{{cite book |last=Bishop |first=Errett |author-link=Errett Bishop |date=1967 |title=Foundations of Constructive Analysis |publisher=Ishi Press International |isbn=4-87187-714-0 }}
*{{cite book |title=Real Analysis: A Constructive Approach |first=Mark |last=Bridger |publisher=Wiley |location=Hoboken |year=2007 |isbn=978-0-471-79230-7 }}

{{Non-classical logic}}

{{Authority control}}

{{DEFAULTSORT:Constructive Analysis}}
[[Category:Mathematical analysis|*]]
[[Category:Constructivism (mathematics)|*]]
[[Category:Intuitionism]]