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 unsatisfactorythe 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 rootsthe spectrum. The spectrum is an element s in the completion of the set of nmultisets 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 J_{n} of intervals such that the sum of the lengths åJ_{n} 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 J_{n}. 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.
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) Mspread on T consists of a sequence e_{1} ³ e_{2} ³ ¼ of real numbers decreasing to 0, called the regulator (of convergence) of the spread, and a function from T to subsets a_{t} of M so that
A Cauchy sequence c_{n} gives rise to a spread a on N by setting a_{n} = {c_{n},c_{n+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 notin our case, t is admissible if a_{t} 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 a_{t}.
If x is any element of M, then defining a_{t} = {x} for all nonzero t Î T, and e_{n} = 0, gives a uniform Cauchy spreada 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 a_{t} = {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 Mspread, as in the traditional intuitionistic view of the continuum R as a Qspread.
Let a and b be Mspreads on trees S and T, respectively. The distance between a and b is given by



We can define operations of addition and subtraction of Rspreads a and b by

By a closed interval we mean a set of the form [u,v] = {x Î R : u £ x £ v}. An Rspread 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.
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 J_{n} a sequence of nonempty intervals such that å J_{n} 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 Î ÈJ_{n}.
Proof. Let e £  I å J_{n} be a positive rational number. If we expand the J_{n} to open intervals J_{n}^{¢} = {x Î R : d(x,J_{n}) < e/2^{n+2}}, then  J_{n}^{¢} =  J_{n} +e/2^{n+1} is the sum of two convergent sequences, and e/2 £  I å J_{n}^{¢} , so the hypotheses are still met. Thus we may assume that the J_{n} are open.
Let T be the tree of finite sequences of the symbols L and R. For t Î T, define I_{t} inductively by I_{0} = I, and, if I_{t} = [a,b], then I_{tL} = [a,(a+b)/2] and I_{tR} = [(a+b)/2,b]. Define the regulator to be e_{i} = (1/2)^{i} I . Note that I_{t} = e_{ t }. Set


Suppose y Î J_{m}. As J_{m} is open, y±d Î J_{m} for some d > 0. So if  t ³ m, then d(y,a_{t}) ³ 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 : a_{t} 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 J_{n} is a singleton for each n. If J_{n} = {r_{n}} for some enumeration r_{n} 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,  J_{n} = e2^{n1} and we may assume that I has rational endpoints and pick e =  I . Then  I_{t} = e2^{ t} = 2 J_{ t } , so





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 r_{n} 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.
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 = {r_{1},¼,r_{n}} such that p(x) is approximately equal to p_{r}(x) = (xr_{1})¼(xr_{n}). The spectrum s defines a nonnegative function d(z,s) on the complex numbersthe limit of the distance functions d(z,r) = inf_{i} zr_{i} . 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 x_{0} = y and choose x_{1} so that
d(x_{1},x_{0}) < v and f(x_{1}) < (uv)/2.
For i > 0, inductively choose
x_{i+1} such that
d(x_{i+1},x_{i})
<(uv)/2^{i}
f(x_{i+1})
<(uv)/2^{i+1}
The x_{i} form a Cauchy sequence. Let x be its limit. Then x Î L because L is closed and f(x_{i}) < (uv)/2^{i+1}, so d(x,L) = 0. Moreover,

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

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 complexvalued 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 S^{c} denote the (metric) complement of S. We first show that
 (**) 
Choose q in (1/2,1) so that (q1/2)e < d/2 and choose q so that 0 < q < (q1/2). Consider the tree T of all finite sequences from {1,2,3,4}. To each node t we inductively associate a square S_{t} of width e_{t} = q^{ t }e. The root node is the empty sequence 0, and we set S_{0} = S. Having constructed S_{t}, cover S_{t} with four squares S_{t1}, S_{t2}, S_{t3}, S_{t4} of width qe_{t}, each with a corner in common with S_{t}. Here is the picture.
Next we show that if f(x) £ d/2, then for each n there exists t at level n such that d(x,S_{t}^{c}) > qe_{t}. 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,S_{t}^{c}) > qe_{t}, then d(x,S_{ti}^{c}) > qe_{ti} for some i = 1,2,3,4.
The condition that means, intuitively, that S_{t} contains a point of f in its interior is
 (*) 
There exists x such that f(x) < d/2, so d(x,S^{c}) ³ 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

If a_{t} is nonempty, then a_{t} = S_{t}. Moreover, f(x) is arbitrarily small for some point x Î S_{t}. Now

Conversely, if f(y) < u, then we need to find t at level n so that d(S_{t},y) < u and a_{t} is nonempty. Because f(y) < u, there exists x with d(x,y) < u and f(x) < qq^{n}e. As f(x) £ d/2, there exists t at level n so that d(x,S_{t}^{c}) > qq^{n}e, so d(x,S_{t}^{c}) > f(x). That's the condition for a_{t} to be nonempty, and d(S_{t},y) < u because x Î S_{t} 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 R^{2}. The proof goes through, mutatis mutandis, for R^{n} as well.
The Baire category theorem [1, Page 93] says that if M is a complete metric space, and U_{n} is a sequence of dense open sets, then the intersection Ç_{n = 1}^{¥}U_{n} 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 U_{n} by U_{n}ÇB.
If S is a subset of M, and r > 0, we let

Theorem 4 If M is a nonempty complete metric space, and U_{n} is a sequence of dense open sets, then there exists an Mspread a such that a_{t} is well contained in U_{ t } for every t.
Proof. The tree T consists of finite sequences of pairs (c_{1},r_{1}),¼,(c_{m},r_{m}) such that
Set a_{0} = M and a_{t} = B_{rm}(c_{m}) where t = ((c_{1},r_{1}),¼,(c_{m},r_{m})). We must show that if 0 < r £ 1/m and B_{r}(c) is well contained in U_{m}, then there exists c^{¢} and 0 < r^{¢} £ 1/(m+1) so that d(c,c^{¢})+r^{¢} < r and B_{r¢}(c^{¢}) is well contained in U_{m+1}. Let c^{¢} Î U_{m+1} be within r/2 of c and choose d > 0 so that B_{d}(c^{¢}) is well contained in B_{r}(c). Let r^{¢} = min(r/2,d).
Because a_{t} is well contained in U_{ t } for every t, any infinite path in a gives a point in the intersection of all the U_{n}.