Free Choice Sequences

There are many constructivists of a variety of flavors, all of whom agree on using intuitionistic logic. The chief place at which they differ is what to use for the real numbers. The standard ways of defining the real numbers are not constructively precise, and so there are many ways of making them more precise.

Brouwer's version, which Heyting outlines, is by far the most radical, and leads to the greatest departures from ordinary mathematics. For the most part the other constructivist versions of the real numbers are parts of his general idea.

Brouwer's real numbers actually allow counterexamples to the law of the excluded middle. Most constructivists, along with everyone else, balk at that and make use of systems in which, even though the law of the excluded middle is not a logical principle, it is still not subject to outright counterexamples.

Classically, one can introduce the real numbers in two fundamentally different ways: "constructing" them, pretty much always out of sets of rational numbers or introducing them "axiomatically," almost always as the smallest real closed field containing the rational numbers.

Constructivists can only make use of the first alternative. There are two general types of constructions that yield the real numbers classically: Dedekind cuts and Cauchy sequences.

Dedekind cuts: the square root of two is introduced in terms of the set of all rational numbers with square less than or equal to two.

Cauchy sequences: A Cauchy sequence is a convergent sequence of rational numbers, that is a sequence of rational numbers %$q_{0},q_{1},\dots$% such that for every (small) rational number %$\epsilon$% there is an %$N$% such that %$|q_{l}-q_{m}|<\epsilon$% for all %$l,m>N$%. The square root of two, for example, is %$1,1.4,1.41,1.414,\dots$%. More than one Cauchy sequence represents each real number, and so one must define what it is for two Cauchy sequences to be equal as real numbers.

Dedekind cuts are useless for the constructivist: Consider the number which is 0 if the sequence 0123456789 occurs in the decimal expansion of %$\pi$% and 1 otherwise. Where is it in the Dedekind cut for %$\frac{1}{2}$%? Constructively, we lose the possibility of putting every rational number either into or out of a cut.

Thus, except as a kind of pathology, the Dedekind cut real numbers are not constructively useful.

There are many variants of Cauchy sequences one might use for the real numbers, and each constructist school has a favorite. Bishop, for example, only considers Cauchy sequences such that

1. There is a procedure for producing the %$n$%th member of the sequence.
2. There is a procedure for, given %$\epsilon%$ producing %$N$%.
3. There is a constructive proof that the procedure given in the previous step works.

Brouwer's real numbers are very different:
A real number is just a set of constraints on what the freely thinking creative subject may choose for the %$n$%th term of the sequence given the preceding terms. Such a sequence, to be a real number, must provably converge. It may therefore be the case that some sequence neither is nor is not a real number, so far as we can tell.

The following is a perfectly good Brouwerian real number: At stage %$n+1$% choose any rational number that differs from the one chosen at stage %$n$% by less than %$\frac{1}{2^n}$%. This "real number" is, in a sense Brouwer carefully analyzes, all the real numbers. It is this single "number" that Brouwer thinks of as "the real numbers."

-- ProfessorShaughanLavine - 04 Feb 2005