For a simple example, consider the intermediate value theorem. In classical analysis, IVT says that, given any continuous functionf from a closed interval to the real lineR, if f is negative while f is positive, then there exists a real numberc in the interval such that f is exactly zero. In constructive analysis, this does not hold, because the constructive interpretation of existential quantification requires one to be able to construct the real number c. 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 numbern, there exists a real number cn in the interval such that the absolute value of f 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 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 and any natural number m, there exists a real number y in the interval such that |y - x| < 1/m and |f| > 0. In this case, the desired number c can be constructed. This is a complicated condition, but there are several other conditions which imply it and which are commonly met; for example, every analytic function is locally non-zero < 0 and f. 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 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.
Another difference between classical and constructive analysis is that constructive analysis does not accept the least upper bound principle, that any subset of the real lineR has a least upper bound, 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. 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 several commonly studied sets, including all intervals and compact sets. Closely related to this, in constructive mathematics, fewer characterisations of compact spaces are constructively valid—or from another point of view, there are several different concepts which are classically equivalent but not constructively equivalent. Indeed, if the interval 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 sequencen.
The diagonal construction in Cantors theorem is intuitionistically valid. Indeed, the constructive component of the diagonal argument already appeared in Cantor's work. According to Kanamori, a historical misrepresentation has been perpetuated that associates diagonalization with non-constructivity. As a result, the real numbers are uncountable in any constructive system. In some models, is subcountable. A variant found in constructive analysis textbooks may go as follows: "Let be a sequence of real numbers. Let x0 and y0 be real numbers, x0 < y0. Then there exists a real number x with x0 ≤ x ≤ y0 and x ≠ an . . . The proof is essentially Cantor's 'diagonal' proof." Sequences of reals appear commonly in analysis. Constructive analysist that reject not just the law of excluded middle but also the limited principle of omniscience and even Markov's principle may make use of the axiom of dependent choice for sequences of reals.
