Editing Constructive analysis (section)

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