On the Failure of BD-ℕ and BD, and an Application to the Anti-Specker Property

Robert S. Lubarsky Dept. of Mathematical Sciences Florida Atlantic University Boca Raton, FL 33431 Robert.Lubarsky@alum.mit.edu

June 27, 2010

Abstract

We give the natural topological model for ¬BD-ℕ, and use it to show that the closure of spaces with the anti-Specker property under product does not imply BD-ℕ. Also, the natural topological model for ¬BD is presented. Finally, for some of the realizability models known indirectly to falsify BD-ℕ, it is brought out in detail how BD-ℕ fails. keywords: anti-Specker, BD, BD-ℕ, realizability, topological models AMS 2010 MSC: 03F60, 26E40

1 Introduction

In recent years much attention has been paid to subtle foundational principles of constructive analysis. (For background in constructive analysis, see [7, 8].) These are principles that hold in the major traditions of mathematics, such as Brouwer’s intuitionism, Russian constructivism, and classical mathematics, yet do not follow from ZF-style axioms on the basis of constructive logic, such as IZF. The principles of this character identified so far are Weak Markov’s Principle [13, 16, 28], a version of Baire’s Theorem [19], and, most importantly for our purposes, the boundedness principles BD and BD-ℕ ^{1}.

1At the conference “Constructive Mathematics,” held on the Fraueninsel in the Chiemsee, Germany, June 7-11, 2010, I advocated replacing the names “BD” and “BD-ℕ” with initials of a descriptive name for these prinicples. For instance, if we were to call the former the Boundedness Principle, then the abbreviation would be BP, current environmental difficulties notwithstanding. Perhaps a better name would be the Pseudo-boundedness Principle, leading to the abbreviations PP or PBP, which with some practice isn’t that hard to say. This suggestion was met with some compassion, and also some scepticism that it just might be too late to change. I do not have the courage to enter into this battle now, nor do I want the current work to be ununderstandable in the future in case this battle is lost. So for the moment I retain the current names, and remain interested in seeing if the community eventually decides that it might be worthwhile to use others instead.

By way of explaining these boundedness principles, a sequence (a_{n}) of natural numbers is pseudo-bounded if lim_{n→∞} a_{n}/n = 0. A set of natural numbers is pseudo-bounded if every sequence of its members is pseudo-bounded. Examples are bounded sets. Equivalently, as observed in [19], a set is pseudobounded if every sequence (a_{n}) of its members is eventually bounded by the identity function: for n large enough, a_{n} < n (or a_{n} ≤ n). (To see this equivalence, consider large enough intervals within (a_{n}).) This latter formulation is often easier to work with.

BD is the assertion that every pseudo-bounded set of natural numbers is bounded. BD-ℕ is that every countable pseudo-bounded set of naturals is bounded. They were first identified during Ishihara’s analysis of continuity [17], as they are equivalent to sequentially continuity functions on certain metric spaces being ϵ − δ continuous. Since their identification, they have become central tools in the foundations of constructive analysis, especially the latter [9, 10, 12, 18, 20].

It can be hard to imagine how BD or BD-ℕ could fail, which is likely a cause or effect of their being true in most systems. That notwithstanding, in order to understand them better, it is useful to see when they are false. Trivially BD implies BD-ℕ, so when discussing their failure we will usually restrict attention to the weaker of the two, the one more difficult to falsify, BD-ℕ. It turns out that the first models falsifying it did so unwittingly. BD-ℕ is new, and continuity is old. So models violating commonly accepted continuity principles were developed long before BD-ℕ was even identified. It was only later that people looked backed and realized that the only way that those continuity properties could fail was through the failure of BD-ℕ.

There are several shortcomings to this state of affairs, which the current work is intended to address. One is that these first models seem somewhat ad hoc for this purpose, falsifying BD-ℕ almost by accident. In contrast, the topological models presented here seem to be the natural models. (For discussion about naturality, see also the questions at the end. For background on topological models, see [14, 15].) That is, to violate BD-ℕ, you’d need a sequence which is sort-of bounded while also sort-of unbounded. Without thinking much about it, you might well guess that either a generic bounded sequence or a generic unbounded sequence would do the trick. This turns out to be exactly right, as we will see. Similarly, to violate BD, you’d need a set which is simultaneously bounded and unbounded, after a fashion. The first guess is again a generic set, either bounded or unbounded; again, this does it.

A second shortcoming of the prior state of knowledge is that the way we know BD-ℕ to fail in these first models is indirect: BD-ℕ plus other foundational axioms imply some continuity principle; said continuity principle fails; check that the other axioms hold; hence BD-ℕ fails. We are left with the unsatisfying feeling of not really knowing just why BD-ℕ fails. What is the pseudo-bounded sequence which is not bounded? Or is there something else going on? This is also addressed later, when for some of these models the indirect argument above is unraveled to reveal just how BD-ℕ fails.

Finally, the first proofs of models violating BD-ℕ was in Lietz’s thesis [22], which also contains the bulk of the known models. Although these models are all ultimately realizability models, the presentation is category-theoretic through and through, and so difficult or even inaccessible for non-category theorists to understand. The presentation of these models given here is purely in terms of realizability for arithmetic and analysis.

Returning to the alleged naturality of the topological models, a good test for naturality is whether the model, while violating BD or BD-ℕ, violates as little else as possible. That is, it should prove independence results around BD or BD-ℕ. For instance, Doug Bridges [11] has shown that, under BD-ℕ, anti-Specker spaces (see below) are closed under products, and asked whether the converse holds. If there is a canonical model falsifying BD-ℕ, that would be the first place to look for this question. Such a model is the gentlest possible extension of a classical model making BD-ℕ false. If the failure of BD-ℕ did not imply that anti-Specker spaces are so closed, then in the canonical model the anti-Specker spaces would retain this closure. This is in fact just what is shown in section 3, that in the first model of section 2 the anti-Specker spaces are closed under Cartesian product. Hence such closure does not imply BD-ℕ.

We hope that the models presented here will make investigations around BD and BD-ℕ easier, as well as promote interest in topological models more generally.

2 Topological models

As discussed above, we are looking for a sequence (or, in the case of BD, set) which is kinda bounded yet also kinda unbounded. The obvious guess is to take either a generic bounded or a generic unbounded sequence. That is, the topological space would be the space of bounded sequences, or unbounded sequences. The topological model over a space introduces a generic elements of that space, so in this case we’d have a generic bounded, or unbounded, sequence. Not surprisingly, this works for both BD-ℕ and BD.

2.1 The natural model for ¬BD-ℕ

Let the points in the topological space T be the functions f from ω to ω with finite range, that is, enumerations of finite sets. A basic open set p is (either ∅ or) given by an unbounded sequence g_{p} of integers, with a designated integer stem(p), beyond which g_{p} is non-decreasing. f ∈ p if f(n) = g_{p}(n) for n < stem(p) and f(n) ≤ g_{p}(n) otherwise. Notice that p ∩ q is either empty (if the stems are incompatible) or is given by taking the longer of the two stems and the pointwise minimum beyond that. Hence these open sets do form a basis.

It is sometimes easier to assume that g_{p}(stemp) ≥ max{g_{p}(i) | i < stem(p)}. The intuition is that once a certain value has been achieved there’s nothing to be gained anymore by trying to restrict future terms from being that big. In fact, that additional restriction would not change the topology, as follows. Let n ≥ stem(p) be the least integer such that g_{p}(n) ≥ max{g_{p}(i) | i < stem(p)}.

Let q be such that stem(q) = n, g_{q} ↾ stem(p) = g_{p} ↾ stem(p), for stem(p) ≤ i < n g_{q}(i) ≤ g_{p}(i) (so q ⊆ p), and otherwise g_{q}(i) = g_{p}(i). By the choice of n, q is of this more restrictive form, and p is the union of all such q’s. So whenever more convenient, a basic open set can be taken to be of this more restrictive form.

Let M be the full topological space built over T. (For background on topological models, see [14, 15]. What is there called the topological model is here described as the full model, to distinguish it from other possible models. The fullness consists of it containing all possible terms.) Let G be the canonical generic: p ⊩ G(n) = x iff n < stem(p) and g_{p}(n) = x. The primary result of this note is

Theorem 2.1 T ⊩ rng(G) is countable and pseudo-bounded, yet not bounded. Also, T ⊩ DC.

A major reason we’re interested in showing that the model validates DC is that it makes the failure of BD-ℕ that much more striking. One might consider arguing for BD-ℕ by, given f : ℕ → ℕ, trying to build a sequence with a_{0} = f(0) and a_{n+1} = min{x | x ∈ rng(f), x > a_{n}}; if this construction succeeds, then f is not pseudo-bounded, and if it doesn’t then f looks to be bounded. This will not work, if for no other reason than that minimum might not exist. With DC, that last objection loses its validity: as long as {x | x ∈ rng(f), x > a_{n}} is inhabited, a value could be chosen for a_{n+1}, and with DC these values could be strung together into a total sequence. Hence DC makes it even harder for BD-ℕ to fail. Another reason to want DC is that it is useful for developing analysis. So this model then provides a nice testing ground or example for the development of analysis in the absence of BD-ℕ.

Proof: It is immediate that rng(G) is countable, as G is total: given n, {p | stem(g_{p}) > n} covers T, and each such p forces n ∈ dom(G). It is almost as immediate that rng(G) is not bounded: given a potential bound B ∈ ℕ, since g_{p} is unbounded, p can be extended to an open set forcing B ∈ rng(G); hence no p can force that any particular natural is a bound, i.e. nothing forces that rng(G) is bounded, so T forces that rng(G) is unbounded.

The work is in showing pseudo-boundedness. The primary lemma for that is:

Lemma 2.2 Let p be an open set forcing “t ∈ rng(G)”, and I an integer such that max_{n<stem(p)} g_{p}(n) ≤ I ≤ g_{p}(stem(p)). Then there is a q extending p with the same stem and g_{q}(stem(q)) ≥ I forcing “t ≤ I”.

Proof: If r is an open set, for i ≤ g_{r}(stem(r)), let r_{i} ⊆ r be such that stem(r_{i}) = stem(r)+1, g_{r_{i}}(stem(r)) = i, and for n ≠ stem(r), g_{r_{i}}(n) = g_{r}(n). Notice that ⋃_{i} r_{i} = r.

Fix I. Say that p′ ⊆ p is a \underline{candidate} if max_{n<stem(p′)} g_{p′}(n) ≤ I ≤ g_{p′}(stem(p′)). If p′ is a candidate, say that q′ ⊆ p′ is \underline{good} if q′ satisfies the conclusion of the lemma as applied to p′. We want to show that p itself has a good extension. Notice that if i ≤ I and p′ is a candidate, so is p′_{i}.

Suppose that each p_{i} (i ≤ I) had a good extension, say q^{i}. Then so would p, as follows. Let stem(q) = stem(p). For n < stem(q), let g_{q}(n) be the common value g_{p}(n); let g_{q}(stem(q)) be I; for all other n, let g_{q}(n) be min_{i} g_{q^{i}}(n). As described above, q is covered by the q_{i}s, and each q_{i} is a subset of q^{i}, so q ⊩ “t ≤ I”.

This means that if p^{0} := p does not have a good extension, neither does some p^{1} := p_{i}. Continuing inductively, let p^{n+1} be p_{i}^{n}, where i ≤ I and p_{i}^{n} does not have a good extension. The initial parts of the p^{n}s cohere to form a function f ∈ p with range (a subset of) {0, 1, ... , I}. Let r ⊆ p be a neighborhood of f forcing a particular value J for t. J ≤ I, as follows. Since t is forced to be in the range of G, extend r to a neighborhood s of f forcing t = G(m) for some natural number m. Without loss of generality, stem(s) can be taken to be larger than m. By the choice of f, G(m) ≤ I, as claimed.

Eventually the values of g_{s} are all ≥ I, so, if need be, shrink s by extending the initial part consistently with f until g_{s}(stem(s)) ≥ I. This is a good extension of some p^{n}, which is a contradiction.

In the end, we will need a more general version of the preceding.

Lemma 2.3 Let p be an open set forcing “t ∈ rng(G)”, and M ≥ stem(p), I an integer such that max_{n<M} g_{p}(n) ≤ I ≤ g_{p}(M). Then there is a q extending p such that for n < M g_{q}(n) = g_{p}(n), stem(q) = stem(p), and g_{q}(M) ≥ I, forcing “t ≤ I”.

Notice that the previous lemma is the special case of the current one in which M = stem(p).

Proof: Using the notation from the beginning of the last proof, {p_{i} | i ≤ g_{p}(stem(p))} is an open cover over p. Similarly, {(p_{i})_{j} | j ≤ g_{p}(stem(p) + 1)} is an open cover of p_{i}, so that the collection of (p_{i})_{j}s as both i and j vary is an open cover of p. Continuing this procedure for M − stem(p) many steps, we have an open cover q_{k} (k < K) of p such that stem(q_{k}) = M. Applying the previous lemma to each q_{k} produces a collection q′_{k} such that each one forces “t ≤ I”. The union ⋃_{k} q′_{k} can be restricted to a basic open set q as follows: stem(q) = stem(p), g_{q}(n) = g_{p}(n) for n < M, and for larger n g_{q}(n) = min_{k}(q′_{k}(n)). q is as desired.

The benefit of this lemma is that it enable one to do fusion arguments, like in Axiom A forcing [1] and in arguments to get minimal degrees in computability theory, to get the pseudo-boundedness of G, as well as DC.

Lemma 2.4 T ⊩ rng(G) is pseudo-bounded.

Proof: Suppose p ⊩ a_{n} is a countable sequence through rng(G). We need to show that p forces that a_{n} is eventually bounded beneath n. That means that p forces the existence of an index N beyond which a_{n} is forced to be less than n. Since forcing existence is local, for any f ∈ p we need to find a neighborhood r of f forcing the adequancy of a particular index N.

Fix f ∈ p. Let N be sup(rng(f)). Let M be the smallest natural such that g_{p}(M) > N. Notice that, since f ∈ p, M ≥ stem(p). Apply the previous lemma to t := a_{N} to extend p to q_{N}. (Notice that f ∈ q_{N}, since g_{p} and g_{q_{N}} agree up to M, and beyond that g_{q_{N}} (n) always bounds rng(f).)

Now apply the previous lemma to p := q_{N}, t := a_{N+1}, I := N + 1, and M the least index n such that g_{q_{N}} (n) ≥ N + 1. This produces a basic open set q_{N+1} containing f forcing a_{N+1} ≤ N + 1.

Again, apply the previous lemma to p := q_{N+1}, t := a_{N+2}, I := N + 2, and M the least index n such that g_{q_{N+1}}(n) ≥ N + 2. This produces a basic open set q_{N+2} containing f forcing a_{N+2} ≤ N + 2.

By continuing this process for ever increasing values of I, the function which is the pointwise limit of g_{q_{N+i}} is unbounded, and so (together with stem(p)) determines an open set ⋂_{n} q_{n} containing f that by construction forces each a_{n} (n ≥ N) to be bounded by n.

In order to prove DC, we need appropriate analogues of the two lemmas from above.

Lemma 2.5 Let p be an open set forcing “∃y ψ(y)”, and I an integer such that I ≤ g_{p}(stem(p)). Then there is a q extending p with the same stem and g_{q}(stem(q)) ≥ I forcing ψ(σ) for some term σ.

Proof: This argument is similar to that of the first lemma above. We need the same notation: p_{i}, for i ≤ g_{p}(stem(p)), is (to put it informally) the same as p only the value at the stem(p)^{th} place is fixed to be i. If each p_{i} has a good extension q^{i}, meaning one satisfying the conclusion of the lemma (when starting from p_{i}), then so does p, as follows. Let q be such that stem(q) = stem(p), for n < stem(q) g_{q}(n) is the common value g_{p}(n), g_{q}(stem(q)) is I, and for all other n g_{q}(n) is min_{i} g_{q^{i}}(n). q is covered by the q_{i}s, each q_{i} is a subset of q^{i}, and each q^{i} forces ψ(σ_{i}). The σ_{i}s can be amalgamated as follows. Recall that a term τ is a set of the form {⟨τ_{j}, r_{j}⟩ | j ∈ J}, where τ_{j} is (inductively) a term, r_{j} an open set, and J an index set. The restriction of τ to some open set r, τ ↾ r, is defined as {⟨τ_{j}, r_{j} ∩ r⟩ | j ∈ J}. Intuitively, τ ↾ r is empty until you’re beneath r, at which point it becomes τ. The amalgamation we want is σ := ⋃_{i} σ_{i} ↾ q^{i}, which roughly stands for “wait until you know which q^{i} you’re in, then become σ_{i}”. This σ witnesses that q is a good extension of p.

So if p^{0} := p did not have a good extension, neither would some p^{1} := p_{i}, nor some p^{2} := p_{j}^{1}, etc. The p^{n}s cohere, or converge, to some f ∈ p. By hypothesis, f has some neighborhood r forcing ψ(σ) for some σ. If need be, shrink r (to r′ say) consistently with f so that g_{r′}(stem(r′)) ≥ I. This r′ is a good extension of some p^{n}, which is a contradiction.

Lemma 2.6 Let p be an open set forcing “∃y ψ(y)”, and M ≥ stem(p), I an integer such that I ≤ g_{p}(M). Then there is a q extending p such that for n < M g_{q}(n) = g_{p}(n), stem(q) = stem(p), and g_{q}(M) ≥ I, forcing ψ(σ) for some term σ.

The proof of this lemma is to the previous proof as the proof of the lemma before that is to the one before it, and so is left to the reader.

Lemma 2.7 T ⊩ DC.

Proof: Suppose p ⊩ “∀x ∃y ϕ(x, y)”. (The argument is unchanged if x and y are restricted to some set.) Let a_{0} be given. Using the previous lemma, at stage 0, extend p to p_{0}, with the same stem and the same value I at stem(p), forcing ϕ(a_{0}, a_{1}) for some a_{1}. At stage 1, let N_{1} be the least index n such that g_{p_{0}}(n) > I, and extend p_{0} to p_{1}, with the same stem and same values at all indices n ≤ N_{1}, forcing ϕ(a_{1}, a_{2}) for some a_{2}. Continue inductively, at stage n preserving some occurrence of an integer at least as large as I+n as a function value, so that ⋂_{n} p_{n} is an open set. By construction, ⋂_{n} p_{n} ⊩ ∀n ∈ ℕ ϕ(a_{n}, a_{n+1}).

This sequence of lemmas completes the proof of the main theorem.

2.2 The natural model for ¬BD

BD is the assertion that every pseudo-bounded set of natural numbers is bounded: BD-ℕ without the assumption of countability. So BD implies BD-ℕ, and the model above falsifying BD-ℕ must also falsify BD. We can do better than that though. The generic above was not bounded: it is false that there exists a bound. That’s different from being unbounded: ∀N∃i ∈ A i > N. There are two good reasons that G above was not unbounded. For one, since G is countable, if it were unbounded it would not be pseudo-bounded. (Let a_{0} be G(0); given a_{n} = G(m), let a_{n+1} be G(k), where k is the least integer greater than m such that G(k) > G(m), which exists by unboundedness. Then (a_{n}) would witness that G is not pseudo-bounded.) For another, even if G were not countable, DC is enough to take an unbounded set and return a witness to nonpseudo-boundedness. So we would like to find a counter-example to BD which is unbounded.

More than that, we would like to find a counter-example to a weakened version of BD. This is based on the following:

Definition 2.8 A ⊆ ℕ is sequentially bounded if every sequence of members of A is bounded.

Notice that if A is sequentially bounded then A is pseudo-bounded. The converse does not hold, as G from the previous theorem illustrates. So the assertion “if A is sequentially bounded then A is bounded” differs from BD in that it has a stronger hypothesis, and so is a weaker assertion. Weaker assertions are harder to falsify. Hence the goal is to produce a sequentially bounded, unbounded set. Can this be done?

The answer is a very satisfying yes, satisfying because it so well complements the previous construction. Recall that it was argued that the best guess for the last section’s counter-example was to take a generic over either the bounded or the unbounded sequences. It turned out that the bounded sequences did the trick. The best guess here would be a generic over either the bounded or unbounded sets. It turns out that the choice this time is the other one: the unbounded sets.

So let T be the space of all unbounded sets X of natural numbers. A basic open set O is given by a pair ⟨P_{O}, N_{O}⟩, so called because P_{O} is a finite set of naturals giving the positive information and N_{O} a set of naturals giving the negative information. X ∈ O iff P_{O} ⊆ X and N_{O} ∩ X is finite. (Hence for the second component we could have taken instead an equivalence class from the power set of ℕ mod the ideal of finite sets.) For O and U open, O ∩ U is given by ⟨P_{O} ∪ P_{U}, N_{O} ∪ N_{U}⟩, so the opens given do form a basis. Notice that O = ∅ iff N_{O} is cofinite.

Let M be the full topological model over T, and G the canonical generic: O ⊩ n ∈ G iff n ∈ P_{O}. Notice that nothing can ever be forced out of G.

Theorem 2.9 T ⊩ G is unbounded and sequentially bounded.

Proof: It is easy to see that T ⊩ G is unbounded. Let X ∈ T, and n ∈ ℕ. Choose j > n, j ∈ X. Let O be given by ⟨{j}, ∅⟩. Then X ∈ O ⊩ j ∈ G. So T is covered by open sets forcing “∃i > n i ∈ G”, hence T forces the same. Since n was arbitrary, T ⊩ “∀n ∃i > n i ∈ G.”

As for sequential boundedness, let O ⊩ “a_{n} is a sequence through G”. We can assume that O is basic and non-empty. We will need the following fact about the topology: if P′_{O} is a finite extension of P_{O}, then the open set O′ determined by ⟨P′_{O}, N_{O}⟩ is compatible with (i.e. is not disjoint from) every open subset of O. Namely, for V ⊆ O basic open, P_{V} ∪ (ℕ − N_{V}) ∈ V; since V ⊆ O, P_{V} ∪ (ℕ − N_{V}) ∈ O; that means (P_{V} ∪ (ℕ − N_{V})) ∩ N_{O} is finite; hence P′_{O} ∪ P_{V} ∪ (ℕ − N_{V}) ∈ O′ ∩ V.

Returning to the main argument, let X_{O} ∈ O be ℕ − N_{O}. For each n, some basic open neighborhood U of X_{O} determines the values of a_{n}. U is given by ⟨P_{U}, N_{U}⟩, where P_{U} is a finite subset of X_{O}, and, crucially, N_{U} differs from N_{O} on a finite set, because U is taken to include X_{O}. Since an open set is unchanged by a finite change to the second component, we can take N_{U} to be N_{O}. By the observation above, any other non-empty basic open subset of O is compatible with U. So any other value of a_{n} that could be forced by a subset of O has to be compatible with the one forced by U. So O is covered by opens all forcing the same value of a_{n}, hence O forces a_{n} to have that value. Since O also forces “a_{n} ∈ G”, and the only numbers O forces to be in G are those in P_{O}, O ⊩ a_{n} ∈ P_{O}. Since n was arbitrary, O forces (a_{n}) to be bounded.

3 Application: Anti-Specker

Doug Bridges has shown [11] that BD-ℕ implies that the spaces that satisfy a version of the anti-Specker property are closed under products. He asked whether the reverse implication is true. Here we show it is not, by showing that in the model of the previous section the anti-Specker spaces are closed under products.

A metric space X satisfies the one-point anti-Specker property (notation: AS^{1}(X)) if, for every one-point extension Z = X ∪ {∗} of X and sequence (z_{n})(n ∈ ℕ) through Z, if (z_{n}) is eventually bounded away from each point in X, then (z_{n}) is eventually bounded away from X. (The name refers to Specker’s Theorem, which is that in computable mathematics the closed interval [0,1] does not have this property [13, 26].) Other variants of anti-Specker include AS(X): every sequence (z_{n}) through any metric space Z ⊇ X eventually bounded away from each point in X is eventually bounded away from X. Z can also be held fixed (notation: AS(X)_{Z}). It is known, for instance, that AS^{1}([0, 1]) iff AS([0, 1])_{ℝ} [9]. For more background on the anti-Specker properties, see [5, 6, 9, 10, 11].

The purpose of this section is achieved with this

Theorem 3.1 T ⊩ AS^{1}(X) ∧ AS^{1}(Y) → AS^{1}(X × Y).

Proof: Let p ⊩ “AS^{1}(X) ∧ AS^{1}(Y) ∧ (z_{n}) is a sequence through X × Y ∪ {∗} eventually bounded away from each (x, y) ∈ X × Y, ” and f ∈ p. We must find a neighborhood of f forcing “(z_{n}) is eventually ∗.”

By way of notation, let x_{n} and y_{n} be terms such that p ⊩ “If z_{n} ∈ X × Y then z_{n} = (x_{n}, y_{n}), and if z_{n} = ∗ then x_{n} = ∗ = y_{n}.” Let I = sup(rng(f)). Without loss of generality, p is basic open, with g_{p}(stem(p)) ≥ I.

Definition 3.2 A finite sequence of integers σ of length at least stem(p) is compatible with p if for all i < stem(p) σ(i) = g_{p}(i) and for all i with stem(p) ≤ i < length(σ) σ(i) ≤ g_{p}(i). For σ compatible with p, p ↾ σ is the open set q ⊆ p such that stem(q) = length(σ), for i < stem(q) g_{q}(i) = σ(i), and otherwise g_{q}(i) = g_{p}(i).

Lemma 3.3 There is an open set q such that f ∈ q ⊆ p, stem(q) = stem(p), and for n ∈ ℕ there is a length i_{n} such that, for all σ of length i_{n} compatible with q, either q ↾ σ ⊩ “x_{n} (equivalently y_{n}) = ∗” or q ↾ σ ⊩ “x_{n} (equivalently y_{n}) ≠ ∗.”

Proof: Let n ∈ ℕ. First we prove a generalization of this lemma for this fixed n. So let j ≥ stem(p), J ≥ I with J ≤ g_{p}(j), and σ be a sequence of length j compatible with p. We claim that there is an open set q extending p such that stem(q) = j, g_{q} ↾ j = σ, and g_{q}(j) = J, and there is an i ≥ j such that, for all σ of length i compatible with q, q ↾ σ decides whether x_{n} (equiv. y_{n}) is ∗ or not.

The proof of that claim is similar to that of the lemmas of the previous section. For notational convenience, extend p if necessary so that j = stem(p). So the claim is that we can build the desired q only by shrinking g_{p} beyond stem(p), and even that by not too much (at stem(p), we must still be at least J).

Using the notation from the last section, if for each j ≤ J p_{j} had such a good extension q_{j} with associated integer i_{j}, then they could be amalgamated to a good extension of p, with the amalgamation of the i_{j}’s being their maximum. So if p had no good extension, then neither would some direct extension p^{1} := p_{j} of p. Similarly, p^{1} would itself have some direct extension p^{2} with no good extension. Continuing countably often, the sequence of p^{N}’s determines an h ∈ p. Some neighborhood r of h must determine whether x_{n} is ∗ or not, which can be restricted to a good extension of some p^{N}. This contradicts the choice of p^{N}, so p must have a good extension.

Now apply the claim with n = 0, j = stem(p), and J = I, which determines σ, to produce q_{0} and i_{0}. Let n = 1, j ≥ i_{0} such that g_{q_{0}}(j) ≥ I + 1, and J = I + 1. For each σ of length j compatible with q_{0} and with range bounded by I, use the claim to construct a q_{σ} and an i_{σ}. There are only finitely many such σ’s, so the q_{σ}’s can be amalgamated via intersection to q_{1} and the i_{σ}’s via their maximum to i_{1}. More generally, at stage k > 0, let n = k, j ≥ i_{k−1} such that g_{q_{k−1}}(j) ≥ I + k, and J = I + k. Use the claim to construct the q_{σ}’s and i_{σ}’s, which are then amalgamated to q_{k} and i_{k}.

Since the choice of J is unbounded as k runs through the natural numbers, q := ⋂_{k∈ℕ} q_{k} is an open set, and has the properties claimed.

Let q be as in the lemma. The members of q naturally form a tree T r_{q}: the nodes are those finite sequences compatible with q, and the members of q are those paths through the tree with bounded range. At height j ≥ stem(q) of T r_{q}, the amount of splitting is g_{q}(j) + 1. The nodes at height i_{n} determine whether x_{n} and y_{n} are ∗ or not. We will have use for subsets of q the members of which have ranges that are uniformly bounded. (Such subsets are, of course, not open.) Such subsets can be given as the set of paths through a subtree T r of T r_{q} with a fixed bound on the ranges of its nodes, as follows.

Definition 3.4 A tree T r ⊆ T r_{q} is bounded if there is a J such that for all σ ∈ T r and j < length(σ) σ(j) < J.

Lemma 3.5 Let T r ⊆ T r_{q} be bounded. Then {σ ∈ T r | length(σ) = i_{n} and q ↾ σ ⊩ “x_{n} ≠ ∗”} is finite.

Proof: Suppose not. Since T r (even T r_{q}, for that matter) is finitely branching, by König’s Lemma there is a path h such that each initial segment of h has such an extension. (Note that we do not claim that h itself goes through infinitely many such nodes, which would make our lives easier if it were true.) Since T r is bounded, h is actually a point in the topological space T.

For each natural number k, choose an n_{k} and σ_{k} extending h ↾ k such that q ↾ σ_{k} forces “x_{n_{k}} ≠ ∗. We can assume without loss of generality that for increasing values of k the n_{k}’s are also increasing and that the σ_{k}’s agree with longer initial segments of h. Let x̂_{k} be a term forced by σ_{k} to equal x_{n_{k}} and forced by all other sequences of the same length as σ_{k} to equal ∗. Since q ⊩ “x_{i} = ∗ iff y_{i} = ∗, ” we can similarly define ŷ_{k} to be a term forced by σ_{k} to equal y_{n_{k}} and by all other same-lengthed sequences to equal ∗. Let ẑ_{n} be a term standing for (x̂_{n}, ŷ_{n}) when those components are not ∗ and ∗ when they are. Notice that q ⊩ “ẑ_{n} is either z_{n} or ∗,” so that (for arbitrary (x, y)) q ⊩ “If (z_{n}) is eventually bounded away from (x, y), then so is (ẑ_{n}).”

Since we’re assuming that the σ_{k}’s agree with h on ever longer initial segments, then σ_{k} has to extend h ↾ k. Hence if σ(k) ≠ h(k) then for j > k q ↾ σ ⊩ “x̂_{j} = ∗”. Hence q − {h} ⊩ “(x̂_{n}) is eventually ∗, and so is eventually bounded away from X, and so in particular is bounded away from each point of X.” If q ⊩ “∀x ∈ X (x̂_{n}) is eventually bounded away from x”, then, since p ⊩ AS^{1}(X), q ⊩ “(x̂_{n}) is eventually ∗”. This, however, contradicts the choice of (x̂_{n}) and h, as no neighborhood of h can force that. Hence for some r ⊂ q and x we have r ⊩ “x ∈ X, ” yet r ⊮ “(x̂_{n}) is eventually bounded away from x”. Coupled with the opening observation in this paragraph, no neighborhood of h can force (x̂_{n}) to be eventually bounded away from x. We would like to thin this sequence so that x is the only point in X with this property.

Let r_{1} ⊆ q force “x̂_{n_{k_{1}}} is within 1 of x.” By extending r_{1} if necessary, we can assume that stem(r_{1}) ≥ length(σ_{k_{1}}). In fact, it turns out to be useful if they are equal. This can be arranged by thinning x̂_{j_{1}}. That is, letting σ be g_{r_{1}} ↾ stem(r_{1}), consider a term which is forced by q ↾ σ to be x̂_{n_{k_{1}}} and, whenever τ ≠ σ has the same length as σ, forced by q ↾ τ to be ∗. By abuse of notation, we will use the same notation x̂_{n_{k_{1}}} for this new term. Furthermore, we want to thin the sequence x̂_{n} at places before n_{k_{1}}. So for k < n_{k_{1}}, change x̂_{k} if need be to a term standing for ∗.

A desired effect of this thinning is that, for every node τ incompatible with σ, q ↾ τ forces the sequence (x̂_{n}) through (that means including) n_{k_{1}} to be the constant ∗. In order to force x̂_{n_{k_{1}}} to be within 1 of x, though, we have to be working not just beneath q, but also beneath r_{1}. So let s_{1} ⊆ q be such that stem(s_{1}) = stem(q), for stem(q) ≤ k < stem(r_{1}) g_{s_{1}}(k) = min(g_{q}(k), g_{r_{1}}(stem(r_{1}))), and for k ≥ stem(r_{1}) g_{s_{1}}(k) = g_{r_{1}}(k). To summarize, s_{1} ⊩ “ for k ≤ j_{1} either x̂_{k} = ∗ or x̂_{k} is within 1 of x,” and stem(s_{1}) = stem(q).

Let r_{2} ⊆ s_{1} force “x̂_{n_{k_{2}}} is within 1/2 of x.” By extending r_{2} if necessary, we can assume that g_{s_{1}}(stem(r_{2})−1) ≥ I +1. Thin (x̂_{n}) similarly to the above, and define s_{2} ⊆ s_{1} to be such that stem(s_{2}) = stem(q), for k < stem(r_{1}) g_{s_{2}}(k) = g_{s_{1}}(k), for stem(r_{1}) ≤ k < stem(r_{2}) g_{s_{2}}(k) = min(g_{s_{1}}(k), g_{r_{2}}(stem(r_{2}))), and for k ≥ stem(r_{2}) g_{s_{2}}(k) = g_{r_{2}}(k). What this gets us is that the stem is not increasing, for k between n_{k_{1}} and n_{k_{2}} x̂_{k} is forced to be either ∗ or within 1/2 of x, and g_{s_{2}}(stem(r_{2}) − 1) ≥ I + 1. That last fact will be preserved at future steps, enabling us to take the intersection of these open sets at the end and still have an open set.

Inductively, let r_{i+1} ⊆ s_{i} force x̂_{n_{k_{i+1}}} is within 1/i of x.” By extending r_{i+1} if necessary, assume g_{s_{i}}(stem(r_{i+1})−1) ≥ I +i. Thin (x̂_{n}), and define s_{i+1} ⊆ s_{i} to be such that stem(s_{i+1}) = stem(q), for k < stem(r_{i}) g_{s_{i+1}}(k) = g_{s_{i}}(k), for stem(r_{i}) ≤ k < stem(r_{i+1}) g_{s_{i+1}}(k) = min(g_{s_{i}}(k), g_{r_{i+1}}(stem(r_{i+1}))), and for k ≥ stem(r_{i+1}) g_{s_{i+1}}(k) = g_{r_{i+1}}(k). As before, the stem is not increasing, for k between n_{k_{i}} and n_{k_{i+1}} x̂_{k} is forced to be either ∗ or within 1/i of x, and g_{s_{i+1}}(stem(r_{i+1}) − 1) ≥ I + i.

Finally, let s_{∞} = ⋂_{i} s_{i}. We have h ∈ s_{∞}, s_{∞} is open, and for all t ⊆ s_{∞}, if h ∈ t ⊩ “(x̃_{n}) is a subsequence of (x̂_{n}),” then t ⊮ “(x̃_{n}) is eventually bounded away from x.”

Just as we had earlier found r ⊆ q and x with r ⊩ “x ∈ X” yet r ⊮ “(x̂_{n}) is eventually bounded away from x,” there are t ⊆ s_{∞} and y such that t ⊩ “y ∈ Y, ” yet t ⊮ “(ŷ_{n}) is eventually bounded away from y.” Because of the monotonicity of (x̂_{n}) approaching x forced by s_{∞}, t ⊮ “(ẑ_{n}) is eventually bounded away from (x, y).” Hence t ⊮ “(z_{n}) is eventually bounded away from (x, y).” But this contradicts the opening hypothesis of the whole theorem.

Armed with this lemma, we are almost done. Consider the sub-tree T r_{1} of T r_{q} of all finite sequences with entries less than or equal to I + 1. By the lemma, {σ ∈ T r_{1} | length(σ) = i_{n} and q ↾ σ ⊩ “x_{n} ≠ ∗”} is finite. Let j_{I+1} be the maximum of the lengths of the nodes in that set. So if some node of greater length forces some x_{n} not to be ∗, that node must have an entry larger than I + 1. More particularly, there is a largest natural number, say M, such that i_{M} ≤ j_{I+1}. For m > M, if a node forces x_{m} not to be ∗, then that node has an entry greater than I + 1. We start to define a function g. Let g ↾ stem(q) = g_{q} ↾ stem(q), and for stem(q) ≤ k ≤ j_{I+1}, g(k) = I.

Now consider the larger sub-tree that on all levels ≤ j_{I+1} has only entries ≤ I (so is compatible with g), and beyond that all numbers ≤ I + 2 may appear. (That is, σ is in the sub-tree iff σ(k) ≤ I for k ≤ j_{I+1} and σ(k) ≤ I + 2 otherwise.) Again, since there are only finitely many nodes forcing some x_{n} not to be ∗, let j_{I+2} be the maximum of their lengths. Extend g so that for j_{I+1} < k ≤ j_{I+2}, g(k) = I + 1. Notice that, when we use g as the bounding sequence g_{r} of a basic open set r, there will be no nodes allowed by g of length between j_{I+1} and j_{I+2} allowing an x_{n} not to be ∗.

In general, at stage e, consider the sub-tree with growth controlled up to height j_{I+e} by the amount of g built so far, and allowing entries up to I + e + 1 after that. Let j_{I+e+1} bound the lengths of nodes which force some x_{n} not to be ∗. Extend g to be defined up to j_{I+e+1} with the new values being I + e.

After countably many of these steps, we will have defined g to be total. Let the basic open set r be such that stem(r) = stem(q) and g_{r} = g. Then f ∈ r ⊩ “∀m > M x_{m} = y_{m} = ∗; ” in other words, f ∈ r ⊩ “(z_{n}) is eventually ∗.”

4 Realizability models

The first model above was the first developed with the intention of falsifying BD-ℕ. It was not the first observed to falsify BD-ℕ. Namely, Ishihara [16, 17] showed that certain continuity principles are equivalent with certain foundational constructive principles, among which is BD-ℕ. Continuity was studied well before BD-ℕ was ever identified, and models, apparently all of them realizability models, were developed in which these continuity properties fail. It was later observed that the other foundational principles identified by Ishihara hold in these models, and then concluded that BD-ℕ must fail. This is all very true, but somewhat unsatisfying. The argument is roundabout. One would naturally ask, for instance, just what is the pseudo-bounded yet unbounded set. The answer is, of course, implicit in the chain of arguments leading to the conclusion that BD-ℕ fails in these models. It just takes some work digging through all of that. In this section, we do that work for a representative (albeit not random) sampling of these models.

4.1 Extensional realizability

In [22] Lietz provides a thorough overview of realizability models, and an analysis of the continuity principles validated and falsified in some particularly interesting ones. We will examine only one of these, extensional realizability (Ext). To make the paper self-contained, we will give the basics of Ext; for more background, see [25] or [3], ch. XI sec. 20.^{2}

The realizers are partial equivalence relations on the natural numbers, which are also viewed as codes for computable functions (in some standard way) when considering application. On the bottom level, the naturals themselves, extensional equality is just equality. A function from ℕ to ℕ, i.e. a member of ℕ^{ℕ}, is given by an index e of a total computable function. If two such indices, say e and e′, yield the same functions, then they are extensionally equal. For an index i to stand for a function from ℕ^{ℕ} to ℕ, on equal inputs i must yield equal outputs: {i}(e) = {i}(e′). (For i to be a function from ℕ^{ℕ} to ℕ^{ℕ}, the outputs on extensionally equal inputs do not have to be numerically equal, just extensionally equal.)

At the level of the naturals, extensionality plays no role, and we have the following fact, true also in many other realizability models.

2Thanks are due here to Thomas Streicher for his correspondence explaining Ext to me.

Proposition 4.1 In Ext, every function from ℕ to ℕ is computable.

Proof: Let e ⊩ “f is a function from ℕ to ℕ.” So e ⊩ “∀n ∃m f(n) = m.” Hence ∀n ({e}(n))_{1} ⊩ f(n) = {e}(n)_{0}. So f = λn.{e}(n)_{0} is computable.

In fact, that proposition is almost enough to get BD-ℕ to be true! Let A be any countable set of naturals, and f any counting of A. Assuming a classical meta-theory, either A is bounded or it’s not. If it is, great. If not, let a_{0} be f(0) and a_{n+1} be the first value of f greater than a_{n}. (a_{n}) is computable, and witnesses that A is not pseudo-bounded.

So, in contrast to the topological models, there is no specific counter-example. Does that mean that BD-ℕ is true?

Theorem 4.2 ([22]) In Ext, BD-ℕ is false.

What’s at stake is uniformity. Each instance of BD-ℕ is true, just not uniformly so.

Central to this proof is the KLST Theorem [21, 29]. As should become clear, BD-ℕ, or the lack thereof, could be viewed as the difference KLST being true in the classical meta-theory and being true internally in Ext. It could also be viewed as the gap within Ext between the full KLST and the fragment of KLST that happens to be true there, sequential continuity. KLST is the following result in classical computability (then called recursion) theory:

Theorem 4.3 (KLST) Every computable, integer-valued function, with domain including the indices of the total computable functions, which is extensional on those indices, is continuous. That is, there is a partial computable function M such that, if {z}(y) converges for every y with {y} total, and {z}(y) = {z}(y′) whenever {y} and {y′} are total and equal to each other, then, for {y} total, M(z, y) is a modulus of convergence for {z}(y).

Lietz [22] used KLST to show the sequential continuity of all functions from ℕ^{ℕ} to ℕ in Ext. Ishihara’s [17] analysis of continuity has as a particular case that BD-ℕ yields that sequential continuity implies continuity. Troelstra [27] showed that extensionality plus a modest amount of choice (which holds in Ext) implies that not all functions from ℕ^{ℕ} to ℕ are continuous; a more accessible source is [3], ch. XI sec. 19. Taken together, as observed in [22], Ext falsifies BD-ℕ. The following argument takes those three proofs, applies them to Ext, and pulls out the concrete counter-example to BD-ℕ in Ext.

Proof: First, in Ext, every F : ℕ^{ℕ} → ℕ is sequentially continuous, as follows. Suppose g_{n} → g in ℕ^{ℕ}. A realizer z ⊩ F : ℕ^{ℕ} → ℕ is also an index for computing F: {z}(x) = F ({x}). Similarly, a realizer y ⊩ g ∈ ℕ^{ℕ} computes g: {y} = g. By KLST, M(z, y) is a modulus of convergence for F at g. However, M may not be the index of a function of higher type in Ext, as it may not be extensional. We seek something more modest – a modulus of convergence only for the sequence (g_{n}) – yet this modulus must be extensional. Since (g_{n}) converges to g, there is a k beyond which g_{n} ↾ M(z, y) = g ↾ M(z, y). That is, for n > k, g_{n} agrees with g up to a modulus of convergence, so F (g_{n}) = F (g). So evaluate {z}(y_{n}) for n from 0 through k, and pick the least n beyond which {z}(y_{n}) is the constant value F (g). That point witnesses the sequential continuity of F for g_{n} → g.

By way of notation, let e_{0} be a canonical index for the constant 0 function: {e_{0}}(n) = 0. By saying g extends 0^{m}, we mean that for x < m g(x) = 0. Later on we will have use for the type 2 version of e_{0}, which we call E_{0}, the constant 0 function with inputs from ℕ^{ℕ}.

Working in Ext, let {z} = F : ℕ^{ℕ} → ℕ. Let A_{z} be {0} ∪ {m | there is a g ∈ ℕ → ℕ extending 0^{m} and eventually 0 with {z}(g) ≠ {z}(e_{0})}. A_{z} is countable: there are only countably many eventually 0 g’s, say (g_{n}); at stage i evaluate {z}(g_{i}); if that’s unequal to {z}(e_{0}) then generate the appropriate integers into A_{z}, else generate another 0. Let e_{z} be an index for a counting of A_{z}.

Moreover, A_{z} is pseudo-bounded, as follows. Given a sequence (m_{n}) of members of A_{z}, let h_{n} be {e_{0}} if m_{n} < n, and the least corresponding g (i.e. extending 0^{m_{n}} and eventually 0 with {z}(g) ≠ {z}(e_{0})) if m_{n} ≥ n. Since h_{n} extends 0^{n}, h_{n} → {e_{0}}. By sequential continuity, we have an index beyond which {z}(h_{n}) = {z}(e_{0}). Whenever {z}(h_{n}) = {z}(e_{0}), we cannot be in the second case in the definition of h_{n}. So we’re in the first case: m_{n} < n. This is exactly the pseudo-boundedness of A_{z}. Let f_{z} be the realizer for the pseudoboundedness of A_{z} just constructed.

To show that BD-ℕ is not realized, it is enough to suppose it is, and come up with a contradiction. So suppose b ⊩ “if A ⊆ ℕ is countable and pseudo-bounded then A is bounded.” In particular, if z is an index as above, {b}(e_{z}, f_{z}) ⊩ “A_{z} is bounded,” and {b}(e_{z}, f_{z})_{0} is a bound for A_{z}. Let m be {b}(e_{E_{0}}, f_{E_{0}})_{0}.

Given β : ℕ → ℕ, let F_{β} : ℕ^{ℕ} → ℕ with index z_{β} be as follows. Given α ∈ ℕ^{ℕ}, F_{β}(α) depends only on α(m + 1). If α(m + 1) = 0, then F_{β}(α) = 0; else F_{β}(α) = β(α(m + 1) − 1). In words, to see F_{β}, take the countably branching tree ℕ^{<ℕ}; go up to the m^{th} level; each node there has countably many immediate successors; label the 0^{th} successor with 0, and spread β out on the other successors; given α a branch through that tree, follow α up to level m + 1 and return the value encountered there.

If β = {e_{0}}, then F_{β} = {E_{0}}, and by extensionality, {b}(e_{z_{β}}, f_{z_{β}})_{0} = m. On the other hand, if β ≠ {e_{0}}, then A_{z_{β}} = {0, ..., m + 1}. Hence m would not be a bound for A_{z_{β}}, and {b}(e_{z_{β}}, f_{z_{β}})_{0} > m.

To conclude, λβ.{b}(e_{β}, f_{β})_{0} is a total, computable, extensional function. By KLST, it’s continuous. But we’ve just seen it’s not: at {e_{0}} it returns m, but does not do so in any neighborhood of {e_{0}}.

4.2 fp-realizability

Beeson [2] introduced formal-provable realizability, abbreviated fp-realizability, in order to show the independence from a theory of constructive arithmetic of some continuity theorems, namely KLST (there called KLS), discussed in the previous section, and MS (Myhill-Shepherdson), the variant of KLST for partial computable functions. Beeson and Scedrov [4] extended fp-realizability to a model of full IZF set theory. Much later, following Ishihara’s analysis of continuity, Bridges et al. [12] realized that fp-realizability validates the other principles Ishihara identified, and so must falsify BD-ℕ. In this section, we bring out exactly how BD-ℕ fails.

For our purposes, the most important clause in the inductive definition of realizability is implication. In standard realizability, this is given as:

e ⊩ ϕ → ψ iff ∀x (x ⊩ ϕ → {e}(x) ⊩ ψ).

Kleene also defined a modification of this realizability, that includes not only that x must realize ϕ but also that ϕ must be provable:

e ⊩ ϕ → ψ iff ∀x (x ⊩ ϕ ∧ P r(ϕ) → {e}(x) ⊩ ψ),

where P r is some appropriate proof predicate. Beeson’s fp-realizability does this one step better, by having that not only must x realize ϕ, and not only that ϕ is provable, but even that the realizability of ϕ by x must be provable:

e ⊩ ϕ → ψ iff ∀x (P r(x ⊩ ϕ) → {e}(x) ⊩ ψ),

where we can afford to eliminate the clause x ⊩ ϕ from the antecedent by the presumed soundness of the provability predicate. What makes this work for our purposes is that more needs to be put in than needs to be put out: the input must be provably realizing, the output merely realizing.

The version of fp-realizability Beeson uses is non-numerical, in that the realizers themselves are suppressed. That is, a translation is given from formulas ϕ to formulas ϕ^{r}, where the latter should be thought of as “ϕ is realized.” The reason given for doing that is that it makes the proof of soundness of fp-realizability easier, although it is observed that it actually makes a difference in some cases about what’s realized, fortunately not in any cases of current interest. The version of fp-realizability given below contains the realizers, because the reader is likely to be more familiar and comfortable with such a presentation. It was derived from Beeson’s non-numerical variant by making what seemed like the only possible such extrapolation. The clauses are:

e ⊩ ϕ iff ϕ (for ϕ atomic) e ⊩ ϕ ∧ ψ iff e_{0} ⊩ ϕ and e_{1} ⊩ ψ e ⊩ ϕ ∨ ψ iff (e_{0} = 0 and P r(e_{1} ⊩ ϕ)) or (e_{0} = 1 and P r(e_{1} ⊩ ψ) e ⊩ ϕ → ψ iff for all x if P r(x ⊩ ϕ) then {e}(x) ⊩ ψ e ⊩ ∀x ϕ(x) iff for all x e ⊩ ϕ(x) e ⊩ ∃x ϕ(x) iff P r(e_{1} ⊩ ϕ(e_{0})).

As usual, ¬ϕ is an abbreviation for ϕ → 0 = 1.

Theorem 4.4 ([12]) Under fp-realizability, BD-ℕ is false.

By analogy with the realizability from the previous section, and realizability in general, you might think that the failure of BD-ℕ is once again the lack of uniformity. Quite to the contrary, here we have a case of a particular counterexample instead.

Definition 4.5 {w}(z) ↓_{<n} if the function coded by w when applied to z converges in fewer than n many steps with output less than n.

Definition 4.6 Let {v}(n) = max{k < n | ∀j, w, z < k if j codes a proof that {w} is total then {w}(z) ↓_{<n}}.

Proof: We will show that rng({v}) is the desired counter-example.

For the countability of rng({v}), we need that {v} is realized to be total. The realizer for this is v itself, which works as long as {v} is actually total. That’s the case because {v}(n) is the maximum of a bounded set, and membership in the set is determined by a finite search.

Now consider the task of realizing that the range of {v} is not bounded. First note that {v} is actually unbounded: to get an n_{k} with {v}(n_{k}) ≥ k, we need to consider all proofs j < k that w < k codes a total function; by soundness {w} then is total; so just wait long enough so that for all such w and z < k {w}(z) has converged. So no e could realize that k is a bound to rng({v}), because n_{k} is a counter-example to that. Hence nothing can realize that rng({v}) is bounded. By the definition of forcing a negation, everything realizes that rng({v}) is not bounded.

The real work is showing that the range of {v} is pseudo-bounded. We need to realize “if f enumerates a subset of rng{v} then there is a bound beyond which f(n) ≤ n.” Suppose x provably realizes the antecedent:

P r(x ⊩ ∀i ∃m f(i) = {v}(m)).

In particular, for all i, f(i) = {v}({x}(i)_{0}).

Let N > x code such a proof. In particular, N also proves that {x} is total, which is all we need. Then for n > N

f(n) = {v}({x}(n)_{0})

= max {k < {x}(n)_{0} | ∀j, w, z < k if j codes a proof
that w is total then {w}(z) ↓<_{{x}(n)_{0}}}.

Consider any k > n, by way of seeing whether it’s in the set above. Let j, w, z be N, x, n, respectively. We need to consider whether {x}(n) ↓<_{{x}(n)_{0}}. That could not happen, since {x}(n) ≥ {x}(n)_{0}, as a pair is at least as large as each of its components. So f(n) is the max of a set which includes nothing greater than n, hence f(n) ≤ n.

5 Questions

Both topological models presented here were called the natural models. This was done because it feels right. They seem like the obvious guesses for topological models violating BD and BD-ℕ. Also, they seem to violate as little else as possible, as for instance the property of anti-Specker spaces discussed still holds. But what could it mean for these models to be natural? How could that be made more precise?

What other independence results could these models show? What other consequences of BD and BD-ℕ might still hold in them?

We discussed two realizability models, one with a specific counter-example, the other with no counter-example, just a lack of uniformity. The topological models both have counter-examples. Is there a topological failure of BD or BD-ℕ with no one counter-example? This is possible on general principles: it could be that every pseudo-bounded set is not not bounded, while there is no open set forcing a bound for each pseudo-bounded set simultaneously. A general way of doing this is forcing with settling [24, 23]. The reason that answer is not satisfactory is that settling does not produce a model of IZF. Power Set must fail; even Subset Collection would. So what would be a topological model of IZF in which each instance of BD (resp. BD-ℕ) holds densely but BD (resp. BD-ℕ) doesn’t?

We discussed the models over the space of bounded sequences and the space of unbounded sets. What are the models like over the space of unbounded sequences and the space of bounded sets? Is there anything interesting going on there, especially relative to BD and BD-ℕ?

References

[1] James E. Baumgartner, “Iterated forcing,” in Surveys in Set Theory, London Mathematical Society Lecture Note Series, vol. 87, Cambridge University Press, Cambridge, 1983, p. 1-59

[2] Michael Beeson, “The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations,” Journal of Symbolic Logic, v. 40 (1975), p. 321-346

[3] Michael Beeson, Foundations of Constructive Mathematics, Springer, Berlin, 1985

[4] Michael Beeson and Andre Scedrov, “Church’s thesis, continuity, and set theory,” Journal of Symbolic Logic, v. 49 (1984), p. 630-643

[5] Josef Berger and Douglas Bridges, “A Fan-theoretic equivalent of the antithesis of Speckers Theorem,” Proc. Koninklijke Nederlandse Akad. Wetenschappen (Indag. Math., N.S.), v. 18 (2007), p. 195-202 [6] Josef Berger and Douglas Bridges, “The anti-Specker property, a Heine-

Borel property, and uniform continuity,” Archive for Mathematical Logic, v. 46 (2008), p. 583-592

[7] Errett Bishop, Foundations of Constructive Mathematics, McGraw-Hill, New York, 1967

[8] Errett Bishop and Douglas Bridges, Constructive Analysis, Springer, Berlin, 1985

[9] Douglas Bridges, “Constructive notions of equicontinuity,” Archive for Mathematical Logic, v. 48 (2009), p. 437-448

[10] Douglas Bridges, “Uniform equicontinuity and the antithesis of Specker’s Theorem,” unpublished

[11] Douglas Bridges, “Inheriting the anti-Specker property”, preprint, University of Canterbury, NewZealand, 2009, submitted for publication

[12] Douglas Bridges, Hajime Ishihara, Peter Schuster, and Luminita Vita, “Strong continuity implies uniformly sequential continuity,” Archive for Mathematical Logic, v. 44 (2005), p. 887-895

[13] Douglas Bridges and Fred Richman, Varieties of Constructive Mathematics, London Mathematical Society Lecture Note Series, vol. 97, Cambridge University Press, Cambridge, 1987

[14] Robin J. Grayson, “Heyting-valued models for intuitionistic set theory,” in Applications of Sheaves, Lecture Notes in Mathematics, vol. 753 (eds. Fourman, Mulvey, Scott), Springer, Berlin Heidelberg New York, 1979, p. 402-414

[15] Robin J. Grayson, “Heyting-valued semantics,” in Logic Colloquium ’82, Studies in Logic and the Foundations of Mathematics, vol. 112 (eds. Lolli, Longo, Marcja) , North-Holland, Amsterdam New York Oxford, 1984, p. 181-208

[16] Hajime Ishihara, “Continuity and nondiscontinuity in constructive mathematics,” Journal of Symbolic Logic, v. 56 (1991), p. 1349-1354

[17] Hajime Ishihara, “Continuity properties in constructive mathematics,” Journal of Symbolic Logic, v. 57 (1992), p. 557-565

[18] Hajime Ishihara, “Sequential continuity in constructive mathematics,” in Combinatorics, Computability, and Logic (eds. Calude, Dinneen, and Sburlan), Springer, London, 2001, p. 5-12

[19] Hajime Ishihara and Peter Schuster, “A Continuity principle, a version of Baire’s Theorem and a boundedness principle,” Journal of Symbolic Logic, v. 73 (2008), p. 1354-1360 [20] Hajime Ishihara and Satoru Yoshida, “A Constructive look at the complete-

ness of D(R),” Journal of Symbolic Logic, v. 67 (2002), p. 1511-1519

[21] Georg Kreisel, Daniel Lacombe, and Joseph Shoenfield, “Partial recursive functions and effective operations,” in Constructivity in Mathematics (ed. Arend Heyting), North-Holland, 1959, p. 195-207

[22] Peter Lietz, “From Constructive Mathematics to Computable Analysis via the Realizability Interpretation,” Ph.D. thesis, Technische Universität Darmstadt, 2004, http://www.mathematik.tu-darmstadt.de/ streicher/THESES/lietz.pdf.gz

[23] Robert Lubarsky, “Topological forcing semantics with settling,” in Proceedings of LFCS 09, Lecture Notes in Computer Science No.5407 (eds. Sergei N. Artemov and Anil Nerode), Springer, 2009, p. 309-322; also Annals of Pure and Applied Logic, to appear; available at http://math.fau.edu/lubarsky/pubs.html

[24] Robert Lubarsky and Michael Rathjen, “On the constructive Dedekind Reals,” Logic and Analysis, v. 1 (2008), pp. 131-152; also in Proceedings of LFCS ’07, Lecture Notes in Computer Science No. 4514 (eds. Sergei N. Artemov and Anil Nerode), Springer, 2007, pp. 349-362

[25] Jap van Oosten, “Extensional realizability,” Annals of Pure and Applied Logic, v. 84 (1997), p. 317-349

[26] Ernst Specker, “Nicht konstruktiv beweisbare Sätze der Analysis,” Journal of Symbolic Logic, v. 14 (1949), p. 145-158

[27] Anne S. Troelstra, “A Note on non-extensional operations in connection with continuity and recursiveness,” Indagationes Mathematicae, v. 39 (1977), p. 455-462

[28] Anne S. Troelstra and Dirk van Dalen, Constructivism in Mathematics, vol. 1, North-Holland, Amsterdam, 1988

[29] G.S. Tseitin, “Algorithmic operators in constructive complete metric spaces,” Doklady Akademii Nauk SSSR, v. 128 (1959), p. 49-52