Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems

Thierry Coquand

Chalmers University,

Sweden

Email: coquand@cs.chalmers.se

Bas Spitters

Radboud University Nijmegen,

the Netherlands

Email: spitters@cs.ru.nl

August 30, 2006

. This is an expanded version of our paper [CS05a]. For the convenience of the reader we have included more details and added a few clarifications. There are no new results. We are grateful to Bob Lubarsky and Fred Richman for suggesting improvements in the presentation.

. This author was supported by the Netherlands Organization for Scientific Research (NWO).

Abstract. We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.

Keywords: Formal topology, constructive mathematics, Riesz space, f-algebra, axiom of choice

A.M.S. subject classification: 03F60 Constructive and recursive analysis, 46S30 Constructive functional analysis, 06D22 Frames, locales

1.Introduction

This paper illustrates the relevance of locale theory for constructive mathematics. We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges [BB85]. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.

The article is organized as follows. After dealing with some preliminaries we prove a pointfree Stone-Yosida representation theorem for Riesz spaces. In the next section this is used to obtain a representation theorem for f-algebras, which in turn is used to prove the Gelfand representation theorem. Next we discuss the similarity between Bishop's notion of compactness, i.e. complete and totally bounded, and compact overt spaces in formal topology. Finally we show that the axiom of dependent choice is needed to construct points in the formal spectrum.

We would like to stress that the present theory needs few foundational commitments, we work within Bishop-style mathematics. Moreover, the mathematics is predicative, even finitary, and we will not use the axiom of choice, even countable choice, unless explicitly stated.

2.Riesz spaces

We present a Stone-Yosida representation theorem for Riesz spaces. This theorem states that a Riesz space with a strong unit may be represented as a Riesz space of functions. In fact, one can even start with an l-group, or lattice ordered group, with a strong unit and construct a Riesz space from this, see [Coq05](sec. 3).

2.1.General definitions

Definition 1. A Riesz space R is a Q vector space with a compatible binary sup operation that is, such that a + (bc) = (a + b)∨(a + c) and, moreover, λa⩾0 and - a⩽0, whenever a in R, λ in Q, a⩾0 and λ⩾0. One can prove that A Riesz space (or vector lattice) is a partially ordered linear space which is a distributive lattice.

As usual we define a + a∨0, a - ≔( - a)∨0, |a|≔a + + a - and ab≔ - ( - a∨ - b). One can prove that a Riesz space is a lattice and that the lattice operations are compatible with the vector space operations, see [Bir67][LZ71][Bou64].

Definition 2. A strong unit 1 in an ordered vector space R is a positive

. We follow the standard terminology using ‘positive' to mean non-negative.

1 element such that for all aR there exists a natural number n such that an⋅1.

We will now consider a Riesz space R with a strong unit. When q is a rational number, we will often write aq to mean aq⋅1.

Definition 3. A representation of R is a linear map σ:RR such that σ(1) = 1 and σ(ab) = σ(a)∨σ(b).

Such a representation automatically preserves all the Riesz space structure.

Example 4. If X is a compact space, then C(X), its space of continuous functions, is a Riesz space where the supremum is taken pointwise. Each point of x defines a representation σx(f)≔f(x).

In Example 19 we show that a complete commutative algebra of Hermitian operators on a Hilbert space is a Riesz space.

2.2.Spectrum

Given a Riesz space R, we will define a lattice that may be used to define the spectrum of R as a formal space, the points of which are then precisely the representations of R.

Let P denote the set of positive elements of a Riesz space R. For a,b in P we define ab to mean that there exists n such that an b. We write ab for ab and ab. The following proposition is proved in [Coq05] and involves only elementary considerations on Riesz spaces.

Proposition 5. We write L(R) for the quotient of P by ≈. Then L(R) is a distributive lattice. In fact, if we define D:RL(R) by D(a)≔[a + ], then L(R) is the free lattice generated by {D(a) | aR} subject to the following relations:

  1. D(a) = 0, if a≤0;
  2. D(1) = 1;
  3. D(a)∧D( - a) = 0;
  4. D(a + b)⩽D(a)∨D(b);
  5. D(ab) = D(a)∨D(b).

We have D(a)⩽D(b) if and only if a + b + and D(a) = 0 if and only if a⩽0.

For a in R and rational numbers p,q, we write a∈(p,q)≔(a - p)∧(q - a). Notice that this is an element of R by our convention that (a - q) means (a - q⋅1).

Lemma 6. a∈(p,q)≼a∈(p,s)∨a∈(t,q), whenever t,s are rational numbers such that t<s. Since our Riesz space has a strong unit, for each a, there exists p and q such that p<q and a∈(p,q) = 1. Moreover, if I0,…,In are open intervals covering (p,q), then veeaIi≈1.

Proof. We may assume that p<t<s<q.

a∈(p,s)∨a∈(t,q) = ((a - p)∧(s - a))∨((a - t)∧(q - a))
= ((a - p)∨(a - t)) ∧ ((a - t)∨(s - a))∧
((a - p)∨(q - a))∧((q - a)∨(s - a))
= (a - p) ∧((a - t)∨(s - a))∧
((a - p)∨(q - a))∧(q - a)
((a - p)∨(q - a))∧((a - t)∨(s - a)).

We claim that (( a - t )∨( s - a ))⩾

t - s
2
. To show this we write m
t + s
2
. Then

( a - s ) ∨ ( t - a ) = ( a - m + ( m - s )) ∨ ( t - m - ( a - m )) =
t - s
2
+ (( a - m ) ∨ - ( a - m ))⩾
t - s
2
.

The proof is finished by the observation that bc whenever for some ε, ε⋅1∧bc.

Lemma 7. If D(b1)∨…∨D(bn) = 1, then there exists r>0 such that D(b1 - r)∨…∨D(bn - r) = 1.

Proof. Since

1
N
b
+
1
∨…∨ b
+
m
we see that

1
2N
(b
+
1
∨…∨b
+
m
) -
1
2N
= (b
+
1
-
1
2N
)∨…∨(b
+
m
-
1
2N
)
(b1 -
1
2N
) + ∨…∨(bm -
1
2N
) + .

The previous lemma is used to prove the following result, which can be found as Theorem 1.11 in [Coq05]. We will not need this, but only state it as a motivation.

Theorem 8. Define Σ, the spectrum of R, to be the locale generated by the elements D(a) and the relations in Proposition 5 together with the relation D(a) = veer>0D(a - r). Then Σ is a compact completely regular locale.

Compact completely regular locales are the pointfree analogues of compact Hausdorff spaces. Moreover, the points of Σ can be identified with representations of R. In fact, if a representation σ is given, then σ∈D(a) if and only if σ(a)>0.

2.3.Normable elements

Dedekind cuts may be used to define real numbers, but it should be noted that constructively one needs to require that such cuts (L,U) are located, i.e. either pL or qU, whenever p<q. Upper cuts in the rational numbers may be conveniently used to deal with certain objects that classically would also be real numbers, we call them upper real numbers, see [Ric98][Vic03]. In general, such a cut does not have a greatest lower bound in R. If it does the upper real number is called located or simply a real number. Define the upper real U(a)≔{qQ|∃q'<q. aq'⋅1} for each element of the Riesz space. If it is located a is said to be normable and the greatest lower bound is denoted by sup a. Then we have sup a<q if and only if qU(a).

Proposition 9. If all elements of R are normable, then the predicate Pos(a)≔sup a>0 has the following properties:

  1. If Pos(a) and D(a)⩽D(b), then Pos(b);
  2. If Pos(ab), then Pos(a) or Pos(b);
  3. If r is a strictly positive rational number, then Pos(a) or D(a - r) = 0.

We note that Pos(a) if and only if Pos(a + ).

In fact, in localic terms this shows that Σ is open, or overt, see [Joh84], but we will not need this. In formal topology one would say that the formal space has a positivity predicate.

We remark that the standard terminologies from the two different fields seem to conflict. Clearly, it is not the case that Pos(a) as soon as a is positive, i.e. a⩾0. In particular, 0 is positive, but Pos(0) does not hold.

In order to prove Proposition 9 we first need three lemmas.

Lemma 10. sup (ab) = sup a∨sup b.

Proof.

Suppose that abq'<q, then a,bq', so both sup aq' and sup bq'. Thus q'⩾sup a∨sup b.
If q'⩾a,b, then q'⩾ab and hence sup ab⩽sup a∨sup b.

Lemma 11. Let r be a rational number. If sup b<r and r<sup(bc), then r<sup c.

Proof. If sup b<r, then br'<r, for some rational number r'. So, using Lemma 10

r<sup (bc) = sup b∨sup cr'∨sup c.

Consequently, r<sup c.

Lemma 12. If 0<sup (b1b2), then sup b1>0 or sup b2>0.

Proof. Suppose that 0<r<sup( b1b2). Either sup b1<r or sup b1>0. In latter case we are done. In the former case sup b2>r by Lemma 11.

Proof. [of Proposition 9]

Property 1 is clear.

Property 2 is Lemma 12.

Finally, to prove property 3 we decide whether sup a>0 or sup a<r. In the former case Pos(a). In the latter case D(a - r) = 0.

Corollary 13. If D(a1)∨…∨D(an) = 1, we can find i1<…<ik such that D(ai1)∨…∨D(aik) = 1 and Pos(ai1),…,Pos(aik).

Proof. By Lemma 7 there exists r>0 such that D(a1 - r)∨…∨D(an - r) = 1. By Proposition 9 for all i, D(ai - r) = 0 or Pos(ai). From this the result follows.

Lemma 14. Let I: = (p,q), J≔(r,s). Define I + J≔(p + r,q + s) and IJ≔(pr,qs). If |a + b - c|⩽ε and Pos(aIbJcK), then the distance between I + J and K is bounded by ε. If |ab - c|⩽ε and Pos(aIbJcK), then the distance between IJ and K is bounded by ε.

Finally, if |a - b|⩽ε and Pos(aIbJ), then the distance between I and J is bounded by ε.

Proof. We only prove the last fact. If the distance between I and J is bigger than ε, than r - q>ε or p - s>ε. Consequently, D(q - ab - r) = 0 or D(a - ps - b) = 0. Both cases imply that D(aIbJ) = 0.

Definition 15. A Riesz space R is separable if there exists a sequence an such that for all a and ε>0, there exists n such that |a - an|⩽ε.

Theorem 16. [DC] Let R be a separable Riesz space all elements of which are normable. Assume that Pos(a), then there exists a representation σ such that σ(a)>0.

Proof. We write εn≔2 - n. Using dependent choice and Lemma 6 we define a sequence (qn) of rationals such that

Pos( a ∈(
sup a
2
, sup a )∧ a 0 ∈( q 0 - ε 0 , q 0 + ε 0 )∧…∧ a n ∈( q n - ε n , q n + ε n )).

If bR, we can find a sequence of elements ank such that for any ε>0 we have |b - ank|≤ε when k is large enough. Then qnk is a Cauchy sequence and we define σ(b)≔limkqnk. By Lemma 14 this definition does not depend on the choice of the sequence ank. The map σ is a representation such that σ(a)>0 and σ(an)∈(qn - εn,qn + εn) for all n.

A suggestive way to state that σ(a)>0 is to say that σ is a point in D(a).

Let Σ be the set of representations of R. We call Σ the spectrum of R. Each representation is a bounded linear functional. Each element a of R defines a pseudo norm ρa(φ)≔|φ(a)| on the space of bounded linear functionals. If R is separable and an is a dense sequence in {aR : |a|⩽1}, we can collect, like Bishop, all the pseudo-norms into one norm ρ(φ)≔∑n2 - n|φ(an)|.

We have the following Stone-Yosida representation theorem, see [Sto41][Yos42].

Theorem 17. [DC] Let R is a separable Riesz space all elements of which are normable. The spectrum Σ is a complete totally bounded metric space. For a in R, we define a^:Σ→R by a^(σ)≔σ(a) and ‖a ‖≔sup(|a|). Then supσ|a^(σ)| = ‖a‖. Finally, the set of functions a^ is dense in C(Σ).

Proof. We define Ua r s D(a∈(r,s)) as an element of the lattice L(R). Intuitively, such an element may be thought of as the set {σ : σ(a)∈(r,s)} = {σ : ρa(σ)<s - r}. Let ε>0. Using Lemma 6 one may find finitely many Ua r s such that s - r<ε, the supremum of which equals 1 in the lattice L(R). By Corollary 13 one can assume all these elements to be positive. Each of them contains a point by Theorem 16. The collection of these points forms an ε-net. Consequently, Σ is totally bounded.

It is straightforward to show that Σ is also complete as a uniform space.

For each σ∈Σ we have |σ(a)|⩽‖a‖. To see this suppose that σ(a)>‖a‖. Then there exists ε>0 such that σ(a) - a⩾ε1, however σ(σ(a) - a) = 0. If r< ‖a‖, then by Theorem 16, there exists σ such that r<|σ(a)|.

Finally, the density follows from Proposition 3.1 in [Coq05]. Its proof involves only elementary properties of Riesz spaces.

Notice the interplay between the pointwise and pointfree framework. From a formal covering, in the lattice L ( R ), it is possible to deduce that Σ, a metric space, is totally bounded. This is remarkable since there are examples of Riesz spaces R such that in a recursive interpretation of Bishop's mathematics Σ does not have enough points. For instance, consider the Riesz space R of continuous real functions on Cantor space (2 ω ). The spectrum of R is precisely Cantor space and the representations are its points

. To see this, note that the characteristic function χu of any basic open u is continuous. So, given a representation σ, σ(χu∧(1 - χu)) = 0 and σ(χu∨(1 - χu)) = 1. Consequently, σ(χu) is either 0 or 1. It follows that the representations can be identified with the points.

2 , which is known not to have enough points in a recursive interpretation. In particular, this means that we have a collection of open sets which covers all the recursive points, but does not allow a finite subcover. This is possible since this collection does not cover the space in the usual terminology of formal topology.

3.f-algebras

In this section we apply the results of the previous section to f-algebras.

Definition 18. An f-algebra is a Riesz space with a strong unit and a commutative

. One can prove classically that the commutativity requirement follows form the other properties of an f-algebra. We intend to provide a constructive proof of this separately using the pointfree description of the spectrum.

3 multiplication such that 0⩽a b, whenever 0⩽a and 0⩽b.

3.1.f-algebra of operators

Example 19. If R is a complete commutative algebra of normable self-adjoint operators on a Hilbert space H, then R is a Riesz space with the order ⩽ defined by 0⩽A if and only if (A u, u)⩾0 for all u in H.

In the rest of this subsection we prove that if A,B⩾0, then A B⩾0.

We have now defined two notions of boundedness on the algebra of operators. One as a bounded operator: A is bounded by a if for all x, ‖A x2ax2. The other from the ordering: A is bounded by a if Aa I, where I is the identity operator.

Lemma 20. The two notions of boundedness coincide that is, for all x, (A x,x)⩽(a x,x) if and only if for all x, ‖A x2a2x2. Consequently, ‖A2‖ = ‖A2.

Proof. The usual proof, for instance in [Lan83] using the polarization identity, is constructive.

Since (A B 2x,x) = (A (B x),(B x)), we see that A B2⩾0, whenever A⩾0. This suffices to prove that R is an ordered ring.

Lemma 21. [Rie32] (p33, footnote 9) Let R be a as above. Then every positive element is the uniform limit of a sum of squares.

Proof. We can assume that 0⩽A⩽1. Define A0: = A and An + 1: = An - A
2
n
. Then 0⩽An + 1⩽1, since An + 1 = An(1 - An)2 + (1 - An)A
2
n
⩾0 and 1 - An + 1 = 1 - An + A
2
n
. Moreover, An + 1 = An - A
2
n
An. Since A = A
2
1
+ ⋯ + A
2
n
+ An + 1, we have A
2
n
⩽1/n→0. By Lemma 20 this implies that An→0.

Corollary 22. A B⩾0, whenever A,B⩾0.

Proof. If A,B⩾0, then (A B x,x) = ∑(A Bnx,Bnx)⩾0, where Bn is a sequence such that ΣB
2
n
converges to B.

The following lemma shows that one can construct the square root

. This is the usual lemma that R admits square root of positive elements if R is complete. Notice that the proof is directly constructive, and it corresponds to the usual Taylor expansion of (1 - x)1/2.

4 when R is complete and thus one can define the absolute value as | A |≔sqrt ( A 2 ). From the absolute value one first defines A + ≔(| A | + A )/2 and then ABA + ( B - A ) + . Consequently, the algebra is a Riesz space and an f-algebra.

Lemma 23. For all A⩾0 we can build a Cauchy sequence (An) of positive elements such that A

2
n
A.

Proof. We can assume 0≤AI. We define the two sequences An∈[0,I] and rn∈[0,1] defined by A0 = 0 and r0 = 0 and

A n + 1 =
1
2
(1 - A + A
2
n
) r n + 1 =
1
2
(1 + r
2
n
)

Clearly, we have Anrn for all n.

We claim that we have for all n

AnAn + 1rnrn + 1An + 1 - Anrn + 1 - rn

This is proved by induction from the equalities

A n + 1 - A n =
1
2
( A n + A n - 1 )( A n - A n - 1 ) r n + 1 - r n =
1
2
( r n + r n - 1 )( r n - r n - 1 )

It follows that we have

(I - An)2 - A = 2(An + 1 - An)≤2(rn + 1 - rn)

In order to conclude, all is left is to show that (rn) has limit 1. We know that 0≤rnrn + 1≤1 and we have

1 - r n + 1 =
1
2
(1 - r
2
n
) = (1 - r n )
1
2
(1 + r n )≤(1 - r n )(1 -
ϵ
2
)

if r n ≤1 - ϵ. This shows that if (1 -
ϵ
2
) N ≤ϵ we have 1 - r n ≤ϵ for all nN .

3.2.Gelfand representation

Any f-algebra is a Riesz space so we have a Gelfand representation of the f-algebra qua Riesz space, see Theorem 17.

Theorem 24. The Gelfand transform ⋅^ preserves multiplication.

Proof. Since 2a b = (a + b)2 - a2 - b2. We need to prove that ⋅^ preserves squares that is σ(a2) = σ(a)2. For this we first prove: σ(a b)>0, whenever σ(a),σ(b)>0.

If σ( a )⩾ r >0, then σ( a - r )>0. By Lemma 6.3 in [ Coq05 ], ( a - r ) + b +

1
r
( a b ) + , so σ( a b ) + r (σ( b ) + ∧σ( a - r ) + )>0, which was to be proved.

Suppose that |σ(a)| <q. Then q>σ(a) and so σ(q - a)>0. Similarly, σ(q + a)>0. Consequently, σ(q2 - a2) = σ((q - a)(q + a))>0. By a similar argument we see that if |σ(a)|<q, then |σ(a2)|<q2. We conclude that σ(a2) = σ(a)2.

We have proved the following representation theorem for f-algebras which explains the name f-algebra: an f-algebra is an abstract function algebra.

Theorem 25. [DC]Let A be a separable f-algebra of normable elements, then the spectrum Σ is a compact metric space and there exists an f-algebra embedding of A into C(Σ).

We now specialize this theorem to the f-algebra in Example 19 and obtain Bishop's version of the Gelfand representation theorem. In fact, like Bishop we first prove the theorem for Hermitian operators. As a corollary we obtain the Gelfand duality theorem for a separable Abelian C*-algebra, exactly as stated by Bishop [BB85] Cor.8.28 by considering its self-adjoint part which is an f-algebra.

Corollary 26. [DC]Let A be a separable f-algebra of normable Hermitian operators on a Hilbert space, then the spectrum is a compact metric space and there exists an f-algebra embedding of A into C(Σ).

Theorem 27. [DC]Let R be an Abelian C*-algebra of operators on a Hilbert space. Then there exists a C*-algebra embedding φ of R into C(Σ,C), where Σ is a compact metric space. Moreover, φ(1) = 1 and R is norm-dense.

Bishop's Gelfand representation theorem states that for any commutative algebra of normable operators on a separable Hilbert space there exists a norm-preserving isomorphism to the algebra of continuous functions on its spectrum. To prove that this map is norm-preserving Bishop proves that certain ε eigenvectors can be computed. In fact, the computational information of the ε eigenvectors is used only to prove the non-computational statement that the map is norm-preserving. In contrast, we work directly on the approximations so that we can avoid these unused computational steps.

3.3.Peter-Weyl

For a typical application, we let G be a compact group and R be the algebra of operators over L2(G) generated by the unit operator and the operators T(f)(g)≔fg, where ∗ denotes the convolution product. Each operator T(f) is compact and hence normable. The non-trivial representations of R are then exactly the characters of the group G. This gives a reduction of the Peter-Weyl theorem to the Gelfand representation theorem, see [CS05b].

4.Compact overt locales

Bishop defines a metric space to be compact if it is complete and totally bounded and proves that all uniformly continuous functions defined on such a metric space are normable. In contrast, in the framework of locale theory it is not true in general that all functions on a compact regular locale are normable, i.e. the norm is only defined as an upper real which may not be a located.

However, the locale considered in Theorem 8 is not only compact completely regular, but also overt that is, has a positivity predicate as shown by Proposition 9. In this case all the continuous functions are normable. This is a general fact.

Theorem 28. If X is a compact completely regular locale, then X is overt if and only if for any fC(X) there exists sup fR such that sup f<s if and only if f - 1( - ∞,s) = X.

Proof. We prove only the ‘only if' part. If X is overt and fC(X), then an approximation of the supremum can be found by considering a finite covering of X by positive opens of the form f - 1(r,s), where s - r is small.

The previous facts suggest a similarity between Bishop's compact metric spaces and the compact overt spaces in formal topology.

Bishop compact ⇔ compact overt

Clearly this requires further developments building on ideas in [ML70][Joh84]. However, we postpone this to further work.

It is interesting to note that Paul Taylor has independently found a similar relation between Bishop compact and compact overt in the context context of his abstract Stone duality [Tay05]. He also introduced the term overt.

We would like to conclude this discussion with the following comparison between the three following frameworks: classical mathematics with the axiom of choice, Bishop's mathematics and our framework, predicative constructive mathematics without dependent choice

. This framework is related to Richman's proposal to develop constructive mathematics without using countable choice, see [Ric00].

5 . Using classical logic and the axiom of choice one can show that the spectrum defined in Theorem 8 has enough points [ Joh82 ]. Thus in this setting the pointfree and pointwise description of the space coincide. In a recursive interpretation of Bishop's framework these descriptions differ. However, using dependent choice, normability and separability assumptions, we have shown how to deduce that Σ is totally bounded from the pointfree description of Σ.

Our conclusion is that the best formulation of the representation theorem is the pointfree one, since, besides being neutral on the use of the axiom of choice and classical logic, it implies the usual formulations both in Bishop's framework and in classical mathematics.

5.Choice

5.1.No points

As mentioned before, when all the elements of the algebra are normable, one can construct points in the spectrum using dependent choice. We claim that dependent choice is needed for this. In fact, it is known that there exist compact overt locales for which we need countable choice to construct a point. Thus it suffices to consider the space of continuous functions on such a locale. We think that a nice example can be extracted from [Ric00].

Richman [Ric00](p.5) gave an informal argument that indicates that one can not construct the zeroes of the complex polynomial X2 - a unless one knows whether a = 0 or not. To a in C we can associate the locale Ya of roots of X2 - a. The existence of a point in Ya requires dependent choice. On the other hand using results from [Vic03] it should be possible to show that Ya is compact overt as an element of the completion of the metric space n-multisets in C. The metric on this space is the usual Hausdorff metric on compact subsets of C.

Finally, we remark that this leaves open the question whether it is possible to construct the points of the spectrum of a discrete countable Riesz space over the rationals, or more generally, to construct the points of the spectrum of a separable Riesz space.

5.2.Spreads

It is interesting to note that Richman [Ric02] proposes to use spreads to avoid dependent choice. We suggest to use formal spaces instead. One motivation of formal topology [ML70][Sam87] was precisely to give a direct treatment of Brouwer's spreads by working with trees of finite sequences. Formal topology may be seen as a predicative and constructive version of locale theory. Johnstone [Joh82] stresses that one may avoid the use of the axiom of choice in topology by using locale theory and dealing directly with the opens. In this light it may not be so surprising that Richman uses spreads to avoid choice.

Richman's definition of spread differs in two respects from Heyting's definition. The branching of the tree is arbitrary, i.e. not necessarily indexed by the natural numbers, and it is not decidable whether or not a branch can be continued. This may be compared to the present situation where we study the maximal spectrum Σ. When Σ has a countable base, we may define it as a finitely branching tree. When furthermore Σ is overt, every positive branch can be continued in a positive way. One difference between Richman's spreads and our approach is that Richman requires the infinite branches to be elements of a metric space.

6.Conclusion

We gave a constructive proof of the Stone-Yosida representation theorem for Riesz spaces. This theorem was used to prove a representation theorem for f-algebras, from which we derived the Gelfand representation theorem for commutative C*-algebras of operators on a Hilbert space. This constructive theorem generalizes the one by Bishop and Bridges. In a similar way one may prove a generalization of Bishop's spectral theorem, see [Spi05].

It should be noted that we have used normability and separability hypothesis in the statements of the main theorems and used the axiom of dependent choice. In fact, without these hypothesis we can still obtain the spectrum as a compact locale. The normability is necessary to show that the spectrum is overt. The separability hypothesis is used to obtain a metric space instead of a uniform space. Finally, the axiom of dependent choice is used in Theorem 16 to construct a point in each positive open, and thus obtain a metric space in the sense of Bishop.

In this context, we would like to mention a problem for both constructive versions of the Gelfand representation theorem: can it be applied to construct the Bohr compactification of, say, the real line, like Loomis [Loo53]? Considering that the Stone-Čech compactification has been successfully treated in locale theory [Joh82], one would hope that a similar treatment is possible. Since the almost periodic functions do not form an algebra constructively, we may consider the f-algebra of functions generated by them. However, in this algebra not all elements are normable. Any element of the group determines a point in the spectrum. However, it is not possible to extend the group operation to the spectrum and obtain a localic group, since every compact localic group has a positivity predicate [Wra90] and since, moreover, the spectrum is compact this would imply that all the functions in the f-algebra are normable. This, as we stated before, is not the case. See Spitters [Spied] and the references therein for a constructive theory of almost periodic functions.

Bibliography

[BB85] Errett Bishop and Douglas Bridges. Constructive analysis, volume 279 of Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, 1985.

[Bir67] Garrett Birkhoff. Lattice theory. Third edition. American Mathematical Society Colloquium Publications, Vol. XXV. American Mathematical Society, Providence, R.I., 1967.

[Bou64] N. Bourbaki. Algèbre, chapitre 6. Hermann, 1964.

[Coq05] Thierry Coquand. About Stone's notion of spectrum. J. Pure Appl. Algebra, 197(1-3):141–158, 2005.

[CS05a] T. Coquand and B. Spitters. Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. Journal of Universal Computer Science, 11(12):1932–1944, 2005. http://www.jucs.org/jucs_11_12/formal_topotoly_and_constructive.

[CS05b] Thierry Coquand and Bas Spitters. A constructive proof of the Peter-Weyl theorem. Mathematical Logic Quarterly, 4:351–359, 2005.

[Joh82] Peter T. Johnstone. Stone Spaces. Number 3 in Cambridge studies in advanced mathematics. Cambridge University press, 1982.

[Joh84] Peter T. Johnstone. Open locales and exponentiation. In Mathematical applications of category theory (Denver, Col., 1983), volume 30 of Contemp. Math., pages 84–116. Amer. Math. Soc., Providence, RI, 1984.

[Lan83] Serge Lang. Real analysis. Addison-Wesley Publishing Company Advanced Book Program, Reading, MA, second edition, 1983.

[Loo53] Lynn H. Loomis. An introduction to Abstract Harmonic Analysis. University Series in Higher Mathematics. van Nostrand, New York, 1953.

[LZ71] W. A. J. Luxemburg and A. C. Zaanen. Riesz spaces. Vol. I. North-Holland Publishing Co., Amsterdam, 1971. North-Holland Mathematical Library.

[ML70] Per Martin-Löf. Notes on constructive mathematics. Almqvist & Wiksell, Stockholm, 1970.

[Ric98] Fred Richman. Generalized real numbers in constructive mathematics. Indagationes Mathematicae, 9:595–606, 1998.

[Ric00] Fred Richman. The fundamental theorem of algebra: a constructive development without choice. Pacific Journal of Mathematics, 196:213–230, 2000.

[Ric02] Fred Richman. Spreads and choice in constructive mathematics. Indagationes Mathematicae, 13:259–267, 2002.

[Rie32] F. Riesz. Ueber die linearen Transformationen des komplexen Hilbertschen Raumes. Acta Sci. Math., 5:23–54, 1930-32.

[Sam87] Giovanni Sambin. Intuitionistic formal spaces - a first communication. In D. Skordev, editor, Mathematical logic and its Applications, pages 187–204. Plenum, 1987.

[Spi05] Bas Spitters. Constructive algebraic integration theory without choice. Dagstuhl proceedings, 2005.

[Spied] Bas Spitters. Almost periodic functions, constructively. Logical Methods in Computer Science, accepted.

[Sto41] M. H. Stone. A general theory of spectra. II. Proc. Nat. Acad. Sci. U. S. A., 27:83–87, 1941.

[Tay05] Paul Taylor. A lambda calculus for real analysis. http://www.cs.man.ac.uk/~pt/ASD, August 2005.

[Vic03] Steven Vickers. Localic completion of generalized metric spaces I. submitted for publication, draft available on web at http://www.cs.bham.ac.uk/~sjv, 2003.

[Wra90] G. C. Wraith. Unsurprising results on localic groups. J. Pure Appl. Algebra, 67(1):95–100, 1990.

[Yos42] Kôsaku Yosida. On the representation of the vector lattice. Proc. Imp. Acad. Tokyo, 18:339–342, 1942.