The Hahn-Banach Theorem in Type Theory

Jan Cederquist and Thierry Coquand Department of Computing Science University of Göteborg

and

Sara Negri Department of Philosophy University of Helsinki

Abstract We give the basic definitions for pointfree functional analysis and present constructive proofs of the Alaoglu and Hahn-Banach theorems in the setting of formal topology.

1 Introduction

We present the basic concepts and definitions needed in a pointfree approach to functional analysis via formal topology. Our main results are the constructive proofs of localic formulations of the Alaoglu and Helly-Hahn-Banach^{1} theorems.

Earlier pointfree formulations of the Hahn-Banach theorem, in a topostheoretic setting, were presented by Mulvey and Pelletier (1987,1991) and by Vermeulen (1986). A constructive proof based on points was given by Bishop (1967). In the formulation of his proof, the norm of the linear functional is preserved to an arbitrary degree by the extension and a counterexample shows that the norm, in general, is not preserved exactly.

As usual in pointfree topology, our guideline is to define the objects under analysis as formal points of a suitable formal space. After this has been accomplished for the reals, we consider the formal topology L(A) obtained as follows: To the formal space of mappings from a normed vector space A to the reals, we add the linearity and norm conditions in the form of covering axioms. The linear functionals of norm ≤ 1 from A to the reals then correspond to the formal points of this formal topology.

Given a subspace M of A, the classical Helly-Hahn-Banach theorem says that the restriction mapping from the linear functionals on A of norm ≤ 1 to those on M is surjective. In terms of covers, conceived as deductive systems, it becomes a conservativity statement (cf. Mulvey and Pelletier 1991): Whenever a is an element and U is a subset of the base of the formal space L(M) and we have a derivation in L(A) of a ⊲ U, then we can find a derivation in L(M) with the same conclusion.

1As explained by Hochstad (1980), the main idea in the usual proof of what is called the Hahn-Banach theorem is due to Helly. Since this is also the key idea in our derivation, we here rename the theorem in this way.

With this formulation it is quite natural to look for a proof by induction on covers. Moreover, as already pointed out by Mulvey and Pelletier (1991), it is possible to simplify the problem greatly, since it is enough to prove it for coherent spaces of which L(A) and L(M) are retracts. Then, in a derivation of a cover, we can assume that only finite subsets occur on the right-hand side of the cover relation. A global proof transformation makes it possible to change a derivation in L(A) into a derivation in L(M), since only a finite-dimensional extension of the space M has to be taken into account. In consequence, as in the case for the classical proof for the one-dimensional extension, no use of Zorn’s lemma is needed.

Of the earlier two pointfree proofs of the Hahn-Banach theorem, the one of Mulvey and Pelletier (1991) shows the Hahn-Banach theorem in any Grothendieck topos. However, the argument relies on Barr’s theorem, for which no constructive justification has been given so far. The proof of Vermeulen (1986) is done in the framework of topos theory with a natural number object, and thus, a priori, relies on the use of impredicative quantification.

Here as elsewhere (cf. Cederquist and Negri 1996; Coquand 1992, 1996; Negri and Valentini 1995) the use of formal topology allows for elementary and constructive proofs of pointfree formulations of classical results.

The two main contributions of this paper are the following:

• Our proof of the pointfree version of the Hahn-Banach theorem, following rather closely the original proof by Helly.

• This proof can actually be expressed in Martin-Löf’s Type Theory (cf. Martin-Löf 1972). In fact, on the basis of our proof, the first author has done a formalisation of the Hahn-Banach theorem in an implementation of the intensional version of Type Theory with one universe and finitary inductive definitions (see Cederquist 1997).

2 Preliminaries

We recall here the definition of formal topology introduced by Per Martin-Löf and Giovanni Sambin (see Sambin 1987). We remark that, in contrast to the definition given by Sambin and without any substantial difference in the development of the theory, we do not require the base monoid to have a unit. Nor do we have the positivity predicate used by Sambin.

Definition 2.1. (Formal topology) A formal topology over a set S is a structure ⟨S, ·, ⊲⟩, where ⟨S, ·⟩ is a commutative monoid, ⊲ is a relation, called cover, between elements and subsets of S such that, for any a, b ∈ S and U, V ⊆ S, the following conditions hold:

(reflexivity)  \frac{a ∈ U}{a ⊲ U}

(transitivity) \frac{a ⊲ U  U ⊲ V}{a ⊲ V}  where U ⊲ V ≡ (∀u ∈ U)(u ⊲ V)

(dot - left)  \frac{a ⊲ U}{a · b ⊲ U}

(dot - right) \frac{a ⊲ U  a ⊲ V}{a ⊲ U · V}  where U · V ≡ \{u · v | u ∈ U, v ∈ V \}.

For readability reasons, when a singleton set occurs we will sometimes omit curly brackets, and write a ⊲ b for a ⊲ {b}, and U · b for U · {b}.

Since we dropped the unit element and the positivity predicate in the definition of formal topology, the definition of formal points given by Sambin (1987) has to be revised as follows:

Definition 2.2 Let ⟨S, ·, ⊲⟩ be a formal topology. A subset α of S is said to be a formal point if for all a, b ∈ S, U ⊆ S the following conditions hold:

(1) (∃a ∈ S)(a ∈ α) ;

(2) \frac{a ∈ α b ∈ α}{a · b ∈ α} ;

(3) \frac{a ∈ α a ⊲ U}{(∃b ∈ U)(b ∈ α)} .

In order to maintain the usual intuition on points, in the sequel we will write α ⊩ a (α forces a, or α is a point in a) in place of a ∈ α.

As an instance of the abstract definition of formal topology the continuum can be defined as a formal space. The proofs that this definition satisfies the rules of a formal topology can all be found in Cederquist and Negri 1996. Further properties of the continuum as a formal space can also be found in Negri and Soravia 1996, where a slightly different definition adopting the unit is given.

Definition 2.3 The formal topology of formal reals is the structure

R ≡ ⟨Q × Q, ·, ⊲_{R}⟩,

where Q is the set of rational numbers. The monoid operation is defined by (p, q) · (r, s) ≡ (max(p, r), min(q, s)), the cover ⊲_{R} by

(p, q) ⊲_{R} U ≡ (∀p′, q′)(p < p′ < q′ < q → (p′, q′) ⊲_{R_{f}} U)

where the relation ⊲_{R_{f}} is inductively defined by

(1) \frac{q ≤ p}{(p, q) ⊲_{R_{f}} U} ;

(2) \frac{(p, q) ∈ U}{(p, q) ⊲_{R_{f}} U} ;

(3) \frac{p ≤ r < s ≤ q (p, s) ⊲_{R_{f}} U (r, q) ⊲_{R_{f}} U}{(p, q) ⊲_{R_{f}} U} ;

(4) \frac{p′ ≤ p < q ≤ q′ (p′, q′) ⊲_{R_{f}} U}{(p, q) ⊲_{R_{f}} U} .

We denote with P t(R) the collection of formal points of R, called formal reals.

In Cederquist and Negri 1996 it is proved that ⊲_{R_{f}} and ⊲_{R} are cover relations. Moreover, ⊲_{R_{f}} is a Stone cover, since we have: Proposition 2.4 If (p, q) ⊲_{R_{f}} U, then there exists a finite subset U_{0} of U such that (p, q) ⊲_{R_{f}} U_{0}. Proof: See Cederquist and Negri 1996. □

In Cederquist and Negri 1996 it is also proved that whenever (p, q) ⊲_{R} U and U is finite then (p, q) ⊲_{R_{f}} U and therefore ⊲_{R_{f}} is the Stone compactification (cf. Sambin 1987; Negri 1996) of ⊲_{R}, but this stronger result will not be used in the sequel.

With I = (p, q) and J = (r, s), we write I < J (resp. I ≤ J) to express that r < p < q < s (resp. r ≤ p < q ≤ s). Thus I ⊲_{R} U means J ⊲_{R_{f}} U for all J < I. Moreover, we use the notations I + J for (p + r, q + s), and tI for (tp, tq) when t ≥ 0 and for (tq, tp) when t < 0.

The following lemma will be used in section 3. Lemma 2.5 If J < I and I ⊲_{R_{f}} U, then there exists a subset V of Q×Q such that (∀K ∈ V)(∃L ∈ U)(K < L) and J ⊲_{R_{f}} V. Proof: Straightforward by induction on the derivation of I ⊲_{R_{f}} U. □

3 Formal linear functionals

In this section we define the space of linear functionals of norm ≤ 1 from a seminormed space to the reals. This space is obtained by means of an inductive definition giving rise to a formal topology: Basic neighbourhoods correspond to basic opens in the weak^{∗} topology (Brezis 1983) and formal points correspond to the linear functionals of norm ≤ 1 from the given seminormed space to the space of formal reals.

Moreover, the formal cover for this space is defined explicitly from a Stone cover, and therefore a simple proof of Alaoglu’s theorem is obtained.

3.1 The dual of a seminormed space as a formal space We start by defining a seminormed space as in Mulvey and Pelletier 1991. The seminorm is defined by means of formal open balls centred around the origin. Definition 3.1 A seminormed space A on the rationals Q is a linear space A on Q together with a mapping

N : Q^{+} ⟶ P(A)

from the positive rationals to the subsets of A satisfying the following conditions for x, x′ ∈ A, q, q′ ∈ Q^{+}:

N1. x ∈ N(q) → (∃q′ < q)(x ∈ N(q′)) ; N2. (∃q)(x ∈ N(q)) ; N3. x ∈ N(q) & x′ ∈ N(q′) → x + x′ ∈ N(q + q′) ; N4. x ∈ N(q′) → qx ∈ N(qq′) ; N5. x ∈ N(q) → −x ∈ N(q) ; N6. 0 ∈ N(q) .

We limit ourselves to the presentation of the formal space L(A) of linear functionals of norm ≤ 1. The basic opens are finite sets of the form

w ≡ {⟨x_{1} ∈ I_{1}⟩, …, ⟨x_{n} ∈ I_{n}⟩} ,

where x_{1}, …, x_{n} ∈ A and I_{1}, …, I_{n} are rational intervals. The intuitive reading of a basic open is that of a neighbourhood of functionals in the weak^{∗} topology. We will in the sequel use the notation ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ for {⟨x_{1} ∈ I_{1}⟩, …, ⟨x_{n} ∈ I_{n}⟩}.

We obtain with the operation

w_{1}w_{2} ≡ w_{1} ∪ w_{2}

a commutative and idempotent monoid with unit given by the empty set. We will denote with S_{L(A)} such a base of L(A).

Let w ≡ ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩, then define

w ≤ ⟨x ∈ I⟩ ≡ (∃⟨x_{i_{1}} ∈ I_{i_{1}}⟩, …, ⟨x_{i_{p}} ∈ I_{i_{p}}⟩ ∈ w)
(x_{i_{1}} = … = x_{i_{p}} = x & I_{i_{1}} · . . . · I_{i_{p}} ≤ I)

and

w ≤ w′ ≡ (∀⟨x ∈ I⟩ ∈ w′)(w ≤ ⟨x ∈ I⟩).

Then, without assuming decidability of equality in A, ≤ is a reflexive and transitive relation.

Equality between basic neighbourhoods is subset equality

w = w′ ≡ (∀⟨x ∈ I⟩)(⟨x ∈ I⟩ ∈ w ⇔ ⟨x ∈ I⟩ ∈ w′) .

Notice that w = w′ implies w ≤ w′. This defines an equivalence relation on the type of basic neighbourhoods. We follow Bishop (1967) in working systematically with types with an equivalence relation. Whenever we define a predicate, we have to be careful to check that this predicate respects the equivalence relation.

The finitary cover ⊲_{f} for L(A) is inductively defined as follows:

C1 \frac{w ∈ U}{w ⊲_{f} U} ;

C2 \frac{w ≤ w′ w′ ⊲_{f} U}{w ⊲_{f} U} ;

C3 \frac{V finite I ⊲_{R_{f}} V (∀J ∈ V)(⟨x ∈ J⟩w′ ⊲_{f} U)}{⟨x ∈ I⟩w′ ⊲_{f} U} ;

C4 \frac{⟨x + y ∈ I + J⟩w′ ⊲_{f} U}{⟨x ∈ I, y ∈ J⟩w′ ⊲_{f} U} ;

C5 \frac{r ≠ 0 ⟨rx ∈ rI⟩w′ ⊲_{f} U}{⟨x ∈ I⟩w′ ⊲_{f} U} ;

C6 \frac{x ∈ N(1) ⟨x ∈ (−1, 1)⟩w ⊲_{f} U}{w ⊲_{f} U} .

A motivation for the above definition can be given as follows: conditions C1-C3 define formal functionals from A to the formal reals, C4 and C5 impose linearity and C6 says that we only consider functionals of norm ≤ 1.

Notice that, by C2, we have w ⊲_{f} U whenever w = w′ and w′ ⊲_{f} U.

In order to get a finitary inductive definition, the subset V in clause C3 has to be finite. This however is not a restriction since ⊲_{R_{f}} is a Stone cover and such a finite set can always be found.

We have:

Proposition 3.2 The relation ⊲_{f} is a cover.

Proof: Reflexivity holds by definition, dot-left follows from C2 since w_{1}w_{2} ≤ w_{1}, transitivity and localization are straightforward by induction on the derivation of w ⊲_{f} U. □

Then ⊲ is defined by

⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U ≡
(∀J_{1} < I_{1}, …, J_{n} < I_{n})(⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U).

Next, we prove that ⊲ is a cover, but before that some lemmas are needed.

Lemma 3.3 If ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ≤ ⟨y_{1} ∈ L_{1}, …, y_{m} ∈ L_{m}⟩ and J_{1} < K_{1}, …, J_{n} < K_{n}, then (∃L′_{1} < L_{1}, …, L′_{m} < L_{m})(⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ≤ ⟨y_{1} ∈ L′_{1}, …, y_{m} ∈ L′_{m}⟩).

Proof: Starting from the hypotheses ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ≤ ⟨y_{1} ∈ L_{1}, …, y_{m} ∈ L_{m}⟩ and J_{1} < K_{1}, …, J_{n} < K_{n}, the intervals L′_{i} (1 ≤ i ≤ m) are constructed in the following way. By definition, for each i ≤ m there exists p_{1}, …, p_{k} such that x_{p_{1}} = … = x_{p_{k}} = y_{i} and K_{p_{1}} · . . . · K_{p_{k}} ≤ L_{i}. Since J_{1} < K_{1}, …, J_{n} < K_{n} we have J_{p_{1}} · . . . · J_{p_{k}} < L_{i}. Thus we put L′_{i} = J_{p_{1}} · . . . · J_{p_{k}}. □

The following lemma makes the definition of ⊲ legitimate.

Lemma 3.4 The relation ⊲ respects equality between basic neighbourhoods.

Proof: We will show that C2 also holds for ⊲. The conclusion then follows since w = w′ implies w ≤ w′.

Suppose ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ≤ ⟨y_{1} ∈ J_{1}, …, y_{m} ∈ J_{m}⟩ and ⟨y_{1} ∈ J_{1}, …, y_{m} ∈ J_{m}⟩ ⊲ U. Let I′_{1} < I_{1}, …, I′_{n} < I_{n}. Then, by Lemma 3.3, there exist J′_{1} < J_{1}, …, J′_{m} < J_{m} such that ⟨x_{1} ∈ I′_{1}, …, x_{n} ∈ I′_{n}⟩ ≤ ⟨y_{1} ∈ J′_{1}, …, y_{m} ∈ J′_{m}⟩. For such J′_{1}, …, J′_{m} we have ⟨y_{1} ∈ J′_{1}, …, y_{m} ∈ J′_{m}⟩ ⊲_{f} U and, by C2, ⟨x_{1} ∈ I′_{1}, …, x_{n} ∈ I′_{n}⟩ ⊲_{f} U. Therefore ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U. □ Lemma 3.5 If w ⊲_{f} U then w ⊲ U. Proof: Suppose ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲_{f} U and let J_{1} < I_{1}, …, J_{n} < I_{n}. Then ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ≤ ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ so, by C2, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U. Therefore ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U. □

The following lemma is used in the proof of transitivity for ⊲. Lemma 3.6 If ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U, J_{1} < K_{1}, …, J_{n} < K_{n} and U ⊲ V, then ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V. Proof: By induction on the derivation of ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U.

1. If ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ∈ U then ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲ V, thus by definition, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V.

2. If ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U is derived by C2 from ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ≤ ⟨y_{1} ∈ L_{1}, …, y_{n} ∈ L_{m}⟩ and ⟨y_{1} ∈ L_{1}, …, y_{n} ∈ L_{m}⟩ ⊲_{f} U, then by Lemma 3.3 there exist L′_{1} < L_{1}, …, L′_{m} < L_{m} such that ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ≤ ⟨y_{1} ∈ L′_{1}, …, y_{n} ∈ L′_{m}⟩. For such L′_{1}, …, L′_{m}, by induction hypothesis, ⟨y_{1} ∈ L′_{1}, …, y_{n} ∈ L′_{m}⟩ ⊲_{f} V. Then, by C2, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V.

3. Let ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U be derived by C3 from K_{1} ⊲_{R_{f}} V′ and (∀J′ ∈ V′)(⟨x_{1} ∈ J′, x_{2} ∈ K_{2}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U), where V′ is finite. Since J_{1} < K_{1} and K_{1} ⊲_{R_{f}} V′, by Lemma 2.5, we can construct a finite subset V′′ such that J_{1} ⊲_{R_{f}} V′′ and (∀J′′ ∈ V′′)(∃J′ ∈ V′)(J′′ < J′). Then, by induction hypothesis, (∀J′′ ∈ V′′)(⟨x_{1} ∈ J′′, x_{2} ∈ J_{2}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V) and, by C3, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V.

4. Let ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U be derived by C4 from ⟨x_{1} + x_{2} ∈ K_{1} + K_{2}, x_{3} ∈ K_{3} …, x_{n} ∈ K_{n}⟩ ⊲_{f} U. Then J_{1} + J_{2} < K_{1} + K_{2} so, by induction hypothesis, ⟨x_{1} + x_{2} ∈ J_{1} + J_{2}, x_{3} ∈ J_{3} …, x_{n} ∈ J_{n}⟩ ⊲_{f} V and, by C4, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V.

5. Similar to 4.

6. Let ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U be derived by C6 from ⟨x ∈ (−1, 1), x_{1} ∈ K_{1} …, x_{n} ∈ K_{n}⟩ ⊲_{f} U and x ∈ N(1). By N1 there exists an r < 1 such that x ∈ N(r). For such an r, by induction hypothesis, ⟨x ∈ (−r, r), x_{1} ∈ J_{1} …, x_{n} ∈ J_{n}⟩ ⊲_{f} V. Now the claim follows by C6. □

We are now ready to prove: Proposition 3.7 The relation ⊲ is a cover. Proof: Reflexivity: Immediate from reflexivity of ⊲_{f} and Lemma 3.5.

Dot-left, dot-right: Immediate from the definition of ⊲ and the corresponding properties of ⊲_{f}.

Transitivity: Suppose ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U and U ⊲ V. If J_{1} < I_{1}, …, J_{n} < I_{n}, then we can find K_{1}, …, K_{n} such that J_{1} < K_{1} < I_{1}, …, J_{n} < K_{n} < I_{n} and, by definition of ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U, we get ⟨x_{1} ∈ K_{1}, …, x_{n} ∈ K_{n}⟩ ⊲_{f} U. Lemma 3.6 now gives ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} V. Thus ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ V. □

Finally, the following lemma will be useful in section 4.

Lemma 3.8 The axioms for ⊲_{f} are valid rules for ⊲.

Proof: 1: Given w ∈ U, w ⊲ U is immediate from C1 and Lemma 3.5. 2: See the proof of Lemma 3.4. 3: Suppose I_{1} ⊲_{R} V and (∀J ∈ V)(⟨x_{1} ∈ J⟩⟨x_{2} ∈ I_{2}, …, x_{n} ∈ I_{n}⟩ ⊲ U). Let

I′_{1} < I_{1}, …, I′_{n} < I_{n}. Then there exists I′′ such that I′_{1} < I′′ < I_{1}. For such an I′′, I′′ ⊲_{R_{f}} V so by Lemma 2.5 there exists a subset V′ such that I′_{1} ⊲_{R_{f}} V′ and (∀L′ ∈ V′)(∃L ∈ V)(L′ < L). But then, since ⊲_{R_{f}} is a Stone cover, there exists a finite subset V′_{0} ⊆ V′ such that I′_{1} ⊲_{R_{f}} V′_{0} and (∀L′ ∈ V′_{0})(∃L ∈ V)(L′ < L). Now, by definition of ⊲, (∀J′ ∈ V′_{0})(⟨x_{1} ∈ J′⟩⟨x_{2} ∈ I′_{2}, …, x_{n} ∈ I′_{n}⟩ ⊲_{f} U) and, by C3, ⟨x_{1} ∈ I′_{1}, …, x_{n} ∈ I′_{n}⟩ ⊲_{f} U. Therefore ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲_{f} U.

4 and 5 follow easily from the definition of ⊲_{f}, C4 and C5, respectively. 6: Suppose x ∈ N(1) and ⟨x ∈ (−1, 1), x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U. Let

J_{1} < I_{1}, …, J_{n} < I_{n}. By N1, there exists r < 1 such that x ∈ N(r). For such an r, \frac{1}{r}x ∈ N(1). Now, by C5 and the definition of ⊲, ⟨\frac{1}{r}x ∈ (−1, 1), x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U and, by C6, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U. Therefore ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U. □

3.2 Linear functionals as formal points In this section, which is not needed for the proof of the Hahn-Banach theorem, we will show how linear functionals of norm ≤ 1 from A to the formal space of reals are obtained in our setting. We denote the collection of formal points of L(A) with P t(L(A)). Given F ∈ P t(L(A)) and x ∈ A, let

F^{∗}(x) ≡ {(p, q) ∈ Q × Q : F ⊩ ⟨x ∈ (p, q)⟩}.

The following propositions are easily proved from the definitions (see also Mulvey and Pelletier 1987):

Proposition 3.9 F^{∗} is a linear functional from A to P t(R) of norm ≤ 1, that is:

(1) For all x ∈ A, F^{∗}(x) ∈ P t(R);

(2) F^{∗}(x + y) = F^{∗}(x) + F^{∗}(y);

(3) F^{∗}(tx) = tF^{∗}(x);

(4) x ∈ N(1) ⇒ −1 < F^{∗}(x) < 1.

Conversely, given a linear functional f from A to P t(R), that is, a map satisfying 1–4 as in Proposition 3.9, let f^{∘} be the subset of S_{L(A)} defined by

f^{∘} ≡ {⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ : f(x_{1}) ⊩ I_{1}, …, f(x_{n}) ⊩ I_{n}}.

Then we have:

Proposition 3.10 f^{∘} ∈ P t(L(A)).

The correspondence stated above is biunivocal since we have, with the notation used above, (f^{∘})^{∗} = f and (F^{∗})^{∘} = F.

3.3 Alaoglu’s theorem The cover ⊲_{f} is a Stone cover, since we have:

Proposition 3.11 If w ⊲_{f} U, then there exists a finite subset U_{0} of U such that w ⊲_{f} U_{0}.

Proof: The proof is straightforward by induction on the derivation of w ⊲_{f} U. We will only consider the case when w ⊲_{f} U is obtained by C3 from w ≡ ⟨x ∈ I⟩w′, I ⊲_{R_{f}} V and (∀J ∈ V)(⟨x ∈ J⟩w′ ⊲_{f} U), for a finite subset V. By induction hypothesis, given an element J ∈ V, there exists a finite subset U_{J} of U such that ⟨x ∈ J⟩w′ ⊲_{f} U_{J}. Let U_{0} be the union of all such U_{J}’s. Then by C3, w ⊲_{f} U_{0}. □

As an immediate consequence of the definition of the cover for L(A), we obtain Alaoglu’s theorem, asserting that the unit ball of the space of linear and continuous functionals is compact in the weak^{∗} topology.

Corollary 3.12 The formal space L(A) is compact.

Proof: Given ⟨ ⟩ ⊲ U, by definition of ⊲, ⟨ ⟩ ⊲_{f} U. Then, since ⊲_{f} is a Stone cover, ⟨ ⟩ ⊲_{f} U_{0} for some finite subset U_{0} of U. Therefore, by Lemma 3.5, ⟨ ⟩ ⊲ U_{0}. □

4 The Helly-Hahn-Banach theorem

In this section we prove the localic version of the Helly-Hahn-Banach theorem in the form of a conservativity result of the theory for the cover in L(A) over that in L(M). At the end of the section we also provide an informal motivation why this result is the localic statement of the usual point-set theorem.

The definition of ⊲ in terms of ⊲_{f} allows us to replace ⊲ with ⊲_{f} for proving conservativity. If M is a linear subspace of A, we say that ⊲_{f} for L(A) is conservative over ⊲_{f} for L(M) if, whenever w is an element and U is a subset of the base of L(M) and w ⊲_{f} U in L(A), then w ⊲_{f} U in L(M). Conservativity of ⊲ for L(A) over ⊲ for L(M) is defined in the same way. Then we have:

Proposition 4.1 If ⊲_{f} for L(A) is conservative over ⊲_{f} for L(M), then ⊲ for L(A) is conservative over ⊲ for L(M).

Proof: If ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U in L(A), then, for all J_{1} < I_{1}, …, J_{n} < I_{n}, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U, hence by conservativity for ⊲_{f}, for all J_{1} < I_{1}, …, J_{n} < I_{n}, ⟨x_{1} ∈ J_{1}, …, x_{n} ∈ J_{n}⟩ ⊲_{f} U in L(M) and hence ⟨x_{1} ∈ I_{1}, …, x_{n} ∈ I_{n}⟩ ⊲ U in L(M). □

The localic statement of the Helly-Hahn-Banach theorem in the framework of formal topologies is, “⊲ for L(A) is conservative over ⊲ for L(M)”. By the above proposition it thus reduces to the following:

Theorem 4.2 ⊲_{f} for L(A) is conservative over ⊲_{f} for L(M).

Since ⊲_{f} is a Stone cover, we can transform any derivation of a ⊲_{f} U in L(A) into one in which only finite subsets occur on the right-hand side of the cover relation. Therefore we can assume that only a finite number of elements not belonging to the base of L(M) are involved. Thus, arguing by induction, the problem is reduced to showing that if a ⊲_{f} U is derived in L(M′), where M′ ≡ [M + x] and x is an element in the base of L(A), then there exists also a derivation of a ⊲_{f} U in L(M). The claim of Theorem 4.2 thus becomes:

Proposition 4.3 ⊲_{f} for L(M′) is conservative over ⊲_{f} for L(M).

We will use the notations w ⊲_{M_{f}} U and w ⊲_{M′_{f}} U to express that w ⊲_{f} U in L(M) and L(M′), respectively. Before proving the proposition, some auxiliary lemmas will be needed.

Lemma 4.4 ⟨y +z ∈ (p, q)⟩ ⊲ {⟨y ∈ (r, s), z ∈ (r′, s′)⟩ : p ≤ r +r′ < s+s′ ≤ q}

Proof: Since (p′′, q′′) < (p, q) implies that

⟨y + z ∈ (p′′, q′′)⟩ ∈ {⟨y + z ∈ (p′, q′)⟩ : p < p′ < q′ < q} ,

we have by definition of ⊲ that

⟨y + z ∈ (p, q)⟩ ⊲ {⟨y + z ∈ (p′, q′)⟩ : p < p′ < q′ < q}.

By N2 and 3.8(6) we have

⟨ ⟩ ⊲ {⟨y ∈ (r, s)⟩ : r < s} ,

and similarly

⟨ ⟩ ⊲ {⟨z ∈ (r′, s′)⟩ : r′ < s′} ,

so by stability

\begin{aligned}⟨y + z ∈ (p, q)⟩ ⊲ \{ & ⟨y + z ∈ (p′, q′), y ∈ (r, s), z ∈ (r′, s′)⟩ : \\ & p < p′ < q′ < q, r < s, r′ < s′\} . \end{aligned}

Since every interval can be covered by arbitrarily small intervals, using 3.8(3), we get

⟨y + z ∈ (p, q)⟩ ⊲ {⟨y + z ∈ (p′, q′), y ∈ (r, s), z ∈ (r′, s′)⟩ :
p < p′ < q′ < q, r < s, r′ < s′,
s − r ≤ min(p′ − p, q − q′)/2,
s′ − r′ ≤ min(p′ − p, q − q′)/2}

and by 3.8(4)

⟨y + z ∈ (p, q)⟩ ⊲ {⟨y + z ∈ (p′, q′), y ∈ (r, s), z ∈ (r′, s′), y + z ∈ (r + r′, s + s′)⟩ :
p < p′ < q′ < q, r < s, r′ < s′,
s − r ≤ min(p′ − p, q − q′)/2,
s′ − r′ ≤ min(p′ − p, q − q′)/2} .

Now, if r + r′ < p then s + s′ < p′ and, by 3.8(2),

⟨y + z ∈ (p′, q′), y + z ∈ (r + r′, s + s′)⟩ ⊲ ⟨y + z ∈ (p′, s + s′)⟩.

Then, since s + s′ < p′, the right-hand side is covered by anything, in particular the empty set. If q < s + s′ we obtain symmetrically ⟨y + z ∈ (p′, q′), y + z ∈ (r + r′, s + s′)⟩ ⊲ ⟨y + z ∈ (r + r′, q′)⟩, where q′ < r + r′. We thus obtain

⟨y + z ∈ (p, q)⟩ ⊲ {⟨y ∈ (r, s), z ∈ (r′, s′)⟩ : p ≤ r + r′ < s + s′ ≤ q}. □

Let I be a finite index set, {a_{n}} and {t_{n}} sequences of A and Q, respectively, such that (∀i ∈ I)(a_{i} ∈ M & a_{i} + t_{i}x ∈ N(1)). Then, for rational q, define

P_{q} = ⟨…, a_{i} ∈ (−1 + t_{i}q, 1 + t_{i}q), …⟩.

The following lemma is the core of our proof. Intuitively it says that we can find a rational approximation for the value of u(x), where u is a generic linear functional. We observe that the argument is similar to the one used by Helly.

Lemma 4.5 ⟨ ⟩ ⊲_{M_{f}} {P_{q} : q ∈ Q}.

Proof: First observe that for all i ∈ I such that t_{i} = 0, we can apply C6 and dot-right. So, in the rest of this proof, we can assume that t_{i} ≠ 0 for all i. For any i, j ∈ I, by the rules of N we have

\begin{aligned}\{ \begin{matrix}a_{i} + t_{i}x ∈ N(1) \\ a_{j} + t_{j}x ∈ N(1) \end{matrix} & ⇒ & \{ \begin{matrix}a_{i}/t_{i} + x ∈ N(1/|t_{i}|) \\ −a_{j}/t_{j} − x ∈ N(1/|t_{j}|) \end{matrix} \\ & ⇒ & a_{i}/t_{i} − a_{j}/t_{j} ∈ N(1/|t_{i}| + 1/|t_{j}|) . \end{aligned}

By the rules for ⊲_{M_{f}} we get

⟨ ⟩ ⊲_{M_{f}} ⟨a_{i}/t_{i} − a_{j}/t_{j} ∈ (−1/|t_{i}| − 1/|t_{j}|, 1/|t_{i}| + 1/|t_{j}|)⟩,

by Lemmas 3.5 and 4.4

\begin{aligned}⟨ ⟩ ⊲_{M} \{ & ⟨a_{i}/t_{i} ∈ (r_{i}, s_{i}), a_{j}/t_{j} ∈ (r_{j}, s_{j})⟩ : \\ & −1/|t_{i}| − 1/|t_{j}| ≤ r_{i} − s_{j} < s_{i} − r_{j} ≤ 1/|t_{i}| + 1/|t_{j}|\}. \end{aligned}

From the definition of ⊲ we obtain the same for ⊲_{f}, and by dot-right

\begin{aligned}⟨ ⟩ ⊲_{M_{f}} \{ & ⟨…, a_{i}/t_{i} ∈ (r_{i}, s_{i}), …⟩ : \\ & (∀i, j ∈ I)(−1/|t_{i}| − 1/|t_{j}| ≤ r_{i} − s_{j} < s_{i} − r_{j} ≤ 1/|t_{i}| + 1/|t_{j}|)\} \end{aligned}

⇒

⟨ ⟩ ⊲_{M_{f}} {⟨…, a_{i}/t_{i} ∈ (r_{i}, s_{i}), …⟩ : (∀i, j ∈ I)(s_{i} − 1/|t_{i}| ≤ r_{j} + 1/|t_{j}|)}

⇒

⟨ ⟩ ⊲_{M_{f}} {⟨…, a_{i}/t_{i} ∈ (r_{i}, s_{i}), …⟩ : ⋁_{i∈I}(s_{i} − 1/|t_{i}|) ≤ ⋀_{i∈I}(r_{i} + 1/|t_{i}|)}.

Now there are two cases depending on whether t_{i} is positive or negative; we only consider the case when t_{i} is positive.

⟨ ⟩ ⊲_{M_{f}} {⟨…, a_{i} ∈ (t_{i}r_{i}, t_{i}s_{i}), …⟩ : ⋁_{i∈I}(s_{i} − 1/|t_{i}|) ≤ ⋀_{i∈I}(r_{i} + 1/|t_{i}|)}.

If q = ⋁_{i∈I}(s_{i} −1/|t_{i}|), then −1+qt_{i} ≤ t_{i}r_{i} < t_{i}s_{i} ≤ 1+qt_{i}, because s_{i} −1/|t_{i}| ≤ q ≤ r_{i} + 1/|t_{i}|, so we get

⟨ ⟩ ⊲_{M_{f}} {P_{q} : q ≡ ⋁_{i∈I}(s_{i} − 1/|t_{i}|) ≤ ⋀_{i∈I}(r_{i} + 1/|t_{i}|)}.

and a fortiori ⟨ ⟩ ⊲_{M_{f}} {P_{q} : q ∈ Q}. □

Let I be a finite set as above. We define ⊲′_{M′_{f}} as ⊲_{M′_{f}}, where the axiom C6 is replaced by

C6′ : \frac{i ∈ I ⟨a_{i} + t_{i}x ∈ (−1, 1)⟩w ⊲′_{M′_{f}} U}{w ⊲′_{M′_{f}} U} .

Let w ≡ ⟨…, b_{j} + u_{j}x ∈ (r_{j}, s_{j}), …⟩ be an element in the base of M′ and let q be a rational number. Then define

w̄ ≡ ⟨…, b_{j} ∈ (r_{j} + u_{j}q, s_{j} + u_{j}q), …⟩,
Ū ≡ {w̄ : w ∈ U}.

Note that w̄ depends on the proof of w ∈ S_{L(M′)}, and if x ∈ M there are many ways of writing b_{j} + u_{j}x and thus many proofs of w ∈ S_{L(M′)}.

We have:

Lemma 4.6 If w ⊲′_{M′_{f}} U, then x ∈ M ∨ (∀q ∈ Q)(P_{q}w̄ ⊲_{M_{f}} Ū).

Proof: By induction on the derivation of w ⊲′_{M′_{f}} U. We only consider the cases C1′ and C6′.

C1′: Given w ∈ U, since U ⊆ S_{L(M′)} we have two proofs of w ∈ S_{L(M′)} and two possibly different values of w̄, ⟨…, a_{i} ∈ (r_{i} + t_{i}q, s_{i} + t_{i}q), …⟩ and ⟨…, b_{i} ∈ (r_{i} + u_{i}q, s_{i} + u_{i}q), …⟩. Then there are two cases; if (∀i)(t_{i} = u_{i}), then (∀i)(a_{i} = b_{i}) and w̄ ∈ Ū, thus (∀q ∈ Q)(P_{q}w̄ ⊲_{M_{f}} Ū); if t_{i} ≠ u_{i}, then x = \frac{a_{i}−b_{i}}{u_{i}−t_{i}} ∈ M.

C6′: By inductive hypothesis we have

x ∈ M ∨ (∀q ∈ Q)(P_{q}⟨a_{i} ∈ (−1 + t_{i}q, 1 + t_{i}q)⟩w̄ ⊲_{M_{f}} Ū)

that gives, since ⟨a_{i} ∈ (−1 + t_{i}q, 1 + t_{i}q)⟩ ∈ P_{q},

x ∈ M ∨ (∀q ∈ Q)(P_{q}w̄ ⊲_{M_{f}} Ū) . □

Observe here that we do not require decidability of membership of M. In Lemma 4.6 a large part of the effort is devoted for the possibility of different values of w̄ for different proofs of w ∈ S_{L(M′)}. This problem only occurs when x ∈ M. So decidability would simplify the proof; if x ∈ M then M′ = M and there is nothing to prove, and if x ∈/ M then the formulation and the proof of Lemma 4.6 are easier.

If w is an element and U is a subset of the base of L(M), then w̄ = w and Ū = U, so as a corollary to Lemma 4.6 we obtain:

Corollary 4.7 Let w be an element, U a subset of the base of L(M), and suppose w ⊲′_{M′_{f}} U. Then x ∈ M ∨ (∀q ∈ Q)(P_{q}w ⊲_{M_{f}} U).

Proof of Proposition 4.3: Suppose w ⊲_{M′_{f}} U, where w is an element and U a subset in the base of L(M). First, by examining the axioms of the form C6 in the proof of w ⊲_{M′_{f}} U, we can find finite sequences {a_{n}} and {t_{n}} in A and in Q, respectively, such that (∀i)(a_{i} ∈ M & a_{i} + t_{i}x ∈ N(1)). Then, the proof of w ⊲_{M′_{f}} U can be converted into a proof of w ⊲′_{M′_{f}} U. By Corollary 4.7 we have x ∈ M ∨ (∀q ∈ Q)(P_{q}w ⊲_{M_{f}} U). If x ∈ M, M′ = M and there is nothing to prove. If (∀q ∈ Q)(P_{q}w ⊲_{M_{f}} U) then {P_{q} : q ∈ Q} · w ⊲_{M_{f}} U and, since ⟨ ⟩ ⊲_{M_{f}} {P_{q} : q ∈ Q} (Lemma 4.5), we obtain w ⊲_{M_{f}} U by localization and transitivity. □

We include a proof in this setting of the following application of the Helly-Hahn-Banach theorem (which is proved indirectly by Mulvey and Pelletier (1987), whereas Vermeulen (1986) gives a direct proof).

Proposition 4.8 If ⟨ ⟩ ⊲ ⟨x ∈ (−1, 1)⟩, then x ∈ N(1).

The above proposition is proved by interpreting the neighbourhoods of L([x]) as subsets of Q × Q. First we define, for r ∈ Q and I = (p, q),

r ∈ I ≡ p < r < q.

Then we put

⟨t_{1}x ∈ I_{1}, …, t_{n}x ∈ I_{n}⟩′ ≡ \{ \begin{matrix}∅ & if (∃i)(t_{i} = 0 & 0 ∉ I_{i}) \\ Q × Q & if (∀i)(t_{i} = 0 & 0 ∈ I_{i}) \\ \{⋀_{1≤i≤n,t_{i}≠0} \frac{1}{t_{i}} I_{i}\} & otherwise \end{matrix}

and let U′ be the union of all w′ such that w ∈ U.

Then we have:

Lemma 4.9 If w ⊲_{f} U in L([x]), then

(∃r ∈ Q)(x ∈ N(r) & (−r, r) · w′ ⊲_{R_{f}} U′).

Proof: The proof is by induction on the derivation of w ⊲_{f} U.

1. Let w ⊲_{f} U be derived by C1 from w ∈ U. Then, by the definition of ′, w′ ⊆ U′ so w′ ⊲_{R_{f}} U′. By N2, (∃r)(x ∈ N(r)) and for such an r, (−r, r)·w′ ⊲_{R_{f}} U′. Thus (∃r)(x ∈ N(r) & (−r, r) · w′ ⊲_{R_{f}} U′).

For 2–6 below we argue by case analysis on the way ⟨t_{1}x ∈ I_{1}, …, t_{n}x ∈ I_{n}⟩′ is constructed. The cases (∃i)(t_{i} = 0 & 0 ∉ I_{i}) and (∀i)(t_{i} = 0 & 0 ∈ I_{i}) are easy, so below we only consider the third case for which

⟨t_{1}x ∈ I_{1}, …, t_{n}x ∈ I_{n}⟩′ ≡ \{ ⋀_{1≤i≤n,t_{i}≠0} \frac{1}{t_{i}} I_{i}\} .

2. Let w_{1} ⊲_{f} U be derived by C2 from w_{1} ≤ w_{2} and w_{2} ⊲_{f} U. From the definition of ≤ and ′, w′_{1} = {I} and w′_{2} = {J}, for some I ≤ J, thus w′_{1} ⊲_{R_{f}} w′_{2}. By induction hypothesis (∃r)(x ∈ N(r) & (−r, r) · w′_{2} ⊲_{R_{f}} U′). For such an r, (−r, r) · w′_{1} ⊲_{R_{f}} (−r, r) · w′_{2} so, by transitivity, (−r, r) · w′_{1} ⊲_{R_{f}} U′. Thus the claim.

3. Suppose ⟨tx ∈ I⟩w ⊲_{f} U is derived by C3 from V finite, I ⊲_{f} V and (∀J ∈ V)(⟨tx ∈ J⟩w ⊲_{f} U). Here also we only consider the case for which w′ is a singleton set of an interval, the other cases being easy. By induction hypothesis (∀J ∈ V)(∃r)(x ∈ N(r) & (−r, r) · (⟨tx ∈ J⟩w)′ ⊲_{R_{f}} U′) and since V is finite we can take the smallest such r and obtain x ∈ N(r) & (∀J ∈ V)((−r, r) · (⟨tx ∈ J⟩w)′ ⊲_{R_{f}} U′). We assume V to be nonempty, since if V is empty, I is negative and the claim follows easily. Since (⟨tx ∈ J⟩w)′ = \frac{1}{t}I · w′, (∀K ∈ (−r, r)· \frac{1}{t}w′ ·V)(K ⊲_{R_{f}} U′). Moreover (−r, r)· \frac{1}{t}w′ ·I ⊲_{R_{f}} (−r, r)· \frac{1}{t}w′ ·V so, by transitivity, (−r, r) · \frac{1}{t}w′ · I ⊲_{R_{f}} U′. Thus the claim.

4. Suppose ⟨t_{1}x ∈ I_{1}, t_{2}x ∈ I_{2}⟩w ⊲_{f} U is derived by C4 from ⟨t_{1}x + t_{2}x ∈ I_{1} + I_{2}⟩w ⊲_{f} U. By induction hypothesis (∃r)(x ∈ N(r) & (−r, r) · (⟨t_{1}x + t_{2}x ∈ I_{1}+I_{2}⟩w)′ ⊲_{R_{f}} U′). Then we just notice that ⟨t_{1}x ∈ I_{1}, t_{2}x ∈ I_{2}⟩′ ≤ ⟨t_{1}x+t_{2}x ∈ I_{1} + I_{2}⟩′ and therefore the claim.

5. Similar to 4.

6. Suppose w ⊲_{f} U is derived by C6 from tx ∈ N(1) and ⟨tx ∈ (−1, 1)⟩w ⊲_{f} U. Again, we only consider the case in which w′ is a singleton set of an interval. By N4 and N5, x ∈ N(\frac{1}{|t|}), and by induction hypothesis,

(∃r)(x ∈ N(r) & (−r, r) · (⟨tx ∈ (−1, 1)⟩w)′ ⊲_{R_{f}} U′).

We have (⟨tx ∈ (−1, 1)⟩w)′ = \frac{1}{t}(−1, 1) · w′. If r ≤ \frac{1}{|t|} then (−r, r) ≤ (−r, r) · \frac{1}{t}(−1, 1) and therefore (−r, r)·w′ ⊲_{R_{f}} U′; if r > \frac{1}{|t|} we have \frac{1}{t}(−1, 1)·w′ ⊲_{R_{f}} U′ and the claim follows from x ∈ N(\frac{1}{|t|}). Thus (∃r)(x ∈ N(r) & (−r, r) · w′ ⊲_{R_{f}} U′). □

Proof of Proposition 4.8: Suppose ⟨ ⟩ ⊲_{L(A)} ⟨x ∈ (−1, 1)⟩. Then, by the (localic) Helly-Hahn-Banach theorem, we have ⟨ ⟩ ⊲_{L([x])} ⟨x ∈ (−1, 1)⟩ and, by definition of ⊲, ⟨ ⟩ ⊲_{L([x])_{f}} ⟨x ∈ (−1, 1)⟩. Thus, by Lemma 4.9, there exists an r ∈ Q^{+} such that x ∈ N(r) and (−r, r) ⊲_{R_{f}} (−1, 1). Therefore (cf. Cederquist and Negri 1996, Lemma 10) (−r, r) ≤ (−1, 1), that is, r ≤ 1, thus x ∈ N(1). □

The usual Hahn-Banach theorem states that the restriction mapping

\begin{matrix}P t(L(A)) & → & P t(L(M)) \\ f & ↦ & \overline{f} ≡ f ∩ S_{L(M)} \end{matrix}

is surjective.

We can obtain this result from ours plus an assumption of extensionality, up to an arbitrarily good approximation. Namely we can prove that given g in P t(L(M) and given ω ∈ g there exists f ∈ P t(L(A)) such that ω ∈ \overline{f}: By contradiction, suppose that no such f exists. Then by extensionality ω ⊲_{L(A)} ∅ and therefore, by conservativity, ω ⊲_{L(M)} ∅, that contradicts ω ∈ g.

5 Conclusion

The basic problem of the Helly-Hahn-Banach theorem can be formulated as follows. We have a normed vector space M, a linear functional u on M of norm ≤ 1, and we want to extend u to [M + x_{0}]. For this we consider two families

\{ \begin{matrix}A_{x} = u(x) − ∥x − x_{0}∥ , & x ∈ M \\ B_{y} = u(y) + ∥y − x_{0}∥ , & y ∈ M. \end{matrix}

We have A_{x} ≤ B_{y} for all x, y ∈ M and the core of the question is to find a real number r such that A_{x} ≤ r ≤ B_{y} for all x and y. Classically this is possible by taking r = sup(A_{x}). Intuitionistically, there is no reason why A_{x} should have a supremum. There are then two alternatives:

Bishop (1967); Bridges and Richman (1987): One finds instead an extension u′ of u of norm ≤ 1 + ϵ for any given ϵ > 0. For this, given ϵ > 0, we change A_{x} and B_{y} into

\{ \begin{matrix}A′_{x} = u(x) − (1 + ϵ)∥x − x_{0}∥ \\ B′_{y} = u(y) + (1 + ϵ)∥y − x_{0}∥. \end{matrix}

We still have A′_{x} ≤ B′_{y}, but the difference is that now sup(A′_{x}) exists, because A′_{x} goes to −∞ when x is big, and we can, in the finite dimensional case, restrict sup(A′_{x}) to a compact subset of M. So here we build a linear functional that extends the given one, but with norm ≤ 1 + ϵ instead of ≤ 1.

Formal topology:

One reduces the problem to a finite collection of x and y. We can then take sup A_{x}, over a finite subset of M. We never build a functional, only a finite approximation.

From this analysis, it is quite unlikely that one can easily deduce the Bishop version from the formal one, nor do we think that the proof in formal topology follows from Bishop’s formulation. On the other hand, the formal one may be as good as Bishop’s result for applications, since in an application one will only need finite approximations of a functional.

As we said, our proof can be represented in Martin-Löf’s type theory, and indeed, proof-theoretically, we use only the notion of finitary inductive definition. An interesting question at this point is the connection of our work to the work of Brown and Simpson (1986). For instance, our spaces are absolute (see Fourman and Grayson 1982) only for separable vector spaces, which explains the separability restriction, in Brown and Simpson 1986, that does not appear here.

One aim of this approach is to provide an alternative to Bishop’s treatment of functional analysis in constructive mathematics. For this, it will be important to find concrete instances of the use of the Alaoglu and Hahn-Banach theorems, for which our proof can help to extract their computational content.

Bibliography

Aczel, P. (1977). An introduction to inductive definitions, in “Handbook of Mathematical Logic”, J. Barwise ed., pp. 739–782, North-Holland, Amsterdam. Bishop, E. (1967). “Foundations of Constructive Analysis”, McGraw Hill, New York. Brezis. H. (1983). “Analyse fonctionelle – Théorie et applications”, Masson Editeur, Paris. Bridges, D. and Richman, F. (1987). “Varieties of Constructive Mathematics”, London Mathematical Society Lecture Notes Series 97, Cambridge University Press,. Brown, D.K. and Simpson, S.G. (1986). Which set existence axioms are needed to prove the separable Hahn-Banach theorem?, Annals of Pure and Applied Logic 31, pp. 123–144. Cederquist, J. (1997). A Machine Assisted Proof of the Hahn-Banach Theorem, submitted for publication. Cederquist, J. and Negri, S. (1996). A constructive proof of the Heine-Borel covering theorem for formal reals, in “Types for Proofs and Programs”, S. Berardi and M. Coppo eds., Lecture Notes in Computer Science 1158, pp. 62–75, Springer. Coquand, T. (1992). Constructive topology and combinatorics, Lecture Notes in Computer Science 613, pp. 159–164. Coquand, T. (1996). Minimal invariant spaces in formal topology, The Journal of Symbolic Logic, in press. Fourman, M.P. and Grayson, R.J. (1982). Formal spaces, in “The L. E. J. Brouwer Centenary Symposium”, A. S. Troelstra and D. van Dalen eds., pp. 107-122, North Holland, Amsterdam. Hochstad, H. (1980). Eduard Helly, Father of the Hahn-Banach theorem, Mathematical Intelligencer, vol. 2, no. 3, pp. 123–125. Martin-Löf, P. (1972). An Intuitionistic Theory of Types, University of Stockholm, Stockholm, this volume.

Mulvey, C.J. and Pelletier, J.W. (1987). The dual locale of a seminormed space, Cahiers de topologie et geometrie differentielle, vol. 23, no. 1, pp. 73–92. Mulvey, C.J. and Pelletier, J.W. (1991). A globalization of the Hahn-Banach theorem, Advances in Mathematics 89, pp. 1–60. Negri, S. (1996). Stone bases, alias the constructive content of Stone representation, in “Logic and Algebra”, A. Ursini and P. Aglianò eds., pp. 617–636, Dekker, New York. Negri, S. and Valentini, S. (1995). Tychonoff’s theorem in the framework of formal topologies, The Journal of Symbolic Logic, in press. Negri, S. and Soravia, D. (1996). The continuum as a formal space, submitted for publication. Sambin, G. (1987). Intuitionistic formal spaces – a first communication, in “Mathematical Logic and its Applications”, D. Skordev ed., pp. 187–204, Plenum Press, New York. Vermeulen, J.J.C. (1986). “Constructive Techniques in Functional Analysis”, Ph. D. Thesis, University of Sussex.