Spreads and choice in constructive mathematics

Fred Richman
Florida Atlantic University
Boca Raton, FL 33431

21 June 2001


An approach to choice-free mathematics using spreads: If constructing a point satisfying property P requires choice, replace this problem by that of constructing a nonempty set of elements satisfying P. Then construct a spread, without choice, whose elements satisfy P. The theory is developed and several examples are given.

1  Constructing points without choice

There are many situations in (constructive) mathematics where you want to construct a point, say a real or complex number, with certain characteristics. The three problems I want to consider are

 For each of these problems, the traditional solutions appeal to countable choice, or rather to the stronger axiom of dependent choices. This appeal does not seem to be removable, although Ruitenburg [5] has proved the fundamental theorem of algebra, without using choice, when the coefficients are given by pairs of Cauchy real numbers (limits of sequences of rational numbers). In the absence of choice we must distinguish between Cauchy real numbers and the more general Dedekind real numbers. The former have not been shown to be Cauchy complete (without using choice), which makes them a little unsatisfactory---the reason we constructed the reals in the first place was because the rationals were not complete!

In [3] the problem posed by the fundamental theorem of algebra is solved by redefining what a solution is. Instead of trying to approximate a single root of the polynomial, we approximate the set of roots---the spectrum. The spectrum is an element s in the completion of the set of n-multisets of Gaussian numbers. We can measure the distance from any complex number to s although we may not be able to construct a complex number whose distance to s is 0 (an element of s). We will see how this may be interpreted in terms of spreads in Theorem 3. For now, we note that attention is shifted from constructing a point with a certain property to constructing a nonempty set of points with that property. We then redefine what we mean by a "nonempty set of points."

We will illustrate these ideas by solving Problem 1 in the chapter on integration in [1] without using choice. In this problem we are given a sequence Jn of intervals such that the sum of the lengths |Jn| converges to a number that is less than the length of another interval I, and are required to construct a point in I that is not in any Jn. Our solution will be to construct a spread, in the sense of [2], such that any infinite path in that spread defines a point of the desired kind. The bad news is that, without countable choice, we cannot prove the existence of such a path. Perhaps that's because we are thinking only of lawlike paths. Brouwer's choice sequences are one way to get around this problem. Constructing a suitable spread is essentially the same as showing that there is a choice sequence with the required property. Alternatively, a spread can be thought of as a nondeterministic algorithm for constructing the desired point.

2  Spreads

A tree is a partially ordered set T with a least element 0 such that for each t T the set {s T : s t} is a finite chain. Denote by | t| the level of t, the natural number describing how far t is from the root 0. The least element is supposed to be a convenience, but it might be more of a nuisance. We denote T\{0} by T+.

Let M be a metric space and T a tree. A (uniform Cauchy) M-spread on T consists of a sequence e1 e2 of real numbers decreasing to 0, called the regulator (of convergence) of the spread, and a function from T to subsets at of M so that

A Cauchy sequence cn gives rise to a spread a on N by setting an = {cn,cn+1,}.

These spreads differ in two respects from the spreads in Heyting [2, page 34]. The branching in the tree T is arbitrary, rather than being indexed by the natural numbers at each node, and we do not assume that each node is either admissible or not---in our case, t is admissible if at is nonempty. Troelstra and van Dalen [6, page 186] use essentially the same definition of a tree (spread law) as Heyting does, but Heyting includes in a spread a complementary law which assigns to each node a mathematical object, as we have done here with at.

If x is any element of M, then defining at = {x} for all nonzero t T, and en = 0, gives a uniform Cauchy spread---a constant spread which we will denote by x. More generally, if X is any nonempty subset of M, then we can form a (constant) spread a representing X by letting T+ = X×N+, with (x,m) < (y,n) if x = y and m < n, and at = {x} for t = (x,m). Thus the notion of a spread can be thought of as a generalization of the notion of a nonempty subset of M. In fact, it is not hard to see that it generalizes the notion of a nonempty subset of the completion of M. In particular, the completion of M itself can be considered to be an M-spread, as in the traditional intuitionistic view of the continuum R as a Q-spread.

Let a and b be M-spreads on trees S and T, respectively. The distance between a and b is given by

d(a,b) =

| s| ,| t| = n 
so d(a,b) r if, for each n and d > 0, there exist s S and t T with | s| = | t| = n and d(as,bt) r+d. The quantity d(a,b) need not be a (located) real number; it is a generalized real number in the sense of [4]. Similarly, the distance between a and a subset X of M is given by
d(a,X) =

| s| = n 
which is equal to the distance between a and the spread representing X. In particular, using either formula, the distance between a point x M and a is given by
d(a,x) =

| s| = n 
If d(a,x) is a real number for each x in M, then we say that a is located. Note that d(a,x) d(at,x)+e| t| .

We can define operations of addition and subtraction of R-spreads a and b by

atbt = {ab : a at and b bt}.
The result is a spread ab, taking the regulator to be the termwise sum of the regulators of a and b. Define a < b to mean that there exist n in N and d > 0 in R so that b-a d whenever a at and b bt and | t| = n. Define a b to mean that a < b+d for all d > 0.

By a closed interval we mean a set of the form [u,v] = {x R : u x v}. An R-spread a is contained in a closed interval [u,v], written a [u,v], if u a v. In general, we say that a is contained in a closed subset C of M if d(a,x) d(C,x) for each x M. The reader can check that these two definitions of ``contained in'' agree for C = [u,v]. A spread is bounded if it is contained in a bounded closed subset of M.

3  Problem 1

We illustrate these ideas on Problem 1 of the integration chapter of [1]. Let |I| denote the length of an interval I of real numbers.

Theorem 1 Let I be a closed interval and Jn a sequence of nonempty intervals such that | Jn| converges to a number that is less than | I| . Then there is a spread a contained in I such that d(y,a) > 0 for each y Jn.

Proof. Let e | I| -| Jn| be a positive rational number. If we expand the Jn to open intervals Jn = {x R : d(x,Jn) < e/2n+2}, then | Jn| = | Jn| +e/2n+1 is the sum of two convergent sequences, and e/2 | I| -| Jn| , so the hypotheses are still met. Thus we may assume that the Jn are open.

Let T be the tree of finite sequences of the symbols L and R. For t T, define It inductively by I0 = I, and, if It = [a,b], then ItL = [a,(a+b)/2] and ItR = [(a+b)/2,b]. Define the regulator to be ei = (1/2)i| I| . Note that |It| = e| t| . Set

at = {x It\ | t|

i = 1 
Ji :

n = 1 
| JnIt| < | It|}.
Note that n = 1| JnIt| converges because | JnIt| | Jn| , and that if at is nonempty, then at = It\i = 1| t| Ji. In particular, a0 = I0 = I is nonempty. As | It| = | ItL| +|ItR| and | JnIt| = | JnItL| +| JnItR| we have
| It| -

n = 1 
| JnIt| = | ItL| -

n = 1 
| JnItL|+| ItR| -

n = 1 
| JnItR|
from which it follows that if n| JnIt| < | It| , then either n| JnItL| < | ItL| or n| JnItR| < | ItR| . That is, if at is nonempty, then either atL or atR is nonempty.

Suppose y Jm. As Jm is open, yd Jm for some d > 0. So if | t| m, then d(y,at) d, whence d(y,a) d.

Notice that the tree T constructed in this proof is a complete binary tree, but the subtree of interest, {t T : at is nonempty}, the set of admissible nodes in the terminology of [2], is not detachable as required in both [2] and [6].

Gabriel Stolzenberg points out that Theorem 1 is interesting even when Jn is a singleton for each n. If Jn = {rn} for some enumeration rn of the rational numbers, then the theorem asserts the existence of an irrational number in I, or rather a spread representing a ``nonempty set'' of irrational numbers. In this case, | Jn| = e2-n-1 and we may assume that I has rational endpoints and pick e = | I| . Then | It| = e2-| t| = 2| J| t| | , so


i = 1 
| Ji| = e(1-2-n)/2 < e/2 =

i = 1 
| Ji|
whence i = n+1| Ji| = e2-n-1. To construct an infinite path in the spread a, and so construct an irrational number in I, proceed as follows. The nodes t such that
| t|

m = 1 
| JmIt| < |It| /2 = e2-| t| -1
form a detachable subset S of T because all the intervals have rational endpoints. If t S, then

n = 1 
| JnIt| < | It|/2+e2-| t| -1 = | It|
so at is nonempty. Moreover,
| It| - | t|

n = 1 
| JnIt| -| J| t| +1It| = |ItL| - | tL|

n = 1 
| JnItL| +| ItR| - | tR|

n = 1 
| JnItR|
and, because t S,
| It| /2 < | It| - | t|

n = 1 
| JnIt|
so 0 <| J_| t| | -| J_| t| +1| | I_t| /2-| J_| t| +1I_t|
<| I_tL| -_n=1^| tL| | J_nI_tL| +| I_tR| -_n=1^| tR| | J_n I_tR|

from which it follows that either tL or tR is in S. Thus we can construct an infinite path by staying in S and, for example, going left except when we have to go right.

The situation is a different if rn is an arbitrary sequence of real numbers rather than an enumeration of the rational numbers. Then we are dealing with Cantor's theorem that the real numbers are uncountable. In that case is not so clear how to construct an infinite path in a without appealing to choice.

4  The fundamental theorem of algebra

In [3] the spectrum of a nonconstant monic polynomial p(x) of degree n is defined to be the limit of the multisets of complex numbers r = {r1,,rn} such that p(x) is approximately equal to pr(x) = (x-r1)(x-rn). The spectrum s defines a nonnegative function d(z,s) on the complex numbers---the limit of the distance functions d(z,r) = infi| z-ri| . If p(x) factors completely, then s can be represented as a multiset of complex numbers (the roots of p); otherwise it is just an object that can be approximated by multisets of complex numbers.

We want to axiomatize (most of) the essential properties of the function d(z,s).

A locater is a function f : M[0,) such that

(Functions with an additional property were called locations in [3] and were identified with points in the completion of M.) If, in addition, f is bounded away from zero on the complement of some bounded subset of M, we say that f is bounded.

If L is a nonempty located subset of M, then d(x,L) is a locater. This, of course, is the prototype locater. The converse can be proved, if M is complete, using the axiom of dependent choices. If L, in addition, is bounded, then d(x,L) is bounded away from zero on the complement of the bounded subset {z M : d(z,L) < 1}.

Theorem 2 Let f be a locater on a complete metric space M. Given the axiom of dependent choices, the set L = f  -1(0) is a located subset of M such that f(y) = d(y,L) for all y M.

Proof. Let u be a positive real number. If there is x L such that d(x,y) < u, then f(y) f(x)+d(x,y) < u (without choice). We will show that, conversely, if f(y) < u, then there is x L such that d(x,y) < u. Hence L is located and d(y,L) = f(y).

Choose v so that f(y) < v < u. Let x0 = y and choose x1 so that d(x1,x0) < v and f(x1) < (u-v)/2. For i > 0, inductively choose xi+1 such that d(xi+1,xi) <(u-v)/2i
f(xi+1) <(u-v)/2i+1

The xi form a Cauchy sequence. Let x be its limit. Then x L because L is closed and f(xi) < (u-v)/2i+1, so d(x,L) = 0. Moreover,

d(y,x) = d(x0,x)

i = 0 
d(xi+1,xi) < v+(u-v) = u.

It's not hard to see that d(z,s) is a bounded locater because s is a limit of the bounded located sets r. Similarly if a is a bounded located spread, then d(z,a) is a bounded locater because

d(z,a) =

| s| = n 
d(as,z) =

| s| = n 
and d(| s| = nas,z) is a locater. We need to check that d(y,a) d(x,a)+d(x,y), but that inequality is preserved by suprema. We must also verify that if d(y,a) < u, then there exists x with d(x,y) < u and d(x,a) arbitrarily small. If d(y,a) < u, then d(| s| = nas,y) < u for all n, so there exists x such that d(x,y) < u and d(x,|s| = nas) is arbitrarily small, hence d(x,a) is arbitrarily small.

To see that d(z,a) is a bounded locater, choose a bounded closed set B containing a. Then d(z,a) d(z,B) for every complex number z, so the function d(z,a) is bounded away from zero on the complement of the bounded set {z : d(z,B) < 1}.

Theorem 3 Let f be a bounded locater on the complex numbers. Then there is a bounded located complex-valued spread a so that the d(a,z) = f(z) for all z.

Proof. Let S be a square of width e so that f(y) d > 0 outside S. Let Sc denote the (metric) complement of S. We first show that

if f(x) d/2, then d(x,Sc) d/2.
Indeed, if y Sc, then d f(y) f(x)+d(x,y), so d(x,y) d/2.

Choose q in (1/2,1) so that (q-1/2)e < d/2 and choose q so that 0 < q < (q-1/2). Consider the tree T of all finite sequences from {1,2,3,4}. To each node t we inductively associate a square St of width et = q| t| e. The root node is the empty sequence 0, and we set S0 = S. Having constructed St, cover St with four squares St1, St2, St3, St4 of width qet, each with a corner in common with St. Here is the picture.

Picture Omitted

The width of the two central strips where the Sti overlap is 2(q-1/2)et.

Next we show that if f(x) d/2, then for each n there exists t at level n such that d(x,Stc) > qet. This is true for n = 0 by (**) and the choice of q and q. The general statement follows by induction upon observing that if d(x,Stc) > qet, then d(x,Stic) > qeti for some i = 1,2,3,4.

The condition that means, intuitively, that St contains a point of f in its interior is

f(x) < d(x,Stc) for some point x St.
If f(x) < u < d(x,Stc), then there exists y such that f(y) is arbitrarily small and d(x,y) < u, so d(y,Stc) d(x,Stc)-u > f(y). Thus if (*) holds for t, then it holds with f(x) arbitrarily small.

There exists x such that f(x) < d/2, so d(x,Sc) d/2 > f(x). Hence Condition (*) holds for t = 0. Moreover, if it holds for t, then it holds for one of t1, t2, t3, t4. Our spread is defined by setting

at = {y St : (*) holds for t},
that is, at = St if (*) holds for t, and at is empty otherwise (not to say that either the condition holds or it doesn't). The regulator of the spread is en = qne.

If at is nonempty, then at = St. Moreover, f(x) is arbitrarily small for some point x St. Now

f(y) f(x)+d(x,y) f(x)+d(St,y)+2q| t|e,
so f(y) d(St,y)+2q| t| e for all t such that at is nonempty, whence f(y) d(a,y).

Conversely, if f(y) < u, then we need to find t at level n so that d(St,y) < u and at is nonempty. Because f(y) < u, there exists x with d(x,y) < u and f(x) < qqne. As f(x) d/2, there exists t at level n so that d(x,Stc) > qqne, so d(x,Stc) > f(x). That's the condition for at to be nonempty, and d(St,y) < u because x St and d(x,y) < u.

If s is the spectrum of a polynomial p, then we can let f(z) = d(z,s) in this theorem. Then a and s are equivalent insofar as they represent objects that can be described by how they are located with respect to the complex numbers. In the presence of choice, a and s can be thought of as equal sets: {z : d(z,a) = 0} and {z : d(z,s) = 0}. The spectrum s has more structure because, in the presence of choice, it is a multiset not just a set. The multiplicities get lost when we pass to a because a is constructed from the function d(z,s) alone.

Nothing about the structure of the complex numbers is used in Theorem 3 other than the metric space structure of R2. The proof goes through, mutatis mutandis, for Rn as well.

5  The Baire category theorem

The Baire category theorem [1, Page 93] says that if M is a complete metric space, and Un is a sequence of dense open sets, then the intersection n = 1Un is dense. It suffices to show that the intersection is nonempty because we can get the stronger theorem by replacing M by the closure of an open ball B in M, and Un by UnB.

If S is a subset of M, and r > 0, we let

Br(S) = {x M : d(x,S) < r}.
We are not assuming that S is located: To say d(x,S) < r is equivalent to saying that there exists s S such that d(x,s) < r. We say that S is well contained in S if Br(S) S for some r > 0. This extends the usage in [1, Page 130] to arbitrary sets S.

Theorem 4 If M is a nonempty complete metric space, and Un is a sequence of dense open sets, then there exists an M-spread a such that at is well contained in U| t| for every t.

Proof. The tree T consists of finite sequences of pairs (c1,r1),,(cm,rm) such that

Set a0 = M and at = Brm(cm) where t = ((c1,r1),,(cm,rm)). We must show that if 0 < r 1/m and Br(c) is well contained in Um, then there exists c and 0 < r 1/(m+1) so that d(c,c)+r < r and Br(c) is well contained in Um+1. Let c Um+1 be within r/2 of c and choose d > 0 so that Bd(c) is well contained in Br(c). Let r = min(r/2,d).

Because at is well contained in U| t| for every t, any infinite path in a gives a point in the intersection of all the Un.


BISHOP, ERRETT AND DOUGLAS BRIDGES, Constructive analysis, Springer-Verlag 1980.

HEYTING, AREND, Intuitionism, an introduction, North-Holland 1956

RICHMAN, FRED, The fundamental theorem of algebra: a constructive development without choice, Pacific J. Math. 196 (2000), 213-230.

_________, Generalized real numbers in constructive mathematics, Indagationes Mathematicae, 9 (1998), 595-606.

RUITENBURG, WIM B. G., Constructing roots of polynomials over the complex numbers. Computational aspects of Lie group representations and related topics (Amsterdam, 1990), 107-128, CWI Tract, 84, Math. Centrum, Centrum Wisk. Inform., Amsterdam, 1991.

TROELSTRA, ANNE S., AND DIRK VAN DALEN, Constructivism in mathematics: an introduction, North-Holland, 1988.

File translated from TEX by TTH, version 2.27.
On 22 Jun 2001, 10:28.