Ishihara's principle BD-N and the anti-Specker Property

Ishihara's principle BD-N

We now consider another principle of great significance for constructive reverse mathematics. Following Ishihara (1992), we say that an inhabited subset S of the set N of natural numbers is pseudobounded if for each sequence (s_n)_n≥1 in S, s/n → ∞ as n → ∞. This brings us to Ishihara's principle (BD-N):

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

This principle has the unusual property of being derivable in all three main interpretations—CLASS, INT, RUSS—of BISH but not in BISH alone: Lietz has shown that BD-N fails in various realizability models of extensional Martin-Löf type theory; see Lietz 2004 and Lietz & Streicher 2011.

Ishihara (1992, Theorem 4) has shown that BD-N is equivalent, over BISH, to each of the statements:

Every sequentially continuous mapping of a complete, separable metric space into a metric space is pointwise continuous;
Every sequentially continuous mapping of a separable metric space into a metric space is pointwise continuous.

He and other authors have subsequently proved that BD-N is a necessary and sufficient addition to BISH to ensure the derivability of a number of results allowing us to pass from sequential to pointwise properties. One important example occurs with Banach's inverse mapping theorem from functional analysis. The classical theorem states that the inverse of an injective bounded linear mapping between Banach spaces is continuous; but Ishihara (1994), working with separable spaces, has shown that the best possible conclusion in BISH is the sequential continuity of the inverse map, and that to pass from that to full continuity, it is necessary and sufficient to work in BISH + BD-N.

The anti-Specker Property

Is there any viable constructive substitute for the classical property of sequential compactness? This question might seem frivolous, since the sequential compactness of the two-point space {0,1} is equivalent, constructively, to LPO. However, and perhaps to the reader's surprise, there is a notion that is both constructively useful and classically equivalent to sequential compactness. In order to discuss it, we need some definitions, and a little motivation from RUSS.

Let z = (z_n)_n≥1 be a sequence in a metric space (Z, ρ), and X a subset of A. We say that z is

eventually bounded away from each point of X if for each x ∈ X there exist δ > 0 and a positive integer N such that ρ(z_n, x) ≥ δ whenever n ≥ N;

eventually bounded away from the set X if there exist δ > 0 and a positive integer N such that for each x ∈ X, ρ(z_n, x) ≥ δ whenever n ≥ N.

We recall, from earlier in this article, the strong recursive counterexample to the sequential compactness of [0,1], Specker's theorem (Specker 1949) in RUSS: there exists a (Specker) sequence z in [0,1] that is eventually bounded away from each point of [0,1]. What would it take to rule such a counterexample out of our constructive mathematics?

By a one-point extension of a metric space X we mean a metric space of the form Z∪{ω} on which the metric ρ restricted to X, is the original one, and ρ(ω, X) > 0. Here we are adopting the convention that ρ(ω, X) > 0 is shorthand for

∃r > 0 ∀x ∈ X (ρ(ω, x) ≥ r}.

To avoid Specker sequences, we can introduce the following anti-Specker property, AS_X, for X:

If Z = X∪{ω} is a one-point extension of X, then every sequence in Z that is eventually bounded away from each point of X is eventually bounded away from X — that is, z_n = ω for all sufficiently large n.

This property is independent of the particular one-point extension of X: if it holds for one such extension, it holds for them all.

The anti-Specker property is classically equivalent to the sequential compactness of X. It allows us to pass from a pointwise property—being eventually bounded away from each point of the set—to a uniform one — being eventually bounded away from the set itself. One might therefore expect it to be connected with some version of the fan theorem. This is indeed the case: the anti-Specker property for [0,1] is equivalent, over BISH, to the fan theorem FT_c for c-bars (Berger and Bridges 2006). It should therefore be no surprise that, when added to BISH, anti-Specker properties enable us to pass from pointwise to uniform properties in a number of instances. To illustrate, we sketch the proof of the following result:

BISH + AS_X   ⊢    Every pointwise continuous mapping of X into a metric space is uniformly sequentially continuous, in the sense that for all sequences (x_n)_n≥1, (x′_n)_n≥1 in X, if ρ(x_n, x′_n) → 0 as n → ∞, then ρ(f(x_n), f(x′_n)) → 0 as n → ∞.

Let Z ≡ X∪{ω} be a one-point extension of X, and consider sequences (x_n)_n≥1, (x′_n)_n≥1 in X such that ρ(x_n, x′_n)→∞ as n→∞. Given ε > 0, construct a binary sequence (λ_n)_n≥1 such that

λ_n  =  0  ⇒ ρ(f(x_n), f(x′_n))  <  ε,

λ_n  =  1  ⇒ ρ(f(x_n), f(x′_n))  >  ε/2.

If λ_n =  0, set z_n  =  ω; if λ_n  =  1, set z_n  = x_n . Using the sequential continuity of f (we omit the details), we can show that the sequence (z_n)_n≥1 is eventually bounded away from each point of X. Hence, by the anti-Specker property of X, it is eventually bounded away from the set X. It follows that λ_n  =  0, and hence that ρ(f(x_n), f(x′_n))  <  ε, for all sufficiently large values of n. Since ε is an arbitrary positive number, the proof is complete.

In our present state of knowledge, we can say that the proof-theoretic strength of AS_[0,1] lies between that of the uniform continuity theorem (a consequence of FT_Π01) and FT_D. Diener (2012) has shown that AS_[0,1] is equivalent to every compact metric space having the anti-Specker property, and that a more general form of anti-Specker property, in which one-point extensions are replaced by arbitrary supersets, is equivalent to FT_Π01). Further interconnections between anti-Specker properties, fan theorems, and other principles of constructive mathematics have been studied in detail by Dent (forthcoming); see also Diener 2008 (Chapter 4).