CCA 2006

On the Cauchy Completeness of the Constructive Cauchy Reals

Robert S. Lubarsky ^{1 ,2}

Dept. of Mathematical Sciences Florida Atlantic University Boca Raton, FL 33431, USA

Abstract Intuitionistic set theory without choice axioms does not prove that every Cauchy sequence of rationals has a modulus of convergence, or that the set of Cauchy sequences of rationals is Cauchy complete. Several other related non-provability results are also shown. Keywords: Cauchy sequence, modulus of convergence, intuitionistic set theory, topological model, Kripke model

1 Introduction

Are the reals Cauchy complete? This is, for every Cauchy sequence of real numbers, is there a real number which is its limit?

This sounds as though the answer should be “of course”. After all, the reals are defined pretty much to make this true. The reason to move from the rationals to the reals is exactly to “fill in the holes” that the rationals have. So however you define R, you’d think its Cauchy completeness would be immediate. At the very least, this property would be a litmus test for any proffered definition.

In fact, for the two most common notions of real number, Dedekind and Cauchy real, this is indeed the case, under classical logic. First off, classically Cauchy and Dedekind reals are equivalent anyway. Then, taking a real as an equivalence class of Cauchy sequences, given any Cauchy sequence of reals, a canonical representative can be chosen from each real, and a limit real can be built from them by a kind of diagonalization, all pretty easily.

Intuitionistically, though, this whole procedure breaks down. Starting even at the beginning, Cauchy and Dedekind reals are no longer equivalent notions (see [2]

1 Thanks are due to Thomas Streicher for his careful reading of the first proof, and to Michael Rathjen for bringing the question that got this started to my attention and for his support during this work.

2 Email: Robert.Lubarsky@alum.mit.edu

This paper is electronically published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Lubarsky

or [4]). While the Dedekind reals are complete, working with the Cauchy reals, it’s not clear that a representative can be chosen from each equivalence class, or, even if you could, that a limit could be built from them by any means.

It is the purpose of this paper to show that, indeed, such constructions are not in general possible, answering a question of Martin Escardo and Alex Simpson ([1]).

While the original motivation of this work was to show the final theorem, that the Cauchy reals are not provably Cauchy complete, it is instructive to lay out the framework and examine the related questions so laid bare. A Cauchy real is understood as an equivalence class of Cauchy sequences of rationals. When working with a Cauchy sequence, one usually needs to know not only that the sequence converges, but also how fast. In classical set theory, this is definable from the sequence itself, and so is not problematic. The same cannot be said for other contexts. For instance, in recursion theory, the complexity of the convergence rate might be important. In our context, intuitionistic set theory, the standard way to define a modulus of convergence just doesn’t work. Certainly given a Cauchy sequence X(n) and positive rational ϵ, there is an integer N such that for m, n > N | X(n) - X(m) |< ϵ: that’s the definition of a Cauchy sequence. A modulus of convergence is a function f such that for any such ϵ f on ϵ returns such an N. Classically this is easy: let f return the least such N. Intuitionistically that won’t work. And there’s no obvious alternative. So a real is taken to be an equivalence class of pairs ⟨X, f⟩, where X is a Cauchy sequence and f a modulus of convergence.

One immediate source of confusion here is identifying reals with sequencemodulus pairs. A real is an equivalence class of such pairs, and it is not obvious how a representative can be chosen constructively from each real; in fact, this cannot in general be done, as we shall see. This distinction has not always be made though. For instance, as observed by Fred Richman, in [7], the Cauchy completeness of the reals was stated as a theorem, but what was proved was the Cauchy completeness of sequence-modulus pairs. To be precise, what was shown was that, given a countable sequence, with its own modulus of convergence, of sequence-modulus pairs, then there is a limit sequence, with modulus. For that matter, it is not hard (and left to the reader) that, even if the given sequence does not come equipped with its own modulus, it still has a Cauchy sequence as a limit, although we will have to punt on the limit having a modulus. But neither of those two observations is the Cauchy completeness of the reals.

Nonetheless, these observations open up the topic about what kinds of behavior in the limit one can expect given certain input data. There are two, independent parameters. Does the outside Cauchy sequence have a modulus of convergence? And are its individual members sequence-modulus pairs, or merely naked sequences? Notice that, while the first question is yes-no, the second has a middle option: the sequences have moduli, but not uniformly. Perhaps each entry in the big sequence is simply a Cauchy sequence of rationals, and it is hypothesized to have a modulus somewhere, with no information about the modulus given. These possibilities are all summarized in the following table.

Entries in the outside Cauchy sequence are:

seq-mod pairs seqs that have mods seqs that may not
somewhere  have mods anywhere

Outside seq

has a mod

Outside seq

doesn’t

have a mod

Not to put the cart before the horse, is it even possible to have a Cauchy sequence with no modulus of convergence, or with only non-uniform moduli? It has already been observed that the obvious classical definition of such does not work intuitionistically, but it still remains to be shown that no such definition is possible.

The goal of this paper is to prove the negative results as much as possible, that any given hypothesis does not show that there is a limit Cauchy sequence, or in certain cases that there is no limit with a modulus.

The positive results are all easy enough (even if the last one is a bit tricky) and so are left as exercises. They are:

(i) Every Cauchy sequence with modulus of sequence-modulus pairs has a limit sequence with modulus.

(ii) Every Cauchy sequence of sequence-modulus pairs has a limit sequence. (iii) Every Cauchy sequence with modulus of Cauchy sequences has a limit sequence.

In tabular form, the positive results are:

Entries in the outside Cauchy sequence are:

seq-mod pairs seqs that have mods seqs that may not
somewhere  have mods anywhere
Outside seq  There is a  There is a  There is a
has a mod limit with mod.  limit sequence.  limit sequence.

Outside seq

doesn’t  There is a
have a mod limit sequence.

Regarding the first and last columns, the negative results are that these are the positive results cited above are the best possible. In detail:

Theorem 2.1 IZF_{Ref} does not prove that every Cauchy sequence has a modulus of convergence. It follows that IZF_{Ref} does not prove that every Cauchy sequence of sequence-modulus pairs converges to a Cauchy sequence with a modulus of convergence.

Theorem 4.1 IZF_{Ref} does not prove that every Cauchy sequence of Cauchy sequences converges to a Cauchy sequence.

Theorem 5.1 IZF_{Ref} does not prove that every Cauchy sequence with a modulus of convergence of Cauchy sequences converges to a Cauchy sequence with a modulus of convergence.

The middle column is discussed briefly in the questions in the last section of this paper.

In tabular form, these negative results are:

Entries in the outside Cauchy sequence are:

seq-mod pairs seqs that have mods seqs that may not
somewhere  have mods anywhere
Outside seq  See questions,  Limit may not have
has a mod  section 7.  a mod. thm 5.1
Outside seq Limit may not  There may not
doesn’t  have a mod.  See questions,  even be a limit.
have a mod  thm 2.1  section 7.  thm 4.1

Then there is the major negative result, the original and ultimate motivation of this work:

Theorem 6.1 IZF_{Ref} does not prove that every Cauchy sequence of reals has a limit.

Recalling that a real is here taken as an equivalence class of sequence-modulus pairs, to prove this result it would suffice to construct a Cauchy sequence (perhaps itself without modulus) of reals, with no sequence-modulus pair as a limit. We will do a tad better, constructing a Cauchy sequence, with modulus, of reals, with no Cauchy sequence, even without modulus, as a limit.

At this point a word about the meta-theory is in order. The results here are stated as non-theorems of IZF_{Ref}, which is the variant of IZF in which the Collection schema is replaced by the Reflection schema. The point is that these independence results are not meant to be based on a weakness of the underlying set theory. Hence the set theory taken is the strongest version of the intuitionistic theories commonly considered. The results would remain valid if IZF were augmented by yet stronger hypotheses, such as large cardinals. Of course, these remarks do not apply if IZF is augmented by whatever choice principle would be enough to build the sequences and moduli here claimed not to exist. Clearly Dependent Choice is strong enough for everything at issue here: choosing representatives from equivalence classes, building moduli, constructing Cauchy sequences. The question what weaker choice principle/s would suffice is addressed in [5].

Regarding the methodology, counter-examples are constructed in each case. These examples could be presented as either topological or Kripke models. While certain relations among topological and Kripke models are known, it is not clear to the author that the natural models in the cases before us are really the same. While the family resemblance is unmistakable (compare sections 2 and 3 below, for instance), it can be deceiving. For instance, the first model of [4] seems to be merely the Kripke version of one of the models of [2] (also in in [6], VI.8), there presented as a sheaf model but easily enough recastable as topological. But there are differences. For instance, consider Bas Spitters’ proof that in the topological model the reals are not uncountable. (His proof consists of a countable list of reals and a demonstration that every real is not apart from all reals on his list. Recalling that in the topological model a real is given by a continuous function, the countable list consists of the two families of functions x + r and −x + r, where r ranges over the rationals.) Pretty much the same argument works in the Kripke model, but it can stand a simplification that would not work in the topological model. (In the Kripke model, it suffices to consider reals of only the form x + r.) Such a difference is certainly subtle, arguably small, but exists nonetheless, and is enough to say that the models are not the same. A better understanding of the relations among Kripke and topological models would be a worthwhile project for some other time. For now, we would like to present the reader with adequate information without being long-winded. Hence all of the constructions will be presented as topological models, since there is better technology for dealing with them. In particular, there is already a meta-theorem (see [3]) that the (full) model over any Heyting algebra models IZF (easily, IZF_{Ref} too). So we will never have to prove that our topological models satisfy IZF_{Ref}. In contrast, we know of no such meta-theorem that would apply to the Kripke models in question. In the simplest case, the first theorem, the Kripke model will also be given, so the reader can see what’s going on there. But even a cursory glance at that argument should make it clear why the author does not want to repeat the proofs of IZF_{Ref} and all the auxiliary lemmas, and the reader likely does not want to read them, three more times.

One last word about notation/terminology. For p an open set in a topological space and ϕ a formula in set theory (possibly with parameters from the topological model), “p ⊆ ∥ϕ∥”, “p ⊩ ϕ”, and “p forces ϕ” all mean the same thing. Also, “WLOG” stands for “without loss of generality”.

2 Not every Cauchy sequence has a modulus of convergence

Theorem 2.1 IZF_{Ref} does not prove that every Cauchy sequence has a modulus of convergence. It follows that IZF_{Ref} does not prove that every Cauchy sequence of sequence-modulus pairs converges to a Cauchy sequence with a modulus of convergence.

The second assertion follows immediately from the first: given a Cauchy sequence X(n), for each n let X_{n} be the constant sequence X(n) paired with some modulus of convergence independent of n. Sending X to the sequence ⟨X_{n} | n ∈ N⟩ embeds the Cauchy reals into Cauchy sequences of sequence-modulus pairs. If provably every one of the latter had a modulus, so would each of the former.

To prove the first assertion, we will build a topological model with a specific Cauchy sequence Z(n) of rationals with no modulus of convergence.

The topological space T consists of all Cauchy sequences of rationals.

A basic open set is given by (p, I), where p is a finite sequence of rationals and I is an open interval. A Cauchy sequence X is in (the open set determined by) (p, I) if p ⊆ X, rng(X\p) ⊆ I, and lim(X) ∈ I. (Notice that, under this representation, the whole space T is given by (∅, R), and the empty set is given by (p, ∅) for any p.)

For this to generate a topology, it suffices to show that the basic open sets are closed under intersection. Given (p, I) and (q, J), if p and q are not compatible (i.e. neither is an extension of the other), then (p, I) ∩ (q, J) = ∅. Otherwise WLOG let q ⊇ p. If rng(q\p) ⊈ I then again (p, I) ∩ (q, J) = ∅. Otherwise (p, I) ∩ (q, J) = (p∪q, I∩J) = (q, I∩J).

Let M be the Heyting-valued models based on T, as describes in e.g. [3]. Briefly, a set in M is a collection of objects of the form ⟨σ, (p, I) ⟩, where σ inductively is a set in M. It is shown in [3] that M ⊧ IZF_{Coll} (assuming IZF_{Coll} in the meta-theory). Similarly, assuming IZF_{Ref} in the meta-theory yields M ⊧ IZF_{Ref}.

We are interested in the term {⟨p̄, (p, I)⟩ |(p, I) is an open set}. (Here p̄ is the canonical name for p. Each set in V has a canonical name in M by choosing (p, I) to be (∅, R) hereditarily: x̄ = {⟨ȳ, (∅, R)⟩ | y ∈ x}.) We will call this term Z.

Proposition 2.2 ∥ Z is a Cauchy sequence ∥ = T.

Proof. To see that ∥Z is total∥ = T, let N be an integer. (Note that each integer in M can be identified locally with an integer in V. For notational ease, we will identify integers in M and V.) Let p be any sequence of rationals of length > N. Then (p, R) ⊆ ∥ Z(N) = p(N) ∥ ⊆ ∥ N ∈ dom(Z) ∥. As T is covered by the open sets of that form, T ⊆ ∥ N ∈ dom(Z) ∥. That Z is a function is similarly easy.

As for Z being Cauchy, again let N be an integer and X be in T. Since X is Cauchy, there is an integer M such that beyond M X stays within an interval I of size 1/(2N). Of course, X’s limit might be an endpoint of I. So let J extend I on either side and still have length less that 1/N. Then X ∈ (X↾M, J) ⊆ ∥∀ m, n > M | Z(m) - Z(n) |≤ 1/N ∥, making Z “Cauchy for 1/N”, to coin a phrase. □

In order to complete the theorem, we need only prove the following

Proposition 2.3 ∥Z has no modulus of convergence∥ = T.

Proof. Suppose (p, I) ⊆ ∥f is a modulus of convergence for Z∥. WLOG I is a finite interval. Let n be such that 1/n is less than the length of I, and let ϵ be (length(I)

- 1/n)/2.

Let (q, J) ⊆ (p, I) force a value m for f(n). WLOG length(q) > m, as q could be so extended. If J=I, then (q, J) could be extended simply by extending q with two values a distance greater than 1/n apart, thereby forcing f not to be a modulus of convergence. So J ⊂ I. That means either inf J > inf I or sup J < sup I. WLOG assume the latter. Let mid J be the midpoint of J, q_{0} be q extended by mid J, and J_{0} be (mid J, sup J). Then (q_{0}, J_{0}) ⊆ (q, J), and therefore (q_{0}, J_{0}) ⊆ ∥f(n) = m∥.

What (q_{1}, J_{1}) is depends:

CASE I: There is an open set K containing sup(J_{0}) such that (q_{0}, K) ⊆ ∥f(n) = m∥. Then let j_{max} be the sup of the right-hand endpoints (i.e. sups) of all such K’s. Let q_{1} be q_{0} extended by sup J_{0}.

\underline{Claim}: (q_{1}, (sup J_{0}, j_{max})) ⊆ ∥f(n) = m∥.

Proof. Let j ∈ (sup J_{0}, j_{max}). By hypothesis, there is a K such that (q_{1}, (sup J_{0}, j)) ⊆ (q_{1}, K) ⊆ ∥f(n) = m∥. Since (q_{1}, (sup J_{0}, j_{max})) is the union of the various (q_{1}, (sup J_{0}, j))’s over such j’s, the claim follows. □

Of course, J_{1} will be (sup J_{0}, j_{max}).

CASE II: Not Case I. Then extend by the midpoint again. That is, q_{1} is q_{0} extended by mid J_{0}, and J_{1} is (mid J_{0}, sup J_{0}). Also in this case, (q_{1}, J_{1}) ⊩ f(n) = m.

Clearly we would like to continue this construction. The only thing that might be a problem is if the right-hand endpoint of some J_{k} equals (or goes beyond!) sup I, as we need to stay beneath (p, I). In fact, as soon as sup(J_{k}) > sup(I) - ϵ (if ever), extend q_{k} by something within ϵ of sup I, and continue the construction with left and right reversed. That is, instead of going right, we now go left. This is called “turning around”.

What happens next depends.

CASE A: We turned around, and after finitely many more steps, some J_{k} has its inf under inf(I) + ϵ. Then extend q_{k} by something within ϵ of inf I. This explicitly blows f being a modulus of convergence for Z.

CASE B: Not Case A. So past a certain point (either the stage at which we turned around, or, if none, from the beginning) we’re marching monotonically toward one of I’s endpoints, but will always stay at least ϵ away. WLOG suppose we didn’t turn around. Then the construction will continue for infinitely many stages. The q_{k}’s so produced will in the limit be a (monotonic and bounded, hence) Cauchy sequence X. Furthermore, lim X is the limit of the sup(J_{k})’s. Finally, X ∈ (p, I). Hence there is an open set (q’, K) with X ∈ (q’, K) ⊆ ∥f(n) = m’∥, for some m’. Let k be such that sup(J_{k}) ∈ K, and q_{k} ⊇ q’. Consider (q_{k}, J_{k}). Note that (q_{k}, J_{k} ∩ K) extends both (q_{k}, J_{k}) and (q’, K), hence forces both f(n) = m and f(n) = m’, which means that m=m’.

Therefore, at this stage in the construction, we are in Case I. By the construction, J_{k+1} = (sup J_{k}, j_{max}), where j_{max} ≥ sup K > lim X = lim_{k} (sup(J_{k})) ≥ sup(J_{k+1}) = j_{max}, a contradiction. □

3 Same theorem, Kripke model version

Theorem 2.1 IZF_{Ref} does not prove that every Cauchy sequence has a modulus of convergence.

3.1 Construction of the Model

Let M_{0} ≺ M_{1} ≺ ... be an ω-sequence of models of ZF set theory and of elementary embeddings among them, as indicated, such that the sequence from M_{n} on is definable in M_{n}, and such that each thinks that the next has non-standard integers. Notice that this is easy to define (mod getting a model of ZF in the first place): an iterated ultrapower using any non-principal ultrafilter on ω will do. We will ambiguously use the symbol f to stand for any of the elementary embeddings inherent in the M_{n}-sequence.

The Kripke model M will have underlying partial order a non-rooted tree; the bottom node (level 0) will have continuum (in the sense of M_{0}) many nodes, and the branching at a node of level n will be of size continuum in the sense of M_{n+1}. (We will eventually name each node by associating a Cauchy sequence to it. Some motivation will be presented during this section, and the final association will be at the end of this section.) Satisfaction at a node will be indicated with the symbol ⊧. There is a ground Kripke model, which, at each node of level n, has a copy of M_{n}. The transition functions (from a node to a following node) are the elementary embeddings given with the original sequence of models (and therefore will be notated by f again). Note that by the elementarity of the extensions, this Kripke model is a model of classical ZF. More importantly, the model restricted to any node of level n is definable in M_{n}, because the original M-sequence was so definable.

The final model M will be an extension of the ground model that will be described like a forcing extension. That is, M will consist of (equivalence classes of) the terms from the ground model. The terms are defined at each node separately, inductively on the ordinals in that model. At any stage α, a term of stage α is a set σ of the form {⟨σ_{j}, (p_{j}, I_{j})⟩ | j ∈ J}, where J is some index set, each σ_{i} is a term of stage < α, each p_{j} is a finite function from N to Q, and each I_{j} is an open rational interval on the real line. Note that all sets from the ground model have canonical names, by choosing each p_{j} to be the empty function and I_{j} to be the whole real line, hereditarily.

Notice also that the definition of the terms given above will be interpreted differently at each node of the ground Kripke model, as the N and Q change from node to node. However, any term at a node gets sent by the transition function f to a corresponding term at any given later node. The definitions given later, such as the forcing relation ⊩, are all interpretable in each M_{n}, and coherently so, via the elementary embeddings.

As a condition, each finite function p is saying “the Cauchy sequence includes me”, and each interval I is saying “future rationals in the Cauchy sequence have to come from me”. For each node of level n there will be an associated Cauchy sequence r (in the sense of M_{n}) such that at that node the true p’s and I’s will be those compatible with r (or, perhaps, those with which r is compatible, as the reader will). You might reasonably think that compatibility means “p ⊂ r and rng(r\p) ⊆ I”: roughly, “r extends p, and anything in r beyond p comes from I”. But that’s not quite right. Consider the Cauchy sequence r(n) = 1/n (n ≥ 1). rng(r) ⊆ (0, 2), but in a non-standard extension, r’s pattern could change at a non-standard integer; at that point, it would be too late for r to change by a standard amount, but it could change by an infinitesimal amount. So the range of r could include (infinitely small) negative numbers, which are outside of (0, 2). Hence we have the following

Definition 3.1 A condition (p, I) and a Cauchy sequence r are \underline{compatible} if p ⊆ r, rng(r\p) ⊆ I, and lim(r) ∈ I.

(p, I) is compatible with a finite function q if p ⊆ q and rng(q\p) ⊆ I.

Given this notion of compatibility, speaking intuitively here, a term σ can be thought of as being interpretable (with notation σ^{r}) inductively in M_{n} as {σ_{j}^{r} | ⟨σ_{j}, p_{j}, I_{j}⟩ ∈ σ and r is compatible with (p_{j}, I_{j})}. (This notion is hidden in the more formal development below, where we define and then mod out by =_{M}.)

Our next medium-term goal is to define the primitive relations at each node, =_{M} and ∈_{M} (the subscript being used to prevent confusion with equality and membership of the ambient models M_{n}). In order to do this, we need first to develop our space’s topology.

Definition 3.2 (q, J) ≤ (p, I) ((q, J) \underline{extends} (p, I)) if q ⊇ p, J ⊆ I, and rng(q\p) ⊂ I.

C = \{(p_{j}, I_{j}) | j ∈ J\} \underline{covers} (p, I) if each (p_{j}, I_{j}) extends (p, I) and each Cauchy sequence r compatible with (p, I) is compatible with some (p_{j}, I_{j}).

≤ induces a notion of compatibility of conditions (having a common extension). We say that a typical member ⟨σ, (p, I) ⟩ of a term is \underline{compatible} with (q, J) if (p, I) and (q, J) are compatible.

We need some basic facts about this p.o., starting with the fact that it is a p.o.

Lemma 3.3 (i) ≤ is reflexive, transitive, and anti-symmetric. (ii) If (p, I) and (q, J) are each compatible with a Cauchy sequence r, then they

are compatible with each other. (iii) If (p, I) and (q, J) are compatible, then their glb in the p.o. is (p∪q, I∩J). (iv) {(p, I)} covers (p, I).

(v) A cover of a cover is a cover. That is, if C covers (p, I), and, for each (p_{j}, I_{j}) ∈ C, C_{j} covers (p_{j}, I_{j}), then ⋃_{j}C_{j} covers (p, I).

(vi) If C covers (p, I) and (q, J) ≤ (p, I), then (q, J) is covered by C ∧ (q, J) =_{def} {(p_{j}∪q, I_{j}∩J) | (q, J) is compatible with (p_{j}, I_{j}) ∈ C}.

Proof. Left to the reader. □

Now we are in a position to define =_{M} and ∈_{M}. This will be done via a forcing relation ⊩.

Definition 3.4 (p, I) ⊩ σ =_{M} τ and (p, I) ⊩ σ ∈_{M} τ are defined inductively on σ and τ, simultaneously for all (p, I):

(p, I) ⊩ σ =_{M} τ iff for all ⟨σ_{j}, (p_{j}, I_{j})⟩ ∈ σ compatible with (p, I) (p∪p_{j}, I ∩I_{j}) ⊩ σ_{j} ∈_{M} τ and vice versa, and

(p, I) ⊩ σ ∈_{M} τ iff there is a cover C of (p, I) such that for all (p_{j}, I_{j}) ∈ C there is a ⟨τ_{k}, (p_{k}, I_{k})⟩ ∈ τ such that (p_{j}, I_{j}) ≤ (p_{k}, I_{k}) and (p_{j}, I_{j}) ⊩ σ =_{M} τ_{k}.

(We will later extend this forcing relation to all formulas.)

Definition 3.5 At a node (with associated real r), for any two terms σ and τ, σ =_{M} τ iff, for some (p, I) compatible with r, (p, I) ⊩ σ =_{M} τ.

Also, σ ∈_{M} τ iff for some (p, I) compatible with r, (p, I) ⊩ σ ∈_{M} τ.

Thus we have a first-order structure at each node.

The transition functions are the same as before. That is, if σ is an object at a node, then it’s a term, meaning in particular it’s a set in some M_{n}. Any later node has for its universe the terms from some M_{m}, m ≥ n. With f the elementary embedding from M_{n} to M_{m}, f can also serve as the transition function between the given nodes. These transition functions satisfy the coherence conditions necessary for a Kripke model.

To have a Kripke model, f must also respect =_{M} and ∈_{M}, meaning that f must be an =_{M}- and ∈_{M}-homomorphism (i.e. σ =_{M} τ → f(σ) =_{M} f(τ), and similarly for ∈_{M}). In order for these to be true, we need an additional restriction on the model. By way of motivation, one requirement is, intuitively speaking, that the sets σ can’t shrink as we go to later nodes. That is, once σ_{j} gets into σ at some node, it can’t be thrown out at a later node. σ_{j} gets into σ because r is compatible with (p_{j}, I_{j}) (where ⟨σ_{j}, (p_{j}, I_{j})⟩ ∈ σ). So we need to guarantee that if r and (p, I) are compatible and r’ is associated to any extending node then r’ and (p, I) are compatible for any condition (p, I). This holds exactly when r’ extends r and all of the entries in r’\r are infinitesimally close to lim(r). This happens, for instance, when r’ = f(r). Other such examples would be f(r) truncated at some non-standard place and arbitrarily extended by any Cauchy sequence through the reals with standard part lim(r); in fact, all such r’ have that form. We henceforth take this as an additional condition on the construction: once r is associated to a node, then for any r’ associated to an extending node, rng(r’\r) must consist only of rationals infinitely close to lim(r).

Lemma 3.6 f is an =_{M} and ∈_{M}-homomorphism.

Proof. If σ =_{M} τ then let (p, I) compatible with r witness as much. At any later node, (p, I) = f((p, I)) = (f(p), f(I)) ⊩ f(σ) =_{M} f(τ). Also, the associated real r’ would still be compatible with (p, I). So the same (p, I) would witness f(σ) =_{M} f(τ) at that node. Similarly for ∈_{M}. □

We can now conclude that we have a Kripke model.

Lemma 3.7 This Kripke model satisfies the equality axioms:

(i) ∀x x = x (ii) ∀x, y x = y → y = x (iii) ∀x, y, z x = y ∧ y = z → x = z (iv) ∀x, y, z x = y ∧ x ∈ z → y ∈ z

(v) ∀x, y, z x = y ∧ z ∈ x → z ∈ y.

Proof. 1: It is easy to show with a simultaneous induction that, for all (p, I) and σ, (p, I) ⊩ σ =_{M} σ, and, for all ⟨σ_{j}, (p_{j}, I_{j})⟩ ∈ σ compatible with (p, I), (p ∪ p_{j}, I ∩ I_{j}) ⊩ σ_{i} ∈_{M} σ.

2: Trivial because the definition of (p, I) ⊩ σ =_{M} τ is itself symmetric.

3: For this and the subsequent parts, we need some lemmas.

Lemma 3.8 If (p’, I’) ≤ (p, I) ⊩ σ =_{M} τ then (p’, I’) ⊩ σ =_{M} τ, and similarly for ∈_{M}.

Proof. By induction on σ and τ. □

Lemma 3.9 If (p, I) ⊩ ρ =_{M} σ and (p, I) ⊩ σ =_{M} τ then (p, I) ⊩ ρ =_{M} τ.

Proof. Again, by induction on terms. □

Returning to proving property 3, the hypothesis is that for some (p, I) and (q, J) each compatible with r, (p, I) ⊩ ρ =_{M} σ and (q, J) ⊩ σ =_{M} τ. By the first lemma, (p ∪ q, I ∩ J) ⊩ ρ =_{M} σ, σ =_{M} τ, and so by the second, (p ∪ q, I ∩ J) ⊩ ρ =_{M} τ. Also, (p ∪ q, I ∩ J) is compatible with r.

4: Let (p, I) ⊩ ρ =_{M} σ and (q, J) ⊩ ρ ∈_{M} τ. We will show that (p ∪ q, I ∩ J) ⊩ σ ∈_{M} τ. Let C be a cover of (q, J) witnessing (q, J) ⊩ ρ ∈_{M} τ. We will show that (p ∪ q, I ∩ J) ∧ C = (p, I) ∧ C is a cover of (p ∪ q, I ∩ J) witnessing (p ∪ q, I ∩ J) ⊩ σ ∈_{M} τ. Let (q_{i}, J_{i}) ∈ C and ⟨τ_{k}, p_{k}, I_{k}⟩ be the corresponding member of τ. By the first lemma, (p ∪ q_{i}, I ∩ J_{i}) ⊩ ρ =_{M} σ, and so by the second, (p ∪ q_{i}, I ∩ J_{i}) ⊩ σ =_{M} τ_{k}.

5: Similar, and left to the reader. □

With this lemma in hand, we can now mod out by =_{M}, so that the symbol “=” is interpreted as actual set-theoretic equality. We will henceforth drop the subscript M from = and ∈, although we will not distinguish notationally between a term σ and the model element it represents, σ’s equivalence class.

At this point, we need to finish specifying the model in detail. What remains to be done is to associate a Cauchy sequence to each node. At the bottom level, assign each Cauchy sequence from M_{0} to exactly one node. Inductively, suppose we chose have the sequence r at a node with ground model M_{n}. There are continuum-in-the-sense-of-M_{n+1}-many immediate successor nodes. Associate each possible candidate r’ in M_{n+1} with exactly one such node. (As a reminder, that means each member of rng(r’\r) is infinitely close to lim(r).)

By way of notation, a node will be named by its associated sequence. Hence “r ⊧ ϕ” means ϕ holds at the node with sequence r.

Note that, at any node of level n, the choice of r’s from that node on is definable in M_{n}. This means that the evaluation of terms (at and beyond the given node) can be carried out over M_{n}, and so the Kripke model (from the given node on) can be defined over M_{n}, truth predicate and all.

3.2 The Forcing Relation

Which (p, I)’s count as true determines the interpretation of all terms, and hence of truth in the end model. We need to get a handle on this. As with forcing, we need a relation (p, I) ⊩ ϕ which supports a truth lemma. Note that, by elementarity, it doesn’t matter in which classical model M_{n} or at what node in the ground Kripke model ⊩ is being interpreted (as long as the parameters are in the interpreting model, of course).

Definition 3.10 (p, I) ⊩ ϕ is defined inductively on ϕ:

(p, I) ⊩ σ =_{M} τ iff for all ⟨σ_{j}, (p_{j}, I_{j})⟩ ∈ σ compatible with (p, I) (p∪p_{j}, I ∩I_{j}) ⊩ σ_{j} ∈_{M} τ and vice versa

(p, I) ⊩ σ ∈_{M} τ iff there is a cover C of (p, I) such that for all (p_{j}, I_{j}) ∈ C there is a ⟨τ_{k}, (p_{k}, I_{k})⟩ ∈ τ such that (p_{j}, I_{j}) ≤ (p_{k}, I_{k}) and (p_{j}, I_{j}) ⊩ σ =_{M} τ_{k}.

(p, I) ⊩ ϕ ∧ ψ iff (p, I) ⊩ ϕ and (p, I) ⊩ ψ

(p, I) ⊩ ϕ ∨ ψ iff there is a cover C of (p, I) such that, for each (p_{j}, I_{j}) ∈ C, (p_{j}, I_{j}) ⊩ ϕ or (p_{j}, I_{j}) ⊩ ψ

(p, I) ⊩ ϕ → ψ iff for all (q, J) ≤ (p, I) if (q, J) ⊩ ϕ then (q, J) ⊩ ψ (p, I) ⊩ ∃x ϕ(x) iff there is a cover C of (p, I) such that, for each (p_{j}, I_{j}) ∈ C,

there is a σ such that (p_{j}, I_{j}) ⊩ ϕ(σ)

(p, I) ⊩ ∀x ϕ(x) iff for all σ (p, I) ⊩ ϕ(σ)

Lemma 3.11 (i) If (q, J) ≤ (p, I) ⊩ ϕ then (q, J) ⊩ ϕ. (ii) If C covers (p, I), and (p_{j}, I_{j}) ⊩ ϕ for all (p_{j}, I_{j}) ∈ C, then (p, I) ⊩ ϕ. (iii) (p, I) ⊩ ϕ iff for all r compatible with (p, I) there is a (q, J) compatible with r

such that (q, J) ⊩ ϕ. (iv) Truth Lemma: For any node r, r ⊧ ϕ iff (p, I) ⊩ ϕ for some (p, I) compatible

with r.

Proof. 1. A trivial induction, using of course the earlier lemmas about ≤ and covers.

2. Easy induction. The one case to watch out for is →, where you need to invoke the previous part of this lemma.

3. Trivial, using 2.

4. By induction on ϕ, in detail for a change.

In all cases, the right-to-left direction (“forced implies true”) is pretty easy, by induction. (Note that only the → case needs the left-to-right direction in this induction.) Hence in the following we show only left-to-right (“if true at a node then forced”).

=: This is exactly the definition of =.

∈: This is exactly the definition of ∈.

∧: If r ⊧ ϕ ∧ ψ, then r ⊧ ϕ and r ⊧ ψ. Inductively let (p, I) ⊩ ϕ and (q, J) ⊩ ψ, where (p, I) and (q, J) are each compatible with r. That means that (p, I) and (q, J) are compatible with each other, and (p ∪ q, I ∩ J) suffices.

∨: If r ⊧ ϕ∨ψ, then WLOG r ⊧ ϕ . Inductively let (p, I) ⊩ ϕ, (p, I) compatible with r. {(p, I)} suffices.

→: Suppose to the contrary r ⊧ ϕ → ψ but no (p, I) compatible with r forces such. Work in the node f(r). (Recall that f is the universal symbol for the various transition functions in sight. What we mean more specifically is that if r ∈ M_{n}, i.e. if r is a node from level n, then f(r) is the image of r in M_{n+1}, i.e. in the Kripke structure on level n+1.) Let (p, I) be compatible with f(r) and p have non-standard (in the sense of M_{n}) length (equivalently, I has infinitesimal length). Since (p, I) ⊮ ϕ → ψ there is a (q, J) ≤ (p, I) such that (q, J) ⊩ ϕ but (q, J) ⊮ ψ. By the previous part of this lemma, there is an r’ compatible with (q, J) such that no condition compatible with r’ forces ψ. At the node r’, by induction, r’ |̸= ψ, even though r’ ⊧ ϕ (since r’ is compatible with (p, I) ⊩ ϕ). This contradicts the assumption on r (i.e. that r ⊧ ϕ → ψ), since r’ extends r (as nodes).

∃: If r ⊧ ∃x ϕ(x) then let σ be such that r ⊧ ϕ(σ). Inductively there is a (p, I) compatible with r such that (p, I) ⊩ ϕ(σ). {(p, I)} suffices.

∀: Suppose to the contrary r ⊧ ∀x ϕ(x) but no (p, I) compatible with r forces such. As with →, let (p, I) non-standard be compatible with f(r). Since (p, I) ⊮ ∀x ϕ(x) there is a σ such that (p, I) ⊮ ϕ(σ). By the previous part of this lemma, there is an r’ compatible with (p, I) such that, for all (q, J) compatible with r’, (q, J) ⊮ ϕ(σ). By induction, that means that r’ |̸= ϕ(σ). This contradicts the assumption on r (i.e. that r ⊧ ∀x ϕ(x)), since r’ extends r (as nodes).

□

3.3 The Final Proofs

Using ⊩, we can now prove

Theorem 3.12 This Kripke model satisfies IZF_{Ref}.

Proof. Note that, as a Kripke model, the axioms of intuitionistic logic are satisfied, by general theorems about Kripke models.

• Empty Set: The interpretation of the term ∅ will do.

• Infinity: The canonical name for ω will do. (Recall that the canonical name x̄ of any set x ∈ V is defined inductively as {⟨ȳ, (∅, R)⟩ | y ∈ x}.)

• Pairing: Given σ and τ, {⟨σ, (∅, R)⟩, ⟨τ, (∅, R)⟩} will do.

• Union: Given σ, {⟨τ, J ∩ J_{i}⟩ | for some σ_{i}, ⟨τ, J⟩ ∈ σ_{i} and ⟨σ_{i}, J_{i}⟩ ∈ σ} will do.

• Extensionality: We need to show that ∀x ∀y [∀z (z ∈ x ↔ z ∈ y) → x = y]. So let σ and τ be any terms at a node r such that r ⊧ “∀z (z ∈ σ ↔ z ∈ τ)”. We must show that r ⊧ “σ = τ”. By the Truth Lemma, let r ∈ J ⊩ “∀z (z ∈ σ ↔ z ∈ τ)”; i.e. for all r’ ∈ J, ρ there is a J’ containing r’ such that J ∩ J’ ⊩ ρ ∈ σ ↔ ρ ∈ τ. We claim that J ⊩ “σ = τ”, which again by the Truth Lemma suffices. To this end, let ⟨σ_{i}, J_{i}⟩ be in σ; we need to show that J ∩ J_{i} ⊩ σ_{i} ∈ τ. Let r’ be an arbitrary member of J ∩ J_{i} and ρ be σ_{i}. By the choice of J, let J’ containing r’ be such that J ∩ J’ ⊩ σ_{i} ∈ σ ↔ σ_{i} ∈ τ; in particular, J ∩ J’ ⊩ σ_{i} ∈ σ → σ_{i} ∈ τ. It has already been observed in 3.7, part 1, that J ∩ J’ ∩ J_{i} ⊩ σ_{i} ∈ σ, so J ∩ J’ ∩ J_{i} ⊩ σ_{i} ∈ τ. By going through each r’ in J ∩ J_{i} and using 3.11, part 3, we can conclude that J ∩ J_{i} ⊩ σ_{i} ∈ τ, as desired. The other direction (“τ ⊆ σ”) is analogous.

• Set Induction (Schema): Suppose r ⊧ “∀x ((∀y ∈ x ϕ(y)) → ϕ(x))”; by the Truth Lemma, let J containing r force as much. We must show r ⊧ “∀x ϕ(x)”. Suppose not. Using the definition of satisfaction in Kripke models, there is an r’ extending (i.e. infinitesimally close to) r (hence in J) and a σ such that r’ |̸= ϕ(σ). By elementarity, there is such an r’ in M_{n}, where n is the level of r. Let σ be such a term of minimal V-rank among all r’s ∈ J. Fix such an r’. By the Truth Lemma (and the choice of J), r’ ⊧ “(∀y ∈ σ ϕ(y)) → ϕ(σ)”. We claim that r’ ⊧ “∀y ∈ σ ϕ(y)”. If not, then for some r” extending r’ (hence in J) and τ, r” ⊧ τ ∈ σ and r” |̸= ϕ(τ). Unraveling the interpretation of ∈, this choice of τ can be substituted by a term τ of lower V-rank than σ. By elementarity, such a τ would exist in M_{n}, in violation of the choice of σ, which proves the claim. Hence r’ ⊧ ϕ(σ), again violating the choice of σ. This contradiction shows that r ⊧ “∀x ϕ(x)”.

• Separation (Schema): Let ϕ(x) be a formula and σ a term. Then {⟨σ_{i}, J ∩ J_{i}⟩ | ⟨σ_{i}, J_{i}⟩ ∈ σ and J ⊩ ϕ(σ_{i})} will do.

• Power Set: A term σ̂ is a canonical subset of σ if for all ⟨σ_{i}, Ĵ_{i}⟩ ∈ σ̂ there is a J_{i} ⊇ Ĵ_{i} such that ⟨σ_{i}, J_{i}⟩ ∈ σ. {⟨σ̂, (∅, R)⟩ | σ̂ is a canonical subset of σ} is a set (in M_{n}), and will do.

• Reflection (Schema): Recall that the statement of Reflection is that for every formula ϕ(x) (with free variable x and unmentioned parameters) and set z there is a transitive set Z containing z such that Z reflects the truth of ϕ(x) in V for all x ∈ Z. So to this end, let ϕ(x) be a formula and σ be a set at a node r of level n (in the tree which is this Kripke model’s partial order). Let k be such that the truth of ϕ(x) at node r and beyond is Σ_{k} definable in M_{n}. In M_{n}, let X be a set containing σ, r, and ϕ’s parameters such that X ≺_{k} M_{n}. Let τ be {⟨ρ, (∅, R)⟩ | ρ ∈ X is a term}. τ will do.

□

We are interested in the canonical term {⟨p̄, (p, I)⟩ | p is a finite function from N to Q and I is a non-empty, open interval from the reals with rational endpoints}, where p̄ is the canonical name for p. We will call this term Z. Note that at node r Z gets interpreted as r.

Proposition 3.13 For all nodes r, r ⊧ “Z is a Cauchy sequence”.

Proof. To see that ⊥ ⊧ “Z is total”, suppose r ⊧ “N is an integer”. Then (⟨N, r(N)⟩, R) is compatible with r and forces “Z(N) = r(N)”. That Z is a function is similarly easy.

As for Z being Cauchy, again let r ⊧ “N is an integer”. Since r is Cauchy, there is an integer M such that beyond M r stays within an interval I of size 1/(2N). Of course, future nodes might be indexed by Cauchy sequences s extending r that go outside of I, but only by an infinitesimal amount. So let J extend I on either side and still have length less that 1/N. Then (r↾M, J) is compatible with r, and forces that Z beyond M stay in J, making Z “Cauchy for 1/N”, to coin a phrase. □

In order to complete the theorem, we need only prove the following

Proposition 3.14 For all nodes r, r ⊧ “Z has no modulus of convergence.”

Proof. Suppose r ⊧ “f is a modulus of convergence for Z.” Let (p, I) compatible with r force as much. WLOG I is a finite interval. Let n be such that 1/n is less than the length of I, and let ϵ be (length(I) - 1/n)/2.

Let (q, J) ≤ (p, I) force a value m for f(n). WLOG length(q) > m, as q could be so extended. If J=I, then (q, J) could be extended simply by extending q with two values a distance greater than 1/n apart, thereby forcing f not to be a modulus of convergence. So J ⊂ I. That means either inf J > inf I or sup J < sup I. WLOG assume the latter. Let mid J be the midpoint of J, q_{0} be q extended by mid J, and J_{0} be (mid J, sup J). Then (q_{0}, J_{0}) ≤ (q, J), and therefore (q_{0}, J_{0}) ⊩ f(n) = m.

What (q_{1}, J_{1}) is depends:

CASE I: There is an open set K containing sup(J_{0}) such that (q_{0}, K) ⊩ f(n) = m. Then let j_{max} be the sup of the right-hand endpoints (i.e. sups) of all such K’s. Let q_{1} be q_{0} extended by sup J_{0}.

\underline{Claim}: (q_{1}, (sup J_{0}, j_{max})) ⊩ f(n) = m.

Proof. Let r be any Cauchy sequence compatible with (q_{1}, (sup J_{0}, j_{max})). Since lim r < j_{max}, r (that is, rng(r\q_{0})) is actually bounded below j_{max}. By the definition of j_{max}, there is an open K containing sup J_{0} such that r is bounded by sup K. As r is bounded below by sup J_{0}, r (again, rng(r\q_{0})) is contained within K. As (q_{0}, K) ⊩ f(n) = m, r ⊧ f(n) = m. □

Of course, J_{1} will be (sup J_{0}, j_{max}).

CASE II: Not Case I. Then extend by the midpoint again. That is, q_{1} is q_{0} extended by mid J_{0}, and J_{1} is (mid J_{0}, sup J_{0}). Also in this case, (q_{1}, J_{1}) ⊩ f(n) = m.

Clearly we would like to continue this construction. The only thing that might be a problem is if the right-hand endpoint of some J_{k} equals (or goes beyond!) sup I, as we need to stay beneath (p, I). In fact, as soon as sup(J_{k}) > sup(I) - ϵ (if ever), extend q_{k} by something within ϵ of sup I, and continue the construction with left and right reversed. That is, instead of going right, we now go left. This is called “turning around”.

What happens next depends.

CASE A: We turned around, and after finitely many more steps, some J_{k} has its inf within inf(I) + ϵ. Then extend q_{k} by something within ϵ of inf I. This explicitly blows f being a modulus of convergence for Z.

CASE B: Not Case A. So past a certain point (either the stage at which we turned around, or, if none, from the beginning) we’re marching monotonically toward one of I’s endpoints, but will always stay at least ϵ away. WLOG suppose we didn’t turn around. Then the construction will continue for infinitely many stages. The q_{k}’s so produced will in the limit be a (monotonic and bounded, hence) Cauchy sequence r. Furthermore, lim r is the limit of the sup(J_{k})’s. Finally, r is compatible with (p, I). Hence r ⊧ “f is total”, and so r ⊧ f(n) = m’, for some m’. Let some condition compatible with r force as much. This condition will have the form (q’, K), where lim r ∈ K. Let k be such that sup(J_{k}) ∈ K, and q_{k} ⊇ q’. Consider (q_{k}, J_{k}). Note that (q_{k}, J_{k} ∩ K) extends both (q_{k}, J_{k}) and (q’, K), hence forces both f(n) = m and f(n) = m’, which means that m=m’.

Therefore, at this stage in the construction, we are in Case I. By the construction, J_{k+1} = (sup J_{k}, j_{max}), where j_{max} ≥ sup K > lim r = lim_{k} (sup(J_{k})) ≥ sup(J_{k+1}) = j_{max}, a contradiction. □

4 Not every Cauchy sequence of Cauchy sequences converges

Theorem 4.1 IZF_{Ref} does not prove that every Cauchy sequence of Cauchy sequences converges to a Cauchy sequence.

The statement of the theorem itself needs some elaboration. The distance d(x_{0n}, x_{1n}) between two Cauchy sequences x_{0n} and x_{1n} is the sequence | x_{0n} −x_{1n} |. x_{0n} < x_{1n} if there are m, N ∈ N such that for all k > N x_{0k} + 1/m < x_{1k}. A rational number r can be identified with the constant Cauchy sequence x_{n} = r. x_{n} = 0 if ∀m ∃N ∀k > N | x_{k} |< 1/m. x_{0n} and x_{1n} are equal (as reals, equivalent as Cauchy sequences if you will) if d(x_{0n}, x_{1n}) = 0. With these definitions in place, we can talk about Cauchy sequences of Cauchy sequences, and limits of such. The theorem is then that it is consistent with IZF_{Ref} to have a convergent sequences of Cauchy sequences with no limit.

Note that we are not talking about reals! A real number would be an equivalence class of Cauchy sequences (omitting, for the moment, considerations of moduli of convergence). It would be weaker to claim that the sequence of reals represented by the constructed sequence of sequences has no limit. After all, given a sequence of reals, it’s not clear that there is a way to choose a Cauchy sequence from each real. We are claiming here that even if your task is made easier by being handed a Cauchy sequence from each real, it may still not be possible to get a “diagonalizing”, i.e. limit, Cauchy sequence.

4.1 The Topological Space and Model

Let T be the space of Cauchy sequences of Cauchy sequences. By way of notation, if X is a member of T, then X_{j} will be the j^{th} Cauchy sequence in X; as a Cauchy sequence of rationals, X_{j} will have values X_{j}(0), X_{j}(1), etc. Still notationally, if X_{n} ∈ T, then the j^{th} sequence in X_{n} is X_{nj}. In the classical meta-universe, the Cauchy sequence X_{j} has a limit, lim(X_{j}); in addition, the sequence X has a limit, which will be written as lim(X).

A basic open set p is given by a finite sequence ⟨(p_{j}, I_{j}) | j < n_{p}⟩ of basic open sets from the space of the previous theorem (i.e. p_{j} is a finite sequence of rationals and I_{j} is an open interval), plus an open interval I_{p}. X ∈ p if X_{j} ∈ (p_{j}, I_{j}) for each j<n_{p}, if lim(X_{j}) ∈ I_{p} for each j≥n_{p}, and lim(X) ∈ I. Note that q ⊆ p (q \underline{extends} p) if n_{q} ≥ n_{p}, (q_{j}, K_{j}) ⊆ (p_{j}, I_{j}) for j < n_{p}, K_{j} ⊆ I_{p} for j ≥ n_{p}, and I_{q} ⊆ I_{p}.

p and q are compatible (where WLOG n_{p} ≤ n_{q}) if, for j < n_{p} (p_{j}, I_{j}) and (q_{j}, K_{j}) are compatible, for n_{p} ≤ j < n_{q} K_{j}∩ I_{p} ≠ ∅, and I_{q}∩ I_{p} ≠ ∅. In this case, p ∩ q is not the basic open set you’d think it is, but rather a union of such. The problem is that for n_{p} ≤ j < n_{q} it would be too much to take the j^{th} component to be (q_{j}, K_{j}∩ I_{p}), because that would leave out all extensions of q_{j} with entries from K_{j}\I_{p} before they finally settle down to K_{j}∩ I_{p}. So p ∩ q will instead be covered by basic open sets in which the j^{th} component will be (r_{j}, K_{j}∩ I_{p}), where (r_{j}, K_{j}) ⊆ (q_{j}, K_{j}). (So the given basic open sets form not a basis for the topology, but rather a sub-basis.)

As always, the sets in the induced Heyting-valued model M are of the form {⟨σ_{k}, p_{k}⟩ | k ∈ K}, where K is some index set, each σ_{k} is a set inductively, and each p_{k} is an open set. Note that all sets from the ground model have canonical names, by choosing each p_{k} to be T (i.e. n_{p} = 0 and I_{p} = R), hereditarily. M satisfies IZF_{Ref}.

4.2 The Extensions ≤_{j} and ≤_{∞}

In the final proof, we will need the following notions.

Definition 4.2 \underline{j-extension} ≤_{j}: q ≤_{j} p for some j < n_{p} if q and p satisfy all of the clauses of q extending p except possibly for the condition on the j^{th} component: (q_{j}, K_{j}) need not be a subset of (p_{j}, I_{j}), although we will still insist that (q_{j}, I_{j}) be a subset of (p_{j}, I_{j}).

More concretely, q_{j} comes from p_{j} by extending with elements from I_{j}; it’s just that we’re no longer promising to keep to I_{j} in the future. Notice that ≤_{j} is not transitive; the transitive closure of ≤_{j} will be notated as ≤_{j}^{∗}.

Definition 4.3 \underline{∞-extension} ≤_{∞}: q ≤_{∞} p if q and p satisfy all of the clauses of q extending p except possibly for the last, meaning that I_{q} need not be a subset of I_{p}.

≤_{∞}^{∗} is the transitive closure of ≤_{∞}.

Lemma 4.4 Suppose q ⊆ p, q ⊆ ∥f(n)=m∥ for some particular m and n, and j < n_{p}. Then for all x ∈ I_{j} there is an r ⊆ p, r ≤_{j}^{∗} q such that r ⊆ ∥f(n)=m∥ and x ∈ L_{j}, where (r_{j}, L_{j}) is r’s j^{th} component.

Proof. If x ∈ K_{j}, then we are done: let r be q. So assume WLOG that x ≥ sup(K_{j}). The inspiration for this construction is the construction of the previous theorem. The main difference is that not only do we have (q_{j}, K_{j}) to contend with, we also have all of q’s other components around. Hence the notion of a j-extension: we will do the last theorem’s construction on the j^{th} coordinates, and leave all the others alone.

First off, we would like to show that q has a j-extension q’ ⊆ p also forcing f(n) = m such that sup(K_{j}) ∈ K’_{j}. Toward this end, let X ∈ T be a member of (the open set determined by) q except that lim(X_{j}) = sup(K_{j}). X is in p, so there is some r ⊆ p such that X ∈ r and r forces a value for f(n), say m’. q and r are compatible though: apart from the j^{th} component, X is in both, and the only thing happening in the j^{th} component is that, in r, sup(K_{j}) ∈ L_{j}, meaning that K_{j} and L_{j} overlap. So any common extension of both q and r would have to force f(n)=m and f(n)=m’; since p already forces that f is a function, m=m’. Using r, it is easy to construct the desired q’: take the j^{th} component from r, and let each other component be the intersection of the corresponding components from r and q.

If there is such a q’ such that x ∈ K’_{j}, then we are done. Else we would like to mimic the last theorem’s construction by having in our next condition the interval part of the j^{th} component be (sup(K_{j}), j_{max}) (for a suitably defined j_{max}). The problem is, q has all these other components around. For any real y < j_{max} we could find a j-extension of q with (sup(K_{j}), y) in the j^{th} component, but not necessarily for y = j_{max} itself.

To this end, consider all such q’ as above. Each q’ can be extended (to say q”) by restricting the interval in the j^{th} component to (sup(K_{j}), sup(K’_{j})). Let q_{1} be such a q” where that interval is at least half as big as possible (i.e. among all such q”, where of course sup(K’_{j}) has to be bounded by sup(I_{j})).

Continue this construction so that q_{n} is defined from q_{n−1} just as q_{1} was defined from q. WLOG dovetail this construction with extending all other components so that after infinitely many steps we would have produced an X ∈ T. (This remark needs a word of justification about the j^{th} components. By the definition of jextension alone, it is not clear that a sequence of j-extending conditions q_{0} ≥_{j} q_{1} ≥_{j} ... converges to a point in T. In our case, though, by the construction itself, the various K_{nj}’s are monotonically increasing and bounded, hence the X_{j} so determined is Cauchy.)

If at some finite stage we have covered x, then we are done. If not, then sup(X_{j}) = sup_{n}(sup(K_{nj})) ≤ x ∈ I_{j}, so that X ∈ p. So there is some r ⊆ p with X ∈ r such that r forces a value for f(n), say m’. Let ϵ be sup(L_{j}) - sup(X_{j}). Eventually in the construction, K_{nj} will be contained within ϵ of sup(X_{j}). With r as the witness, at the next stage K_{(n+1)j} would go beyond sup(X_{j}), which is a contradiction. Hence this case is not possible, and at some finite stage we must have covered x, as desired.

□

We have a similar lemma for ∞-extensions.

Lemma 4.5 Suppose q ⊆ p and q ⊆ ∥f(n)=m∥ for some particular m and n. Then for all x ∈ I_{p} there is an r ⊆ p, r ≤_{∞}^{∗} q such that r ⊆ ∥f(n)=m∥ and x ∈ I_{r}.

Proof. Similar to the above. □

Observe that the same arguments work for preserving finitely many values of f simultaneously.

4.3 The Final Proof

We are interested in the canonical term {⟨p̄_{j}, p⟩ | p is an open set}, where p̄_{j} is the canonical name for the sequence ⟨p_{j} | j < n_{p}⟩ from p. We will call this term Z. It should be clear that T = ∥Z is a Cauchy sequence of Cauchy sequences∥. Hence we need only prove

Proposition 4.6 T = ∥Z does not have a limit∥.

Proof. Suppose p ⊆ ∥f is a Cauchy sequence∥. It suffices to show that for some q ⊆ p, q ⊆ ∥f ≠ lim(Z)∥.

If p can ever be extended to force infinitely many values for f simultaneously, then do so, and further extend (it suffices here to extend merely the last component) to force Z away from f’s limit. This suffices for the theorem.

If this is not possible, then the construction will be to build one or two sequences of open sets, p_{k} and possibly r_{k}, indexed by natural numbers k. It is to be understood even though not again mentioned that the construction below is to be dovetailed with a countable sequence of moves designed to produce a single member of T in the end (i.e. each individual component must shrink to a real as in the previous theorem, the n_{p_{k}}’s must be unbounded as k goes through N, and the last components I_{p_{k}} must shrink to something of length 0).

First, let p_{0} be built by extending p by cutting I_{p} to its bottom third, and let L be some point in I_{p}’s top half. If p_{0} can be extended (to p_{1}) so that f is forced to have an additional value (that is, beyond what has already been forced) in I_{p}’s top half, then do so. Else proceed as follows. First extend p_{0} to force an additional value for f, necessarily in I_{p}’s bottom half. Then by the second lemma above, ∞-extend that latter condition, to q say, preserving the finitely many values of f already determined, and getting L into I_{q}. Typically n_{q} > n_{p}, so let q̄ be such that nq̄ = n_{q}, if j < n_{p} then q̄’s j^{th} component is the same as p’s, if n_{p} ≤ j < n_{q} then q̄’s j^{th} component is (∅, I_{p}), and Iq̄ = I_{p}. Note that q ⊆ q̄ ⊆ p, so we can apply the first lemma above to q and q̄. Starting from q, iteratively on j from n_{p} up to n_{q}, j-extend to get L into the interval part of the j^{th} component, while preserving the finitely many values of f already determined. Call the last condition so obtained r_{0}. Finally, ∞-extend r_{0} to get the last component to be a subset of I_{p_{0}}, while still preserving f of course. Let this latter condition be p_{1}.

Stages k > 0 will be similar. To start, if possible, extend p_{k} to force an additional value for f in I_{p}’s top half. Call this condition p_{k+1}.

If that is not possible, first extend p_{k} to force a new value for f, necessarily in I_{p}’s bottom half. Then ∞-extend (to q say) to get L into the last component I_{q}. After that, j-extend for each j from n_{r_{i}} to n_{q} to get L in those components, where i is the greatest integer less than k such that r_{i} is defined. (It bears mentioning that r_{h} is defined if and only if at stage h we are in this case.) If need be, shrink those components to be subsets of I_{r_{i}}, for the purpose of getting r_{k} ⊆ r_{i} (once we define r_{k}). That last condition will be r_{k}. Next, ∞-extend r_{k} to get the last component to be a subset I_{p_{k}}. This final condition is p_{k+1}.

This completes the construction.

If the second option happens only finitely often, let k be greater than the last stage where it happens. Then not only does p_{k} force lim(Z) to be in I_{p}’s bottom third, as all p_{i}’s do actually, but also p_{k} is respected in the rest of the construction: for i > k, p_{i} ⊆ p_{k}. Let l ≥ k be such that 6/l < length(I_{p}) (i.e. the distance between I_{p}’s top half and bottom third is greater than 1/l). Recall that p ⊆ ∥f is a Cauchy sequence∥; that is, p ⊆ ∥∀ϵ > 0 ∃N ∀m, n ≥ N |f(m) − f(n)| < ϵ∥. Since 1/l > 0, p ⊆ ∥∃N ∀m, n ≥ N |f(m) − f(n)| < 1/l∥. That means there is a cover C of p such that each q ∈ C forces a particular value for N. Let S be ⋂_{j≥k}p_{j}, and let q ∈ C contain S. Similarly, let q̂ containing S force a value for f(N). q ∧q̂∧ p_{k} is non-empty because it contains S, and q ∧q̂∧ p_{k} forces by the construction that f(N) is in I_{p}’s top half, by the choice of q that lim(f) is away from I_{p}’s bottom third, and by choice of k that lim(Z) is in I_{p}’s bottom third. In short, q ∧q̂∧ p_{k} ⊆ ∥f ≠ lim(Z)∥.

Otherwise the second option happens infinitely often. Then we have an infinite descending sequence of open sets r_{k}, and a similar argument works. Let S be ⋂_{j} r_{j}, where the intersection is taken only over those j’s for which r_{j} is defined. Let k be such that r_{k} ⊆ ∥lim(Z) - midpoint(I_{p}) < ϵ∥, for some fixed ϵ > 0. Let q containing S be such that, for a fixed value of N, q ⊆ ∥∀m, n ≥ N |f(m) − f(n)| < ϵ∥. Let q̂ force a particular value for f(N), necessarily in I_{p}’s bottom half. Again, q ∧q̂∧ p_{k} ⊆ ∥f ≠ lim(Z)∥.

□

5 The given Cauchy sequence has a modulus, but the limit doesn’t

Theorem 5.1 IZF_{Ref} does not prove that every Cauchy sequence with a modulus of convergence of Cauchy sequences converges to a Cauchy sequence with a modulus of convergence.

Definition 5.2 c is a convergence function for a Cauchy sequence ⟨X_{j} | j ∈ N⟩ if c is a decreasing sequence of positive rationals; for all n, if j, k ≥ n then | X_{j} − X_{k} |≤ c(n); and lim(c(n)) = 0.

Notice that convergence functions and moduli of convergence are easily convertible to each other: if c is the former, then d(n) := the least m such that c(m) ≤ 2^{−n} is the latter; and if d is the latter, then c(n) := 2^{−m}, where m is the greatest integer such that max(m, d(m)) ≤ n, is the former. Therefore the current construction will be of a Cauchy sequence ⟨X_{j} | j ∈ N⟩ with a convergence function but no limit. Without loss of generality, the convergence function in question can be taken to be c(n) = 2^{−n}.

Let the topological space T be {⟨X_{j} | j ∈ N⟩ | ⟨X_{j} | j ∈ N⟩ is a Cauchy sequence of Cauchy sequences with convergence function 2^{−n} }. As in the previous section, for X ∈ T, X_{j} will be the j^{th} Cauchy sequence in X’s first component. The real number represented by X_{j}, i.e. X_{j}’s limit, will be written as lim(X_{j}). In the classical meta-universe, the limit of the sequence ⟨X_{j} | j ∈ N⟩ will be written as lim(X).

T is a subset of the space from the previous section, and the topology of T is to be the subspace topology. That is, a basic open set p is given again by a finite sequence ⟨(p_{j}, I_{j}) | j < n_{p}⟩ and an open interval I_{p}. X ∈ p if, again, X_{j} ∈ (p_{j}, I_{j}) for each j<n_{p}, lim(X_{j}) ∈ I_{p} for each j≥n_{p}, and lim(X) ∈ I_{p}. p and q are compatible under the same conditions as before, and p ∩ q is covered by basic open sets, just as in the last theorem; the convergence function causes no extra trouble.

Note that q ⊆ p (q \underline{extends} p) if all of the same conditions from the last section hold: n_{q} ≥ n_{p}, (q_{j}, K_{j}) ⊆ (p_{j}, I_{j}) for j < n_{p}, K_{j} ⊆ I_{p} for j ≥ n_{p}, and I_{q} ⊆ I_{p}.

In the following, we will need to deal with basic open sets in canonical form. The issue is the following. Suppose, in p, I_{0} = (0, 1) and I_{1} = (0, 10). Then X_{1} could certainly contain elements from (0, 10). However, when it comes to taking limits, X_{1} has 2 as an upper bound, because of I_{0} and the convergence function 2^{−n}, but this is not reflected in I_{1}.

Definition 5.3 p is in canonical form if, for j < k < n_{p}, |sup(I_{j}) - sup(I_{k}) |≤ 2^{−j}, and also |sup(I_{j}) - sup(I_{p}) |≤ 2^{−j}.

The value of canonical form is that, if for j < n_{p} lim(X_{j}) = sup(I_{j}) and if lim(X) = sup(I_{p}), then, although X ∉ p, X could still be in T.

Proposition 5.4 Every open set is covered by open sets in canonical form.

Proof. Let X ∈ p open. If, in q ⊆ p, J_{k} is an interval with midpoint lim(X_{k}) and radius independent of k, and I_{q} an interval with midpoint lim(X) and the same radius, then q will be canonical. We will construct such a q containing X.

By way of choosing the appropriate radius, as well as n_{q}, let δ be half the distance from lim(X) to the closer of I_{p}’s endpoints. Let N ≥ n_{p} be such that for all k ≥ N lim(X_{k}) is within δ of lim(X). Let r ≤ δ be such that for all k < N (lim(X_{k}) - r, lim(X_{k}) + r) ⊆ I_{k}. Let n_{q} ≥ N be such that for all k ≥ n_{q} lim(X_{k}) is within r of lim(X). For k < n_{q} let J_{k} be the neighborhood with center lim(X_{k}) and radius r, and let q_{k} be an initial segment of X_{k} long enough so that beyond it X_{k} stays within J_{k}. Let I_{q} be the neighborhood with center lim(X) and radius r. This q suffices. □

As always, the sets in the induced Heyting-valued model M are of the form {⟨σ_{k}, p_{k}⟩ | k ∈ K}, where K is some index set, each σ_{k} is a set inductively, and each p_{k} is an open set. Note that all sets from the ground model have canonical names, by choosing each p_{k} to be T (i.e. n_{p} = 0 and I_{p} = R), hereditarily. M satisfies IZF_{Ref}.

We are interested in the canonical term {⟨p̄_{j}, p⟩ | p is an open set}, where p̄_{j} is the canonical name for the sequences ⟨p_{j} | j < n_{p}⟩ from p. We will call this term Z. It should be clear that T = ∥Z is a Cauchy sequence of Cauchy sequences with convergence function 2^{−n}∥. Hence we need only prove

Proposition 5.5 T = ∥No Cauchy sequence equal to lim(Z) has a modulus of convergence∥.

Proof. Suppose p ⊆ ∥f is a modulus of convergence for a Cauchy sequence g∥, p in canonical form. It suffices to show that for some q ⊆ p, q ⊆ ∥g ≠ lim(Z)∥.

Let ϵ < (length I_{p})/2. Let q ⊆ p in canonical form force “f(ϵ) = N”; WLOG n_{q} > N. We can also assume (by extending again if necessary) that q forces a value for g(N); WLOG g(N) ≤ midpoint(I_{p}). Let X ∈ p be on the boundary of q; that is, X_{k} extends q_{k} (k < n_{q}), X_{k} beyond length(q_{k}) is a sequence through J_{k} with limit sup(J_{k}), and X beyond n_{q} is a sequence through I_{q} with limit sup(I_{q}) (more precisely, ⟨lim(X_{k}) | k ≥ n_{q}⟩ is such a sequence).

(Technical aside: By the canonicity of q’s form, X ∈ T. But why should X be in p? This could fail only if sup(J_{k}) = sup(I_{k}) or if sup(I_{q}) = sup(I_{p}). The latter case would actually be good. The point of the current argument is to get a condition r (forcing the things q forces) such that I_{r} contains points greater than g(N) + ϵ, which would fall in our lap if sup(I_{q}) = sup(I_{p}). If sup(I_{q}) < sup(I_{p}) and sup(J_{k}) = sup(I_{k}), then X_{k} must be chosen so that lim(X_{k}) is slightly less than this sup. Could this interfere with 2^{−n} being a convergence function for X? No, by the canonicity of p. If l is another index such that sup(J_{l}) = sup(I_{l}), then by letting lim(X_{l}) be shy of this sup by the same amount as for k the convergence function 2^{−n} is respected (for these two indices). If sup(J_{l}) < sup(I_{l}), then what to do depends on whether sup(J_{k}) and sup(J_{l}) are strictly less than 2^{−min(k,l)} apart or exactly that far apart. In the former case, there’s some wiggle room in the k^{th} slot for lim(X_{k}) to be less than sup(J_{k}). In the latter, sup(J_{l}) must be sup(J_{k}) either increased or decreased by 2^{−min(k,l)}. The first option is not possible, by the canonicity of p, as sup(J_{l}) < sup(I_{l}). In the second option, having lim(X_{k}) be less than sup(J_{k}) brings lim(X_{k}) and lim(X_{l}) even closer together. Similar considerations apply to comparing lim(X_{k}) and lim_{k}(X_{k}) = sup(I_{q}).)

Let q_{1} in canonical form containing X force values for f(ϵ) and g(f(ϵ)). Since q_{1} and q are compatible, they force the same such values. WLOG q_{1} is such that sup(I_{q_{1}}) is big (that is, sup(I_{q_{1}}) - sup(I_{q}) is at least half as big as possible). Continuing inductively, define q_{n+1} from q_{n} as q_{1} was defined from q. Continue until I_{q_{n}} contains points greater than g(N) + ϵ. This is guaranteed to happen, because, if not, the infinite sequence q_{n} will converge to a point X in p. Some neighborhood r of X forcing values for f(ϵ) and g(f(ϵ)) will contain some q_{n}, witnessing that q_{n+1} would have been chosen with larger last component than it was, as in the previous proofs.

Once the desired q_{n} is reached, shrink I_{q_{n}} to be strictly above g(N) + ϵ. Call this new condition r. r forces “lim(Z) > g(N) + ϵ”, and r also forces “g ≤ g(N) + ϵ”. So r forces “g ≠ lim(Z)”, as desired. □

6 The reals are not Cauchy complete

Theorem 6.1 IZF_{Ref} does not prove that every Cauchy sequence of reals has a limit.

As stated in the introduction, what we will actually prove will be what seems to be the hardest version: there is a Cauchy sequence, with its own modulus of convergence, of real numbers, with no Cauchy sequence as a limit, even without a modulus of convergence. Other versions are possible, such as changing what does and doesn’t have a modulus. After all of the preceding proofs, and after the following one, it should not be too hard for the reader to achieve any desired tweaking of this version.

Let T consist of all Cauchy sequences of Cauchy sequences, all with a fixed convergence function of 2^{−n}. An open set p is given by a finite sequence ⟨(p_{j}, I_{j}) | j < n_{p}⟩ as well as an interval I_{p}, with the usual meaning to X ∈ p.

Recall from the previous section:

Definition 6.2 p is in canonical form if, for each j < k < n_{p} | sup(I_{j}) - sup (I_{k}) |≤ 2^{−j}. Also, | sup(I_{j}) - sup (I_{p}) |≤ 2^{−j}.

Also from the last section:

Proposition 6.3 Every open set is covered by sets in canonical form.

Henceforth when choosing open sets we will always assume they are in canonical form.

Definition 6.4 p and q are similar, p∼q, if n_{p} = n_{q}, I_{p} = I_{q}, I_{k} = J_{k}, and length(p_{k}) = length(q_{k}). So p and q have the same form, and can differ only and arbitrarily on the rationals chosen for their components.

If moreover p_{k} = q_{k} for each k ∈ J then we say that p and q are J-similar, p∼_{J}q.

If p∼q, this induces a homeomorphism on the topological space T, and therefore on the term structure. (To put it informally, wherever you see p_{k}, or an initial segment or extension thereof, replace it (or the corresponding part) with q_{k}, and vice versa. This applies equally well to members of T, open sets, and (hereditarily) terms.)

Definition 6.5 If p, q, and r are open sets, σ is a term, and q and r are similar, then the image of p under the induced homeomorphism is notated by p_{qr} and that of σ by σ_{qr}.

Lemma 6.6 p ⊩ ϕ(σ⃗) iff p_{qr} ⊩ ϕ(σ⃗_{qr}).

Proof. A straightforward induction. □

Definition 6.7 σ has support J if for all p∼_{J}q ⊥ ⊩ σ = σ_{pq}. σ has finite support if σ has support J for some finite set J.

The final model M is the collection of all terms with hereditarily finite support. As always, let Z be the canonical term. Note that Z is not in the symmetric

submodel! However, each individual member of Z, Z_{j}, is, with support {j}. Also, so is ⟨[Z_{j}] | j ∈ N⟩, which we will call [Z], with support ∅. (Here, for Y a Cauchy sequence, [Y] is the equivalence class of Cauchy sequences with the same limit as Y, i.e. the real number of which Y is a representative.) That’s because no finite change in Z_{j} affects [Z_{j}]. (Notice that even though each member of [Z_{j}] has support {j}, [Z_{j}]’s support is still empty.) It will ultimately be this sequence [Z] that will interest us. But first:

Proposition 6.8 M ⊧ IZF_{Ref}.

Proof. As far as the author is aware, symmetric submodels have been studied only in the context of classical set theory, not intuitionistic, and, moreover, the only topological models in the literature are full models, in which the terms of any given model are all possible terms built on the space in question, not submodels. Nonetheless, the same proof that the full model satisfies IZF (easily, IZF_{Ref}) applies almost unchanged to the case at hand. To keep the author honest without trying the patience of the reader, only the toughest axiom, Separation, will be sketched.

To this end, suppose the term σ and formula ϕ have (combined) support J (where the support of a formula is the support of its parameters, which are hidden in the notation used). The obvious candidate for a term for the appropriate subset of σ is {⟨σ_{i}, p ∩ p_{i}⟩ | ⟨σ_{i}, p_{i}⟩ ∈ σ ∧ p ⊩ ϕ(σ_{i})}, which will be called Sep_{σ,ϕ}. We will show that this term has support J.

To this end, let q∼_{J}r. We need to show that ⊥ ⊩ Sep_{σ,ϕ} = (Sep_{σ,ϕ})_{qr}. In one direction, any member of (Sep_{σ,ϕ})_{qr} is of the form ⟨σ_{i}, p ∩ p_{i}⟩_{qr}, where ⟨σ_{i}, p ∩ p_{i}⟩ ∈ Sep_{σ,ϕ}, i.e. ⟨σ_{i}, p_{i}⟩ ∈ σ and p ⊩ ϕ(σ_{i}). We need to show that (p ∩ p_{i})_{qr} ⊩ (σ_{i})_{qr} ∈ Sep_{σ,ϕ}. Since ⊥ ⊩ σ = σ_{qr} and (p_{i})_{qr} ⊩ (σ_{i})_{qr} ∈ σ_{qr}, (p_{i})_{qr} ⊩ (σ_{i})_{qr} ∈ σ. In addition, by the lemma above, p_{qr} ⊩ ϕ_{qr}((σ_{i})_{qr}) (where ϕ_{qr} is the result of taking ϕ and applying the homeomorphism to its parameters). Since ϕ’s parameters have support J, ⊥ ⊩ ϕ_{qr} = ϕ, and p_{qr} ⊩ ϕ((σ_{i})_{qr}). Summarizing, (p∩p_{i})_{qr} ⊩ (σ_{i})_{qr} ∈ σ∧ϕ((σ_{i})_{qr}), so (p ∩ p_{i})_{qr} ⊩ (σ_{i})_{qr} ∈ Sep_{σ,ϕ}, as was to be shown.

The other direction is similar. □

So there was no harm in taking the symmetric submodel. The benefit of having done so is the following Lemma 6.9 Extension Lemma: Suppose q, r ⊆ p, q ⊆ ∥f(n) = m∥ and for j ∈ J (q_{j}, K_{j}) = (r_{j}, L_{j}) (i.e. q and r agree on f’s support). Then r has an extension forcing f(n) = m.

Proof. Take a sequence of refinements of q converging to a point X on q’s boundary, as follows. Consider j < n_{r}, j ∉ J. If K_{j}∩ L_{j} is non-empty, then just work within the latter set. Else either sup(K_{j}) < inf(L_{j}), in which case let lim(X_{j}) = sup(K_{j}), or inf(K_{j}) > sup(L_{j}), in which case let lim(X_{j}) = inf(K_{j}). (In what follows, we will consider only the first of those two cases.) Similarly for I_{q} and I_{r}. As usual, since X ∈ p, X has a neighborhood forcing a value for f(n); since X is on q’s boundary, any such neighborhood has to force the same value for f(n) that q did. Let q_{1} be such a neighborhood where, for j the smallest integer not in J, sup((K_{1})_{j}) - sup(K_{j}) is at least half as big as possible.

To continue this construction, consider what would happen if sup (K_{1})_{j} < inf(L_{j}). We would like to take another point X, this time on the boundary of q_{1}, with lim(X_{j}) = sup(K_{1})_{j}. The only possible obstruction is that (q_{1})_{j} might have entries far enough away from sup(K_{1})_{j} so that the constraint of the convergence function would prevent there being such an X. In this case, change (q_{1})_{j} so that this is no longer an obstruction. Since j ∉ J, the new condition is J-similar to the old, and so will still force the same value for f(n).

Repeat this construction, making such that each of the finitely many components j < n_{r}, j ∉ J and the final component get paid attention infinitely often (meaning sup((K_{n+1})_{j}) - sup((K_{n})_{j}) is at least half as big as possible). This produces a sequence q_{n}. Eventually q_{n} will be compatible with r. If not, let X be the limit of the q_{n}’s. If X ∉ r then for some component j lim(X_{j}) < inf(L_{j}). X has a neighborhood, say q_{∞}, forcing f(n) = m. At some large enough stage at which j gets paid attention, the existence of q_{∞} would have made the j^{th} component of the next q_{n} contain lim(X_{j}), a contradiction. □

With the Extension Lemma in hand, the rest of the proof is easy. It should be clear that [Z] has convergence function 2^{−n}. So it remains only to show

Proposition 6.10 ∥ [Z] has no limit ∥ = T.

Proof. Suppose p ⊆ ∥ f is a Cauchy sequence ∥. It suffices to find a q ⊆ p such that q ⊆ ∥ f ≠ lim([Z]) ∥.

By the Extension Lemma, all of f’s values are determined by f’s finite support J. So f cannot be a limit for [Z], as any such limit has to be affected by infinitely many components. □

7 Questions

There is a variant of the questions considered nestled between the individual Cauchy sequences of the big Cauchy sequence being adorned with a modulus of convergence and not. It could be that each such sequence has a modulus of convergence, but the sequence is not paired with any modulus in the big sequence. Looked at differently, perhaps the big sequence is one of Cauchy sequences with moduli of convergence but not uniformly. Certainly this extra information would not weaken any of the positive results. Would it weaken any of the negative theorems though? Presumably not: knowing that each of the individual sequences has a modulus doesn’t seem to help to build a limit sequence or a modulus for such, if there’s no way you can get your hands on them. Still, in the course of trying to prove this some technical difficulties were encountered, so the questions remain open.

The negative results here open up other hierarchies. Starting with the rationals, one could consider equivalence classes of Cauchy sequence with moduli of convergence. By the last theorem, that may not be Cauchy complete. So equivalences classes can be taken of sequences of those. This process can be continued, presumably into the transfinite. Is there a useful structure theorem here? All of this can be viewed as taking place inside of the Dedekind reals, which are Cauchy complete. There is a smallest Cauchy complete set of reals, namely the intersection of all such sets. As pointed out to me by the referee, this could be a proper subset of the Dedekind reals, since that is the case in the topological model of [2]. Naturally enough, the same is also the case in the Kripke model of [4]. Is there any interesting structure between the Cauchy completion of the rationals and the Dedekind reals? What about the corresponding questions for other notions of reals, such as simply Cauchy sequences sans moduli?

As indicated in the introduction, the first two models, one topological and the other Kripke, are essentially, even if not substantially, different. What is the relation between the two?

In the presence of Countable Choice, all of the positive results you could want here are easily provable (e.g. every Cauchy sequence has a modulus of convergence, the reals are Cauchy complete, etc.). Countable Choice itself, though, is a stronger principle than necessary for this, since, as pointed out to me by Fred Richman, these positive results are true under classical logic, but classical logic does not imply Countable Choice. Are there extant, weaker choice principles that would suffice instead? Can the exact amount of choice necessary be specified? These questions will start to be addressed in the forthcoming [5], but there is certainly more that can be done than is even attempted there.

8 Bibliographical references

References

[1] M.H. Escardo and A.K. Simpson, A Universal Characterization of the Closed Euclidean Interval (Extended Abstract), Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp.115-125, 2001

[2] M.P. Fourman and J.M.E. Hyland, Sheaf models for analysis, in M.P. Fourman, C.J. Mulvey, and D.S. Scott (eds.), Applications of Sheaves, Lecture Notes in Mathematics Vol. 753 (Springer-Verlag, Berlin Heidelberg New York, 1979), pp. 280-301

[3] R.J. Grayson, Heyting-valued models for intuitionistic set theory, in M.P. Fourman, C.J. Mulvey, and D.S. Scott (eds.), Applications of Sheaves, Lecture Notes in Mathematics Vol. 753 (Springer-Verlag, Berlin Heidelberg New York, 1979), pp. 402-414

[4] R. Lubarsky and M. Rathjen, On the constructive Dedekind reals, in preparation

[5] R. Lubarsky and F. Richman, in preparation

[6] S. MacLane and I. Moerdijk, Sheaves in Geometry and Logic (Springer-Verlag, New York, 1992)

Lubarsky

[7] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics, Vol. 1 (North Holland, Amsterdam New York Oxford Todyo, 1988)