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. 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. 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, constructive second-order arithmetic, or strong enough topos-, type- or constructive set theories. Of course, a 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 is not automatically assumed for every proposition can generally be not reversed.

exhibits the disjunction property. Already in classical arithmetic, this is violated for the most basic propositions about sequences of numbers - as demonstrated next.

Undecidable predicates

and so we draw motivation and examples in terms of those. So to define terms, consider a decidable-examples are the Goldbach conjecture and the Rosser sentence of a theory.

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

This theorem is 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 consistent and arithmetically sound. Now Gödel's theorems. again amounts to the proposition of universally quantified form. Trivially

" in formalizations below as well. For implications of disjunctions of yet not proven or disproven propositions, one speaks of 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, which constitutes a strict total order in its constructive formulation (also called linear order or, to be explicit about the context, a pseudo-order.

This first-order theory is relevant as the structures discussed below are model thereof. However, this section thus does not concern aspects akin to topology and relevant arithmetic substructures are not definable therein.

", which will be rendered equivalent to a negation. Crucial disjunctions are now discussed explicitly.

Trichotomy

In intuitionistic logic, the disjunctive syllogism-direction. In a pseudo-order, one has

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,

See {\mathrm {LPO}}, related to locatedness of the reals.

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

may be independently defined and constitutes an apartness relation. With it, the substitute of the principles above give tightness

", rendering it a negation. All negations are stable in intuitionistic logic, and therefore

The elusive trichotomy disjunction itself then reads

Importantly, a carries positive information 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.

" below.

Non-strict partial order

may be defined by or proven equivalent to the logically negative, see also {\mathrm {LLPO}}.

By a valid De Morgan's law, the conjunction of such statements is also rendered a negation of apartness, and so

, but the other direction is also not provable in general. In a constructive real closed field, " is a negation and is not equivalent to the disjunction in general.

Variations

. Notably, the MacNeille completion.

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

Formalization

Rational sequences

, eventually has an index beyond which all its elements are invertible. Various implications between the relations, as well as between sequences with various properties, may then be proven.

Moduli

As the maximum on a finite set of rationals is decidable, an absolute value map on the reals may be defined and Cauchy convergence and limits of sequences of reals can be defined as usual.

A modulus of convergence. 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 bound". A supremum" (discussed below), it has a supremum.

Bishop's formalization

One formalization fulfilling the regularity. This is provably transitive and in turn an equivalence relation, but then shown to be equivalent of the logical negation of the former.

Variations

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

Function choice or stronger principles aid such frameworks.

Coding

using the fundamental theorem of arithmetic. There are more economic pairing functions, may be used to compute Euler's number. 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 are called the equality or real numbers-related reals.

and validates the existence of even classically uncountable function spaces (and certainly {\mathsf{CZF}} may be collected into a set and then this is called the 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.

Dedekind reals

In this context it may also be possible to model a theory or real numbers in terms of Dedekind cuts or dependent choice, these structures are isomorphic.

Interval arithmetic

, holding pairs representing inhabited, pairwise intersecting intervals.

Uncountability

Recall that the preorder on cardinals" in set theory is the primary notion defined as injection or some models of the reals can be taken to be subcountable.

That said, Cantors diagonal construction is intuitionistically or alternatively the countable choice are always uncountable also over a constructive framework. 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:

1. .

Formulations of the reals aided by explicit moduli permit separate treatments.

According to Kanamori, "a historical misrepresentation has been perpetuated that associates diagonalization with non-constructivity" and a constructive component of the diagonal argument already appeared in Cantor's work.

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. Weaker forms may be formulated.

The Brouwerian school reasons in terms of 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 in recursive mathematics.. The existence of a Specker sequence. Such phenomena also occur in 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 spaces. Some theorems can only be formulated in terms of approximations.

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 while f(b) is positive, then there exists a real number c in the interval such that f(c) is exactly 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 cn in the interval such that the absolute value of f(cn) 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, 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 intervals and all 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 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 (cn)n∈N.

See also

• Computable analysis

• Constructive nonstandard analysis

• Heyting field

• Indecomposability (constructive mathematics)

• Pseudo-order

References

Further reading