Inheriting the Anti-Specker Property

Douglas S. Bridges

Received: December 9, 2009 Revised: July 26, 2010

Communicated by Anil Nerode

Abstract. The antithesis of Specker’s theorem from recursive analysis is further examined from Bishop’s constructive viewpoint, with particular attention to its passage to subspaces and products. Ishihara’s principle BD-N comes into play in the discussion of products with the anti-Specker property.

2010 Mathematics Subject Classification: 03F60, 54E35, 54E45 Keywords and Phrases: constructive, anti-Specker property, BD

1 Introduction

This note is set in the framework of BISH—Bishop-style constructive mathematics. For all practical purposes this is mathematics with intuitionistic logic, an appropriate set theory (such as that described in [1, 2]), and dependent choice. We assume some familiarity with standard constructive notions such as inhabited and located; more on these, and on constructive analysis in general, can be found in [4, 10].

First, we recall that a sequence (z_{n} )_{n⩾1} in a metric space (Z, ρ) is

– eventually bounded away from the point z ∈ Z if there exist N and δ > 0 such that ρ(z, z_{n} ) > δ for all n ⩾ N;

– eventually bounded away from the subset X of Z if there exist N and δ > 0 such that ρ(x, z_{n} ) > δ for all x ∈ X and all n ⩾ N;

– eventually not in X if there exists N such that z_{n} ∉ X for all n ⩾ N.

We call a metric space Z a one-point extension of a subspace X if Z = X∪{ζ} for some ζ such that ρ (ζ, X) > 0. Note that the expression “ρ (ζ, X) > 0” is used, without any implication that the distance from ζ to X exists, as shorthand for

∃_{r} > 0∀_{x∈X} (ρ(ζ, x) > r) .

If the distance ρ(x, X) exists, we say that X is located in Z.

In an earlier paper [6], we introduced the following (unrelativised)^{1} anti-Specker property for X,

AS_{X}^{1} For some one-point extension Z of X, every sequence in Z that is eventually bounded away from each point of X is eventually not in X,

which expresses the antithesis of Specker’s famous theorem of recursion theory [14]. As is shown in [6], AS_{X}^{1} is independent of the one-point extension Z with respect to which it is stated. With classical logic, it is equivalent to the sequential compactness of X. Relative to BISH, AS_{[0,1]}^{1} is equivalent to Brouwer’s fan theorem FT_{c} for so-called “c-bars”[3]; so it is not unreasonable to regard the anti-Specker property as a serious candidate for the role of constructive substitute for the classical, and clearly nonconstructive, property of sequential compactness.

Now if AS_{X}^{1} is to be a decent substitute for a classical compactness property, we would expect it to have inheritance properties like those of the standard constructive notion of compactness (that is, completeness plus total boundedness). Thus we might hope to prove that every inhabited, closed, located subspace of a space with the anti-Specker property would have that same property; that if an inhabited subspace Y of a metric space has the anti-Specker property, then Y is closed and located; and that the product of two spaces with the anti-Specker property has that property. We address such concerns in this paper.^{2}

2 Anti-Specker for subspaces

For the proof of our first result we need a surprisingly useful result in constructive analysis, Bishop’s lemma: If Y is an inhabited, complete, located subset of a metric space X, then for each x ∈ X there exists y ∈ Y such that if ρ(x, y) > 0, then ρ(x, Y) > 0 ([4], page 92, Lemma (3.8)).

Proposition 1 Let X be a metric space with the property AS_{X}^{1}, and let Y be an inhabited, complete, located subspace of A. Then AS_{Y}^{1} holds.

1There is a more general, relativised, anti-Specker property; see [3, 6].

2Some related work is found in [6, 7, 9]. For example, Proposition 10 of [9] tells us that the anti-Specker property is preserved by pointwise continuous mappings.

Documenta Mathematica 15 (2010) 973–980

Proof. Fix a one-point extension Z ≡ X ∪ {ζ} of X; then Y ∪ {ζ} is a one-point extension of Y. Consider a sequence (w_{n} )_{n⩾1} in Y ∪ {ζ} that is eventually bounded away from each point of Y. Given x ∈ X, we show that (w_{n} )_{n⩾1} is eventually bounded away from x. By Bishop’s lemma, there exists y ∈ Y such that if ρ (x, y) > 0, then ρ(x, Y) > 0. Choose N and δ > 0 such that ρ (w_{n} , y) > δ for all n ⩾ N. Either ρ (x, y) > 0 or ρ (x, y) < δ/2. In the first case, ρ (x, Y)> 0 and therefore ρ (w_{n} , x) ⩾ ρ(x, Y) > 0 for all n. In the second case, ρ (w_{n} , x) ⩾ δ/2 for all n ⩾ N. Thus the sequence (w_{n} )_{n⩾1} is eventually bounded away from x. Since x ∈ X is arbitrary, we can apply AS_{X}^{1} to show that w_{n} = ζ for all sufficiently large n. Hence AS_{Y}^{1} holds.

We can drop the completeness hypothesis in Proposition 1 if, instead, we require Y to be proximinal in X: that is, for each x ∈ X there exists y ∈ Y (a closest point to x in Y) such that ρ (x, y) = ρ(x, Y). For in that case, with Z, ζ, and (w_{n} )_{n⩾1} as in the above proof, and given x ∈ X, we construct a closest point y to x in Y. There exist δ > 0 and N such that ρ(w_{n} , y) > δ for all n ⩾ N. Either ρ(x, y) > δ/4 or ρ(x, y) < δ/2. In the first case, ρ(w_{n} , x) ⩾ ρ(x, Y) = ρ(x, y) > δ/4 for all n; in the second case, ρ(w_{n} , x) > δ/2 for all n ⩾ N. Thus the sequence (w_{n} )_{n⩾1} is eventually bounded away from x. As before, this leads us to the conclusion that AS_{Y}^{1} holds.

Next, consider an inhabited, located subset Y of a metric space X, such that AS_{Y}^{1} holds. We cannot expect to prove that Y is closed, since the proof of [9] (Proposition 14) shows that the countably infinite, located subspace

\{0\} ∪ | \frac{1}{n} : n ⩾ 1∥

of [0, 1], whose closedness is an essentially nonconstructive proposition, has the anti-Specker property. However, we can prove that Y has a property classically equivalent to that of being closed. To do so, we need to define the complement of Y (in X):

∼Y ≡ {x ∈ X : ∀_{y∈Y} (x ≠ y)},

where “x ≠ y” means “ρ(x, y) > 0”.

Proposition 2 Let X be a metric space, and Y an inhabited, located subset of X with the property AS_{Y}^{1}. Then ∼Y is open in X.

Proof. Let Z ≡ Y ∪ {ζ} be any one-point extension of Y. Given x in ∼Y, we need only prove that ρ (x, Y) > 0; for then the open ball B(x, ρ(x, Y)) is contained in ∼Y. To that end, we may assume that ρ(x, Y) < 1/4. Construct an increasing binary sequence (λ_{n} )_{n⩾1} such that

λ_{n} = 0 } ρ (x, Y)< 2^{−n} ,
λ_{n} = 1 } ρ (x, Y)> 2^{−n−1} .

Note that λ_{1} = 0. If λ_{n} = 0, pick z_{n} ∈ Y with ρ (x, z_{n} ) < 2^{−n}; if λ_{n} = 1, set z_{n} = ζ. Given y ∈ Y, choose N such that ρ (x, y) > 2^{−N+1} . If n ⩾ N and λ_{n} = 0, then

ρ (y, z_{n} ) ⩾ ρ(x, y) − ρ(x, z_{n} ) > 2^{−N+1} − 2^{−n} ⩾ 2^{−N}.

It follows that

ρ(y, z_{n} ) ⩾ min {2^{−N} , ρ (ζ, Y)} (n ⩾ N) .

Hence the sequence (z_{n} )_{n⩾1} is eventually bounded away from each point y of Y. Using AS_{Y}^{1}, we see that z_{n} = ζ, and hence λ_{n} = 1, for all sufficiently large n. Thus there exists n such that ρ (x, Y)> 2^{−n−1} .

The foregoing proof provides a good example of how to set things up in order to apply the anti-Specker property: create a sequence in the one-point extension such that if the sequence is eventually not in the original space, then the desired property holds. Proofs of this kind can be used widely in constructive analysis in situations where the classical analyst would use sequential compactness.

3 Anti-Specker for products

So much for subspaces. We would also hope that the anti-Specker property will freely pass between a product space and each of its “factors”. The passage down from product to factors is relatively straightforward to prove.

Proposition 3 Let X ≡ X_{1} × X_{2} be the product of two inhabited metric spaces such that AS_{X}^{1} holds. Then AS_{X_{k}}^{1} holds for each k.

Proof. For each k, let Z_{k} ≡ X_{k} ∪ {ζ_{k}} be a one-point extension of X_{k}; then Z ≡ X∪{(ζ_{1}, ζ_{2})} is a one-point extension of X. Consider any sequence (y_{n} )_{n⩾1} in Z_{1} that is eventually bounded away from each point of X_{1}. Fixing ξ_{2} in X_{2}, define a sequence (z_{n} )_{n⩾1} in Z by

z_{n} ≡ \{ \begin{matrix}(y_{n} , ξ_{2}) & if y_{n} ∈ X_{1} \\ (ζ_{1}, ζ_{2}) & if y_{n} = ζ_{1}. \end{matrix}

Consider any (x_{1}, x_{2}) ∈ X. There exist N and δ > 0 such that ρ(y_{n} , x_{1}) ⩾ δ for all n ⩾ N. Hence

ρ (z_{n} , (x_{1}, x_{2})) ⩾ min {δ, ρ ((ζ_{1}, ζ_{2}), X)} > 0

for each n ⩾ N. Thus the sequence (z_{n} )_{n⩾1} is eventually bounded away from each point of X. By AS_{X}^{1}, there exists ν such that z_{n} = (ζ_{1}, ζ_{2}), and therefore y_{n} = ζ_{1}, for all n ⩾ ν. Hence AS_{X_{1}}^{1} , and similarly AS_{X_{2}}^{1} , holds.

For a converse of this proposition we recall some notions discussed in [8]. A subset S of N is said to be pseudobounded if for each sequence (s_{n} )_{n⩾1} in S, there exists N such that s_{n} < n for all n ⩾ N. Our definition of pseudoboundedness is equivalent to the original one given by Ishihara in [11]; see [13]. In [11], Ishihara introduced the following principle, which has proved of considerable significance in constructive reverse mathematics:

BD-N Every inhabited, countable, pseudobounded subset of N is bounded.

Theorem 4 BISH + BD-N ⊢ Let X, Y be inhabited metric spaces, each having the anti-Specker property. Then the product space X × Y has the anti-Specker property.

Proof. Let X ∪ {ζ_{1}} be a one-point extension of X with ρ (ζ_{1}, X) > 1, and Y ∪ {ζ_{2}} a one-point extension of Y with ρ (ζ_{2}, Y) > 1. Then Z ≡ (X × Y) ∪ {(ζ_{1}, ζ_{2})} is a one-point extension of X × Y. Let (z_{n} )_{n⩾1} be a sequence in Z that is eventually bounded away from each point of X×Y. Given x ∈ X, we aim to prove that the sequence (pr_{1}(z_{n_{k}} ))_{n⩾1} is eventually bounded away from x. Fix ξ_{2} ∈ Y. If necessary, replacing (z_{n} )_{n⩾1} by the sequence (z′_{n} )_{n⩾1} , where

z′_{n} ≡ \{ \begin{matrix}(x, ξ_{2}) & if n = 1 \\ z_{n−1} & if n > 1, \end{matrix}

we may assume that pr_{1} (z_{1}) = x. Construct a binary mapping α on N^{+} × N^{+} such that

α(n, k) = 0 } ρ (pr_{1}(z_{n} ), x) < 2^{−k} and n ⩾ k,
α(n, k) = 1 } ρ (pr_{1}(z_{n} ), x) > 2^{−k−1} or n < k.

Then α(1, 1) = 0, so the countable subset

S ≡ {j ∈ N^{+} : ∃_{n} (α(n, j) = 0) }

of N^{+} is inhabited. We prove that S is pseudobounded. To that end, let (s_{k})_{k⩾1} be any sequence in S. By countable choice, there is a mapping k ⇝ n_{k} on N^{+} such that α(n_{k}, s_{k}) = 0 for each k. Construct a binary sequence (λ_{k})_{k⩾1} such that

λ_{k} = 0 } s_{k} < k,
λ_{k} = 1 \} s_{k} > \frac{k}{2}.

Note that if λ_{k} = 1, then n_{k} ⩾ s_{k} > k/2,

ρ (pr_{1}(z_{n_{k}} ), x) < 2^{−s_{k}} < 2^{−k/2} < ρ(ζ_{1}, X) ⩽ ρ (ζ_{1}, x),

and so z_{n_{k}} ∈ X × Y. Now construct a sequence (θ_{k})_{k⩾1} in Y ∪ {ζ_{2}} as follows: if λ_{k} = 0, set θ_{k} = ζ_{2}; if λ_{k} = 1, set θ_{k} = pr_{2}(z_{n_{k}} ) ∈ Y. Given y ∈ Y, compute a positive integer N such that ρ (z_{n} , (x, y)) > 2^{−N} for all n ⩾ N. Consider any k > 2N. If λ_{k} = 0, then ρ (θ_{k}, y) ⩾ ρ(ζ_{2}, Y) > 1 ⩾ 2^{−N}. If λ_{k} = 1, then

ρ (z_{n_{k}} , (x, y)) > 2^{−N} > 2^{−s_{k}} > ρ (pr_{1}(z_{n_{k}} ), x)

and therefore

ρ(θ_{k}, y) = ρ (pr_{2}(z_{n_{k}} ), y) = ρ (z_{n_{k}} , (x, y)) > 2^{−N}.

Thus the sequence (θ_{k})_{k⩾1} is eventually bounded away from each point of Y. Since AS_{Y}^{1} holds, there exists K such that θ_{k} = ζ_{2} for all k ⩾ K. It follows that λ_{k} = 0, and therefore s_{k} < k, for all such k. This completes the proof that S is pseudobounded.

Applying BD-N, we can find J such that j < J for each j ∈ S. If n ⩾ J and ρ (pr_{1}(z_{n} ), x) < 2^{−J−1}, then α(n, J) ≠ 1, so α(n, J) = 0 and therefore J ∈ S, a contradiction. It follows that if n ⩾ J, then ρ (pr_{1}(z_{n} ), x) ⩾ 2^{−J−1}. Since x ∈ X is arbitrary, we conclude that the sequence (pr_{1}(z_{n} ))_{n⩾1} is eventually bounded away from each point of X. Applying AS_{X}^{1}, we obtain N such that pr_{1}(z_{n} ) = ζ_{1}, and therefore z_{n} = (ζ_{1}, ζ_{2}), for all n ⩾ N.

The question remains: is BD-N necessary in order to prove

(*) the product of any two spaces having the anti-Specker property also has that property.

The answer is “no”: R. Lubarsky [12] has a topological model in which (*) holds but BD-N does not. In a private communication, he has conjectured that the statement (*), which, in view of Theorem 4 and Lubarsky’s result, is weaker than BD-N, may be independent of BISH; in that case, it would be an interesting and possibly important business to find theorems of analysis that are equivalent, over BISH, to (*).

Acknowledgements. This work was supported by Marie Curie grant PIRSES-GA-2008-230822 from the European Union, with counterpart funding from the Ministry of Research, Science & Technology of New Zealand, for the project Construmath. The author is grateful to the Department of Mathematics & Statistics at the University of Canterbury, for releasing him to visit Munich under the terms of that award. He is also grateful to Helmut Schwichtenberg and his colleagues at the Mathematisches Institut der Ludwig-Maximilians-Universität München, for hosting him during his visit.

References

[1] P. Aczel and M. Rathjen, Notes on Constructive Set Theory, Report No. 40, Institut Mittag-Leffler, Royal Swedish Academy of Sciences, 2001.

[2] P. Aczel and M. Rathjen, Constructive Set Theory, monograph, forthcoming.

[3] J. Berger and D.S. Bridges, ‘A fan-theoretic equivalent of the antithesis of Specker’s theorem’, Proc. Koninklijke Nederlandse Akad. Weten. (Indag. Math., N.S.), 18(2), 195–202, 2007.

[4] E.A. Bishop and D.S. Bridges, Constructive Analysis, Grundlehren der Math. Wiss. 279, Springer-Verlag, Heidelberg, 1985.

[5] D.S. Bridges, ‘Converses of Bishop’s lemma on located sets’, Proc. Koninklijke Nederlandse Akad. Wetenschappen (Indag. Math.). 11(1), 31–38, 2000.

[6] D.S. Bridges, ‘Constructive notions of equicontinuity’, Arch. Math. Logic 48, 437–448, 2009.

[7] D.S. Bridges, ‘Omniscience, sequential compactness, and the anti-Specker property’, Logic J. of the IGPL, online 20 at doi: 10.1093/jigpal/jzq001, 2010, 2010.

[8] D.S. Bridges, ‘Limited omniscience, anti-Specker properties, and the uniform continuity theorem’, preprint, Ludwig-Maximilians-Universität München, 2009.

[9] D.S. Bridges and H. Diener, ‘The anti-Specker property, positivity, and total boundedness’, Math. Logic Quart. 56(4), 434–441, 2010.

[10] D.S. Bridges and L.S. Vîţă, Techniques of Constructive Analysis, Universitext, Springer New York, 2006.

[11] H. Ishihara, ‘Continuity properties in constructive mathematics’, J. Symb. Logic 57(2), 557–565, 1992.

[12] R. Lubarsky, ‘On the failure of BD-ℕ’, preprint, Florida Atlantic University, Boca Raton, 2010.

[13] F. Richman, ‘Intuitionistic notions of boundedness in N’, Math. Logic Quart. 55(1), 31–36, 2009.

[14] E. Specker, ‘Nicht konstruktiv beweisbare Sätze der Analysis’, J. Symb. Logic 14, 145–158, 1949.

Douglas S. Bridges Department of Mathematics & Statistics University of Canterbury Private Bag 4800 Christchurch 8140 New Zealand dugbridges@zoho.com