#### Supplement to Constructive Mathematics

## 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 ofNis 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 Xif for eachx ∈ Xthere exist δ > 0 and a positive integerNsuch that ρ(z,_{n}x) ≥ δ whenevern ≥ N;

eventually bounded away from the set Xif there exist δ > 0 and a positive integerNsuch that for eachx ∈ X, ρ(z,_{n}x) ≥ δ whenevern≥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:

IfZ=X∪{ω} is a one-point extension ofX, then every sequence inZthat is eventually bounded away from each point ofXis eventually bounded away fromX— that is,z= ω for all sufficiently large_{n}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 ofXinto a metric space isuniformly sequentially continuous, in the sense that for all sequences (x)_{n}_{n≥1}, (x′)_{n}_{n≥1}inX, if ρ(x,_{n}x′) → 0 as_{n}n→ ∞, then ρ(f(x),_{n}f(x′)) → 0 as_{n}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).