Separating the Fan Theorem and Its Weakenings

Robert S. Lubarsky and Hannes Diener Dept. of Mathematical Sciences Florida Atlantic University Boca Raton, FL 33431 Robert.Lubarsky@alum.mit.edu Department Mathematik, Fak. IV Emmy-Noether-Campus, Walter-Flex-Str. 3 University of Siegen 57068 Siegen, Germany diener@math.uni-siegen.de

March 31, 2012

Abstract Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which suffices to separate all of the as yet identified fan theorems. keywords: fan theorems, Kripke models, forcing, non-standard models, Heyting-valued models AMS 2010 MSC: 03C90, 03F50, 03F60, 03H05

1 Introduction

To be able to talk about fans, Cantor space, and similar objects properly, we will start by introducing some notation. The space of all infinite binary sequences, endowed with the usual metric, will be denoted by 2^{ℕ}; the space of all finite binary sequences will be denoted by 2^{∗}. The concatenation of u, v ∈ 2^{∗} will be denoted by u ∗ v. The length of a finite sequence u ∈ 2^{∗} will be denoted by |u|. For α ∈ 2^{ℕ} and n ∈ ℕ, the first n elements of α form a finite sequence denoted by \overline{α}n. A subset B ⊂ 2^{∗} is called a bar if

∀α ∈ 2^{ℕ}∃n ∈ ℕ(\overline{α}n ∈ B),

and a bar is called uniform if

∃n ∈ ℕ∀α ∈ 2^{ℕ}∃m ⩽ n(\overline{α}m ∈ B).

Notice that if a bar B is closed under extensions, that is if

∀u ∈ 2^{∗}(u ∈ B ⟹ ∀w ∈ 2^{∗}u ∗ w ∈ B),

then it is uniform if and only if

∃n ∈ ℕ∀α ∈ 2^{ℕ}(\overline{α}n ∈ B).

Not all of the bars we consider will be so closed.

There are currently four versions of Brouwer’s fan theorem in common use. All of them enable one to conclude that a given bar is uniform. The differences among them lie in the required complexity of the bar, which ranges from the very strongest requirement to no restriction on the bar at all. A bar C ⊂ 2^{∗} is decidable if it is decidable as a set:

∀u ∈ 2^{∗} u ∈ C ∨ u ∉ C.

A bar C ⊂ 2^{∗} is called a c-bar if there exists a decidable set C′ ⊂ 2^{∗} such that

u ∈ C ⟺ ∀w ∈ 2^{∗} (u ∗ w ∈ C′) .

A bar B ⊂ 2^{∗} is called a Π_{1}^{0}-bar if there exist a decidable set S ⊂ 2^{∗} × ℕ such that

u ∈ B ⟺ ∀n(u, n) ∈ S .

(The Π_{n}^{0}-nomenclature alludes to the arithmetical hierarchy in recursion theory.) We can now state four commonly used versions of the fan theorem.

FAN_{Δ}: Every decidable bar is uniform.
FAN_{c}: Every c-bar is uniform.
FAN_{Π_{1}^{0}}: Every Π_{1}^{0}-bar is uniform.
FAN_{full}: Every bar is uniform.

Notice that every decidable bar can be taken to be closed under extensions; that is, the closure of a decidable bar under extension is still decidable. If there is no restriction on the definability of a bar, then every bar can be taken to be so closed, by working with the closure of any given bar. Every c-bar is already closed under extension. In contrast, Π_{1}^{0}-bars seemingly cannot be replaced by their closures while remaining Π_{1}^{0}.

By way of motivation, these principles were developed within reverse constructive mathematics, because they are equivalent with certain continuity principles. In particular, FAN_{Δ} is equivalent with the assertion that every uniformly continuous, positively valued function from [0,1] to ℝ has a positive infimum [8], FAN_{c} with the uniform continuity of every continuous f : 2^{ℕ} → ℕ [2], and FAN_{Π_{1}^{0}} with the uniform equicontinuity of every equicontinuous sequence of functions from [0,1] to ℝ [6].

The following implications hold trivially [2, 5]:

FAN_{full} ⟹ FAN_{Π_{1}^{0}} ⟹ FAN_{c} ⟹ FAN_{Δ}.

One naturally wonders whether any of the implications can be reversed, including whether FAN_{Δ} is outright provable in constructive set theory. Some such non-implications have already been determined. It is well-known (see [1] for instance) that FAN_{Δ} is not provable, via recursive realizability. That is, from computability theory there is an infinite computable sub-tree of 2^{∗} with no infinite computable branch, which fact translates to a failure of FAN_{Δ} under IZF (Intuitionistic ZF, the constructive correlate to classical ZF) via recursive realizability, and also to the independence of WKL (Weak König’s Lemma) over RCA_{0} in reverse mathematics [9]. Berger [3] shows that FAN_{Δ} does not imply FAN_{c} over a very weak base system. His argument is in its essence a translation of the reverse mathematics proof that WKL_{0} does not imply ACA [9], by coding the Turing jump into a c-bar. In order for this argument to work, he must be in a context in which the existence of the Turing jump is not outright provable, hence the use of a weak base system. Fourman and Hyland [7] present a Heyting-valued, almost topological, model in which FAN_{full} fails; they do not address which fragments of the Fan Theorem might hold, since these distinctions were not available at the time. We show below that FAN_{Π_{1}^{0}} holds in their model, separating the left-most pair of principles in the diagram above. We are not aware of any prior proofs separating FAN_{c} and FAN_{Π_{1}^{0}}.

The goal of this paper is to separate all of these principles via a uniform technique. This has several benefits. For one, it separates FAN_{c} and FAN_{Π_{1}^{0}}. For another, it separates FAN_{Δ} and FAN_{c} over full IZF. That is, Berger’s argument still leaves open the possibility that standard full set theory would allow that implication to go through; independence of FAN_{c} over IZF + FAN_{Δ} means that it does not. In addition, since the arguments employed rather handily provide four separation results, they seem to provide a flexible tool that might be useful elsewhere. This seems not to be the case for the other techniques that have been used. It could well be the case, for instance, that realizability could produce all of the results discussed here. But no one has been able to do this yet. As for the Fourman-Hyland argument, they also show in the same work that all topological models satisfy FAN_{full}. So for the separations of interest here, topological models are just out. To be sure, variants of topological models, along the lines used by Fourman and Hyland, might still do the trick. But before coming up with the arguments below that’s exactly what we tried, and got nowhere. In short, we cannot say that the techniques used here get you anything that could not be gotten by other means, but it least it seems to be easier to use. Beyond that, it could be the case that the proofs here really are in some sense the right ones for these results. In the face of the perfectly nice realizability and Heyting-valued models that provide some of these separations, we are not at this point making that claim. While the constructions below are natural enough, they are not so compelling as to seem canonical. Nonetheless, since they seem to work so well, it might be that with further reflection and development, it turns out that proofs along these lines are the way to go for a large class of problems.

As for what the techniques employed actually are, since it seemed that realizability and Heyting algebras weren’t working, we turned to the only other kind model we know of, Kripke models. To build a tree we could control, along with its paths, over full set theory, we turned to forcing. In order to have the trees be decidable, yet not completely pinned down, as required by the theories in question, we were forced to use non-standard integers, to provide non-standard levels on the trees.

Since this is a paper about constructive mathematics, a word about the meta-theory used is in order. It is classical through and through. We work in ZFC. Presumably most if not all of the arguments are fully constructive, as in so many math papers. We did not check, and so have no idea.

In the next section we discuss the Fan Theorem in topological and related models, including giving a proof that the Fourman-Hyland model satisfies FAN_{Π_{1}^{0}}. The following sections provide the advertised separation results, going right-to-left in the diagram above. We then close with some questions.

2 The Fan Theorem in Heyting-Valued Models

To make this paper somewhat self-contained, we repeat the proof that explains why the construction afterwards is more complicated than just a topological model.

Proposition 1. (Fourman-Hyland [7]) In any topological model FAN_{full} holds.

Proof. Let T be a topological space, and suppose

T ⊩ “B ⊆ 2^{∗} is a bar closed under extension.”

Then, in particular, for any external sequence α ∈ 2^{ℕ} (that is, one from the ground model)

(1)  T = ⟦∃n \overline{α}n ∈ B⟧ = ⋃_{n∈ℕ}⟦\overline{α}n ∈ B⟧ .

Let A_{u} denote the open set

⟦the bar {w | u ∗ w ∈ B} is uniform⟧ .

If T ⊮ “B is uniform,” then choose some p ∉ A_{()}. Define a set T r = {u ∈ 2^{∗} | p ∉ A_{u}}. Since A_{u} = A_{u∗0} ∩ A_{u∗1} for any u ∈ 2^{∗}, T r is a tree (i.e. closed under restriction) with no terminal nodes. Since in addition () ∈ T r (that is, T r is non-empty), T r is infinite. Thus, by Weak Kőnig’s Lemma, there exists an infinite path β in T r. By the definition of T r, p ∉ A_{\overline{β}n} for all n ∈ ℕ. Now Equation 1 yields the existence of n ∈ ℕ such that

p ∈ ⟦\overline{β}n ∈ B⟧ ;

but this contradicts ⟦\overline{β}n ∈ B⟧ ⊂ A_{\overline{β}n}.

This suggests that if we are looking for models in which some form of the fan theorem fails we need to “delete points”. This was done in [7], section 4, where they consider K(T), the coperfect open sets of a topological space T. This can be viewed as the equivalence classes of the open sets of T, under which an open set is identified with its smallest coperfect superset. In this setting, removing a point from an open set does not change the set.

Definition 1. A Heyting algebara is connected if A ∨ B = ⊤ and A ∧ B = ⊥ implies that either A = ⊤ or A = ⊥.

Let Ω be K([0, 1] × [0, 1]). It is easy to see that Ω is connected.

Proposition 2. If H is a connected Heyting algebra, then H ⊩ FAN_{Π_{1}^{0}}.

Proof. Suppose H ⊩ “B is a Π_{1}^{0}-bar, given say by S : u ∈ B iff ∀n ∈ ℕ (u, n) ∈ S.” Since H ⊩ “S is decidable,” for any u ∈ 2^{∗} and n ∈ ℕ,

H ⊩ “(u, n) ∈ S ∨ (u, n) ∉ S.”

By the connectedness of H either H ⊩ “(u, n) ∈ S” or H ⊩ “(u, n) ∉ S.” So define a set B̃ ⊂ 2^{∗} in the metatheory by

u ∈ B̃ ⟺ ∀n ∈ ℕ H ⊩ “(u, n) ∈ S.”

B̃ is itself a bar: for let α ∈ 2^{ℕ} be arbitrary. If \overline{α}n ∉ B̃ for all n ∈ ℕ then for all n there exist i_{n} such that ⟦(\overline{α}n, i_{n}) ∈ B⟧ = ⊥. Thus

⟦∀m ∈ ℕ (\overline{α}n, m) ∈ B⟧ = ⊥

for any n ∈ ℕ, and therefore

⟦∃n ∈ ℕ∀m ∈ ℕ (\overline{α}n, m) ∈ B⟧ = ⊥ ;

a contradiction to B being a bar internally. Hence B̃ is bar externally, and therefore, working with a classical metatheory (or simply the Fan Theorem), it is uniform. So there exists N such that for all u ∈ 2^{N} some initial segment of u is in B̃. Then it is easy to see, that this same N witnesses the uniformity of B internally.

Corollary 3. FAN_{Π_{1}^{0}} does not imply FAN_{full}.

Proof. In [7] it shown that Ω ⊮ FAN_{full}.

3 FAN_{Δ} is not Provable

As discussed in the introduction, recursive realizability shows that IZF does not prove FAN_{Δ}. However, we do not see how to adapt that, or the Heyting-valued model from the previous section, to the other desired separation results. Hence we are hoping not merely to provide here a different model falsifying FAN_{Δ} as a technical exercise, but rather to provide a technique more flexible than those referenced, to produce the other separation results. Of course, if this really is a flexible technique, it should work for the known separations too.

We will build a Kripke model, working within ZFC. To construct a bar, it will be crucial to control what paths exist. This is most easily done with a generic.

Definition 2. Let the forcing partial order P be the set of appropriate labelings of finitely many nodes from 2^{∗}. A labeling of nodes assigns to each one either IN, OUT, or ∞, with the following restrictions. Any node labeled IN has no descendant, the idea being that once a node gets into the eventual bar so are all of its descendants automatically, so nothing more need be said. Any descendant of a node labeled OUT must labeled IN or OUT. Finally, for any node labeled ∞, if both children are labeled, then at least one of them must be labeled ∞.

Let G be a generic through the condition that labels ⟨⟩ with ∞. By straightforward density arguments, any node labeled OUT by G has a uniform bar above (resp. below) it all labeled IN, and every node labeled ∞ has a path through it always labeled ∞, in fact a perfect set of such.

Let B = {α ∈ 2^{∗}| for some n G(α ↾ n) = IN}. B ∈ M[G] is the interpretation σ_{B}^{G} of the term σ_{B} = {⟨p, α̂⟩ | for some n p(α ↾ n) = IN}. (As usual, the function ^{ ˆ .} is the canonical injection of the ambient universe into the terms: x̂ = {⟨∅, ŷ⟩ | y ∈ x}.) Because of these latter ∞-paths, B is not a bar. However, we might reasonably think that if we no longer had access to the distinction between the OUT and the ∞ nodes, we might no longer be able to build a path avoiding B. This intuition is confirmed by the next lemma.

Definition 3. The shadow forcing Q is the set of functions from finite subtrees of 2^{∗} to {IN, OUT} such that any node labeled IN has no descendant. Equivalently, Q is the sub-p.o. of P beneath the condition labeling ⟨⟩ with OUT (together with the condition which labels ⟨⟩ IN, which has no extension). The canonical project proj_{Q} of P onto Q replaces all occurrences of ∞ with OUT. The canonical projection of the terms of P ’s forcing language to those of Q’s, ambiguously also called proj_{Q}, acts by applying proj_{Q} to the conditions that appear in the terms, hereditarily. (Notice that Q term are also P terms.)

Notice that a P -filter projects to a Q-filter. If G is a generic P -filter, then proj_{Q}(G) will not be Q-generic, because in Q the terminal conditions are dense. Still, proj_{Q}(G) induces an interpretation σ^{proj_{Q}(G)} of the terms σ of Q. These interpretations are in M[G], as they are easily definable from σ and G; alternatively, σ^{proj_{Q}(G)} = (proj_{Q}^{−1′′}σ)^{G}.

For any P -filter G, proj_{Q}(σ_{B})^{proj_{Q}(G)} = B: the induced interpretation of the projection of B is just B itself. Effectively, B as a P -term is already a Q-term.

Proposition 4. If σ is a Q-term and p ⊩_{P} “proj_{Q}^{−1′′}σ is an infinite branch through 2^{∗},” then p ⊩_{P} “proj_{Q}^{−1′′}σ goes through σ_{B}.”

Proof. By standard forcing technology, it suffices to extend p to some condition forcing “proj_{Q}^{−1′′}σ goes through σ_{B},” as then it will be dense beneath p to force as much, and so will happen generically.

First extend p so that every sequence in 2^{∗} of length 2^{n−1} for some n either is labeled OUT or ∞ or has a proper initial segment labeled IN. Then extend again by adjoining both children to all nodes of length 2^{n−1}, and labeling them ∞ whenever possible (otherwise IN or OUT). For a technical reason soon to become clear, we must extend yet again. This time have the domain include all length k descendants of the length n nodes not labeled IN, and label them so that every length n node labeled ∞ has a unique descendant of length k labeled ∞, and, most importantly, for each pair of nodes α and β of length k labeled ∞, there is some i with α(i) = 1 and β(i) = 0. One way of doing this is to let s be the number of nodes of length n labeled ∞, to let k be n + s, and to build the ∞-labeled descendant of the j^{th} such node by adjoining to it j − 1 0’s, a 1, and then s − j 0’s, all other descendants of length k being labeled OUT.

Extend one last time to q ⊩ proj_{Q}^{−1′′}σ(k̂) = α̂ for some fixed α, where as usual x̂ is the standard term for the internalization of the set x. Moreover, q should force the equality in the strong sense that for each j < k there is a term τ and a condition r ≥ q with ⟨r, τ⟩ ∈ proj_{Q}^{−1′′}σ and q ⊩ τ = ⟨ĵ, α̂(ĵ)⟩; even further, if α(j) = 1 then q forces a particular element to be in τ’s second component.

If q labels some initial segment of α IN then we’re done.

If q labels α OUT then it is dense beneath q that all descendants of α of some fixed length are labeled IN, and again we’re done.

If q labels α ∞ then let q_{alt} be identical to q except that all descendants of α ↾ n labeled ∞ by q are labeled OUT by q_{alt}. Observe first that q_{alt} extends p. Then note that, because proj_{Q}(q_{alt}) = proj_{Q}(q), the strong forcing facts posited of q hold for q_{alt} as well: for the same τ and j as above, q_{alt} ⊩ τ ∈ proj_{Q}^{−1′′}σ and q_{alt} ⊩ “τ is an ordered pair with first component ĵ,” and if q forced τ’s second component to be non-empty, q_{alt} also forces it to be non-empty, containing the same term as for q. The difference between q and q_{alt}, from σ’s point of view, is that q_{alt} has more extensions than q: there are conditions extending q_{alt} which bar the tree beneath α, which is not so for q. That means that it is possible for extensions of q_{alt} to force sets into Q-terms that no extension of q could. In the case of proj_{Q}^{−1′′}σ(k̂), though, such opportunities are limited. That term is already forced by p to be a function with domain k; for each j < k there is already a fixed term forced to stand for ⟨j, (proj_{Q}^{−1′′}σ(k̂))(j)⟩; if that function value at j was forced by q to be 1 then it must retain a member and so is also forced by q_{alt} to be 1. The only change possible is that something formerly forced to be empty (i.e. be 0) could now be forced by some extension to have an element (i.e. be 1). Recall, though, the construction of q on level k: if proj_{Q}^{−1′′}σ(k̂) is ever forced by some r ≤ q_{alt} to be some β ≠ α by flipping some 0’s to 1’s, by α’s distinguished 1 r cannot label β ∞. So r can be extended so that all extensions of β of a certain length are labeled IN, forcing proj_{Q}^{−1′′}σ to hit σ_{B}. Of course, any extension of q_{alt} forcing proj_{Q}^{−1′′}σ(k̂) to be α works the same way as such an r does, since q_{alt} already labels α OUT. In either case we have an extension of p forcing proj_{Q}^{−1′′}σ go through σ_{B}.

Even though we have just seen that B is a bar relative to the Q-paths, we will perhaps surprisingly have occasion to consider weaker situations, where B is larger and hence even easier to hit. The case of interest is if we were to change some ∞’s in G to OUTs, thereby allowing uniform bars above those nodes. Notice that if α’s sibling is not labeled ∞, then α’s label could not consistently be changed from ∞, as then α’s parent, labeled ∞, would then have both children not labeled ∞. Such considerations do not apply when α = ⟨⟩.

Definition 4. H is a legal weakening of G if H can be constructed by choosing finitely many nodes labeled ∞ by G, changing those labels (to either IN or OUT), also changing the labeling of finitely many descendants of those nodes from ∞ or OUT to OUT or IN in such a way that each node labeled OUT has a uniform bar above it labeled IN, and then eliminating all descendants of nodes labeled IN. Furthermore, this must be done in such a manner that H is a filter through P (avoiding, for instance, the problem posed just before this definition).

Notice that the difference between H and G can be summarized in one condition p, which contains the new bars, all labeled IN, and all of their ancestors. Hence we use the notation G_{p} to stand for this H: to build G_{p}, make the minimal change to each condition in G in order to be consistent with p.

Lemma 5. If G_{p} is a legal weakening of G then G_{p} is generic through p.

Remark 6. Notice that if p labels the empty sequence IN or OUT then p = G_{p} is a terminal condition in P, trivially satisfying the lemma.

Proof. Let D be dense beneath p. Notice that G ↾ dom(p) is a condition in P contained in G. It is not hard to define the notion of projection beneath p, proj_{p}, by making the minimal changes in a condition necessary to be compatible with p. We claim that proj_{p}^{−1′′}D is dense beneath G ↾ dom(p). To see this, let q ≤ G ↾ dom(p). Extend proj_{p}(q) to r ∈ D. The only way r can extend proj_{p}(q) is by labeling extensions α of nodes which are unchanged by proj_{p}: if α ∈ dom(r)\dom(proj_{p}(q)) then, for α ↾ n ∈ dom(q), q(α ↾ n) = proj_{p}(q)(α ↾ n). Extend q to q_{r} by labeling those same extensions the same way: for α ∈ dom(r)\dom(proj_{p}(q)) q_{r}(α) = r(α). We have that proj_{p}(q_{r}) = r, hence q_{r} ∈ proj_{p}^{−1′′}D. So proj_{p}^{−1′′}D is dense beneath G ↾ dom(p), hence contains a member of G, say q. Then proj_{p}(q) is in both D and G_{p}.

We can now start to describe the ultimate Kripke model. Recall that G is generic for P over M and labels the empty sequence with ∞. The bottom node ⊥ of the Kripke model consists of the Q-terms, with membership (not equality!) as interpreted by proj_{Q}(G). Let N be an ultrapower of M[G] using any non-principal ultrafilter on ω, with elementary embedding f : M[G] → N. This necessarily produces non-standard integers. Let H be the set of legal weakenings of f(G), as defined in N, which induce the same B on the standard levels of 2^{∗}, which restriction is definable only in M[G]. That is, any standard node labeled ∞ by G can only be changed to OUT by the legal weakening. H will index the successors of ⊥. At the node indexed by f(G)_{p}, the universe will be the Q-terms of N as interpreted by proj_{Q}(f(G)_{p}). Regarding the embeddings from ⊥, for a Q-term σ ∈ M, f(σ) is an f(Q)-term in N, so send σ to f(σ). If f(G)_{p} is a terminal condition in P, then the node indexed by f(G)_{p} is terminal in the Kripke ordering. Else iterate. That is, suppose f(G)_{p} is non-terminal. The structure at its node can be built in N. As an ultrapower of M[G], N internally looks like f(M)[f(G)]; internally, f(G) is f(P)-generic over the ground model f(M). The structure at node f(G)_{p} could be built in f(M)[f(G)_{p}], where, by the previous lemma, f(G)_{p} is generic through f(P), and also non-terminal. Hence the construction just described, using an ultrapower and legal weakenings to get additional nodes, can be performed in f(M)[f(G)_{p}] just as above. Continue through ω-many levels. We will ambiguously use f to stand for any of the elementary embeddings, including compositions of such (making f a sort-of polymorhpic transition function). Notice that the construction relativizes: the Kripke structure from node f(G)_{p} onwards is definable in f(M)[f(G)_{p}] just as the entire structure is definable in M[G].

This defines a Kripke structure interpreting membership. Equality at any node can now be defined as extensional equality beyond that node in this structure, inductively on the ranks of the terms, even though the model is not wellfounded, thanks to the elementarity present. That is, working at ⊥, suppose σ and τ are terms of rank at most α, and we have defined equality at ⊥ for all terms of rank less than α. Moreover, suppose (strengthening the inductive assumption here) that this definability was forced in M by the empty condition ∅. At node f(G)_{p} the structure is definable over f(M)[f(G)_{p}], and, by elementarity, in f(M), ∅ ⊩ “Equality in the Kripke model is unambiguously definable for all terms of rank less that f(α).” So at that node we can see whether there is a witness to f(σ) and f(τ) being unequal. If there is such a witness at any node f(G)_{p}, then σ and τ are unequal at ⊥, else they are equal at ⊥. This extends the definability of equality to all terms of rank α. Hence inductively equality is definable for all terms.

Proposition 7. ⊥ ⊮ FAN_{Δ}.

Proof. It is immediate that B is a bar: any node is internally of the form f(M)[f(G)_{p}]; by the lemma, f(G)_{p} is always f(P)-generic; by the proposition, no path given by a Q-term can avoid the B as given by an f(P)-generic. Moreover, B is decidable, as f(G)_{p} agrees with G on the standard part of 2^{∗}, the only part that exists at ⊥, and that argument relativizes to all nodes. However, B is not uniform at any non-terminal node, since f(G)_{p}, when non-terminal, has labels of ∞ at every level.

What remains to show is that our model satisfies IZF. In order to do this, we will need to get a handle on internal truth in the model. This is actually unnecessary for most of the IZF axioms, but for Separation in particular we will have to deal with truth in the model. When forcing, this is done via the forcing and truth lemmas: M[G] ⊧ ϕ iff for some p ∈ G p ⊩ ϕ, where ⊩ is definable in M. Since our Kripke model is built in M[G], statements about it are statements within M[G], and so are forced by conditions in G. The problem is that the Kripke model internally does not have access to G, but only to B. In detail, Separation for M[G] is proven as follows: given ϕ and σ, it suffices to consider {⟨q, τ⟩ | for some ⟨p, τ⟩ ∈ σ q ≤ p and q ⊩ ϕ(τ)}. The problem we face is that that set seems not to be in the Kripke model, even if σ is. What we need to show is that if σ and ϕ’s parameters are Q-terms then that separating set is given by a Q-term.

Recall that proj_{Q} operates by replacing all occurrences of ∞ by OUT.

Definition 5. p ∼ p′ if proj_{Q}(p) = proj_{Q}(p′).

Definition 6. p ⊩^{∗} ϕ, for ϕ in the language of the Kripke model, i.e. when ϕ’s parameters are Q-terms, inductively on ϕ :

• p ⊩^{∗} σ ∈ τ if for some ⟨q, ρ⟩ ∈ τ q ≥_{Q} proj_{Q}(p) and p ⊩^{∗} σ = ρ.

• p ⊩^{∗} σ = τ if for all p′′ ≤_{P} p′ ∼ p and ⟨q, ρ⟩ ∈ σ if proj_{Q}(p′′) ≤_{Q} q then there is a p′′′ ≤_{P} p′′ such that p′′′ ⊩^{∗} ρ ∈ τ, and symmetrically.

• p ⊩^{∗} ϕ ∧ θ if p ⊩^{∗} ϕ and p ⊩^{∗} θ.

• p ⊩^{∗} ϕ ∨ θ if p ⊩^{∗} ϕ or p ⊩^{∗} θ.

• p ⊩^{∗} ϕ → θ if for all p′′ ≤_{P} p′ ∼ p if p′′ ⊩^{∗} ϕ then there is a p′′′ ≤_{P} p′′ such that p′′′ ⊩^{∗} θ.

• p ⊩^{∗} ∃x ϕ(x) if for some Q-term σ p ⊩^{∗} ϕ(σ).

• p ⊩^{∗} ∀x ϕ(x) if for all p′′ ≤_{P} p′ ∼ p and Q-term σ there is a p′′′ ≤_{P} p′′ such that p′′′ ⊩^{∗} ϕ(σ).

Lemma 8. If p ∼ p′ then p ⊩^{∗} ϕ iff p′ ⊩^{∗} ϕ.

Proof. For the cases ∈, =, →, and ∀, that is built right into the definition of ⊩^{∗}. The other cases are a trivial induction.

Lemma 9. If q ≤_{P} p ⊩^{∗} ϕ then q ⊩^{∗} ϕ.

Proof. Inductively on ϕ. For ∈, use that proj_{Q} is monotone. The cases ∧, ∨, and ∃ are trivial inductions. For the remaining cases, suppose q′′ ≤_{P} q′ ∼ q ≤_{P} p. Then q′′ ≤_{P} q′ ↾ dom(p) ∼ p, and use that p ⊩^{∗} ϕ.

Proposition 10. ⊥ ⊧ ϕ iff for some p ∈ G p ⊩^{∗} ϕ.

Proof. Inductively on ϕ.

σ ∈ τ: ⊥ ⊧ σ ∈ τ iff there are p ∈ G and ⟨q, ρ⟩ ∈ τ such that proj_{Q}(p) ≤_{Q} q and ⊥ ⊧ σ = ρ. Inductively ⊥ ⊧ σ = ρ iff there is an r ∈ G ∗-forcing the same. In one direction, using lemma 9, p ∪ r suffices, in the other we have p = r.

σ = τ: Suppose G ∋ p ⊩^{∗} σ = τ. By taking p′ equal to p in the definition of ⊩^{∗}, for every member ρ of either σ or τ, it is dense to ∗-force ρ to be in the other set. By the genericity of G some such p′′′ will be in G, and so inductively ρ will end up in the other set. This shows that σ and τ have the same members at ⊥. Regarding a future node f(G)_{p′′}, because f(G)_{p′′} is a legal weakening of f(G), p′′ ↾ dom(p) ∼ p, so again it is dense for any member of σ or τ to be forced into the other, so they have the same members at node f(G)_{p′′}. Hence ⊥ ⊩^{∗} σ = τ.

Conversely, suppose for all p ∈ G p ⊮^{∗} σ = τ. That means there are p′′ ≤_{P} p′ ∼ p and ρ forced by p′′ into σ (without loss of generality), but p′′ has no extension ∗-forcing ρ into τ. For every natural number n the set D_{n} = {q | for some k > n dom(q) ⊆ 2^{k} and all binary sequences of length k either are labeled ∞ by q or some initial segment is labeled IN by q} is dense. Hence cofinally many levels of G are in D_{0}. Observe that if q is in D_{0} ∩ G and q′ ∼ q then any extension of q′ can be extended again to induce a legal weakening of G. In N, by overspill choose p ∈ f(G) to be in f(D_{0}). Choose p′′ ≤_{P} p′ ∼ p and ρ as given by the case hypothesis. Extend p′′ to p′′′ so that f(G)_{p′′′} is a legal weakening of f(G). Since p′′′ has no extension ∗-forcing ρ into τ, inductively at node f(G)_{p′′′} ρ is not a member of τ. Hence ⊥ |̸= σ = τ.

ϕ ∧ θ: Trivial.

ϕ ∨ θ: Trivial.

ϕ → θ: Suppose G ∋ p ⊩^{∗} ϕ → θ. At any node f(G)_{p′}, if f(G)_{p′} ⊧ ϕ then inductively choose p′′ ∈ f(G)_{p′} such that p′′ ⊩^{∗} ϕ. Without loss of generality p′′ can be taken to extend p′. Since f(G)_{p′} indexes a node in the model, p′ ↾ dom(p) ∼ p, so p′′ ≤_{P} p′ ↾ dom(p) ∼ p. By the case assumption there is a p′′′ extending p′′ with p′′′ ⊩^{∗} θ. By the genericity of f(G)_{p′} there is such a p′′′ in f(G)_{p′}. So inductively f(G)_{p′} ⊧ θ. At node ⊥ the argument is even simpler, as p′ can be chosen to be p. So ⊥ ⊧ ϕ → θ.

Conversely, suppose for all p ∈ G p ⊮^{∗} ϕ → θ. That means there are p′′ ≤_{P} p′ ∼ p with p′′ ⊩^{∗} ϕ but no extension of p′′ ∗-forces θ. As in the = case above, in N, by overspill choose p ∈ f(G) to be in f(D_{0}). Choose p′′ ≤_{P} p′ ∼ p as given by the case hypothesis. Extend p′′ to p′′′ so that f(G)_{p′′′} is a legal weakening of f(G). Inductively f(G)_{p′′′} ⊧ ϕ, but since p′′′ has no extension ∗-forcing θ, inductively f(G)_{p′′′} |̸= θ. Hence ⊥ |̸= ϕ → θ.

∃x ϕ(x): Trivial.

∀x ϕ(x): Suppose G ∋ p ⊩^{∗} ∀x ϕ(x). For any node f(G)_{p′} and any σ in the universe there, p′ ≤_{P} p′ ↾ dom(p) ∼ p, so there is a p′′ ≤_{P} p′ such that p′′ ⊩^{∗} ϕ(σ). By genericity there is such a p′′ in f(G)_{p′}. Inductively f(G)_{p′} ⊧ ϕ(σ). So every element at node f(G)_{p′} satisfies ϕ there. At node ⊥ the argument is even easier, since p′ can be chosen to be p. Hence ⊥ ⊧ ∀x ϕ(x).

Conversely, suppose for all p ∈ G p ⊮^{∗} ∀x ϕ(x). That means there are p′′ ≤_{P} p′ ∼ p and Q-term σ such that p′′ has no extension ∗-forcing ϕ(σ). As in the cases of = and → above, in N, by overspill choose p ∈ f(G) to be in f(D_{0}). Choose p′′ ≤_{P} p′ ∼ p and σ as given by the case hypothesis. Extend p′′ to p′′′ so that f(G)_{p′′′} is a legal weakening of f(G). Since p′′′ has no extension ∗-forcing ϕ(σ), inductively f(G)_{p′′′} |̸= ϕ(σ). Hence ⊥ |̸= ∀x ϕ(x).

Theorem 11. ⊥ ⊧ IZF

Proof. Empty Set and Infinity are witnessed by ∅ and ω̂ respectively. Pairing is witnessed by {⟨∅, σ⟩, ⟨∅, τ⟩}, and Union by {⟨q ∪ r, ρ⟩ | for some τ ⟨q, τ⟩ ∈ σ and ⟨r, ρ⟩ ∈ τ}. Extensionality holds because that’s how = was defined.

For ϵ-Induction, suppose ⊥ ⊧ “(∀y ∈ x ϕ(y)) → ϕ(x).” If it were not the case that ⊥ ⊧ “∀x ϕ(x)”, then at some later node G_{p} there would be a term σ with f(G)_{p} |̸= ϕ(σ). The restricted Kripke model of node f(G)_{p} and its extensions is definable in a model of ZF, say N, which is a finite iteration of the ultrapower construction, and so is itself a model of ZF. Hence in N σ can be chosen to be such a term of least V -rank, say κ. Then at all nodes after f(G)_{p}, by elementarity, it holds that f(κ) is the least rank of any term not satisfying ϕ. So all members of σ, being of lower rank, satisfy ϕ at whatever node they appear. By the induction hypothesis, σ must also satisfy ϕ, contradicting the assumption that some term does not satisfy ϕ.

For the powerset of σ take all sets with members of the form ⟨q, τ⟩, where ⟨p, τ⟩ ∈ σ and q ≤_{Q} p.

It is easy to give a coarse proof of Bounding. The Kripke model can be built in M[G]. Given a σ at ⊥, Bounding in M[G] can be used to bound the range of ϕ on σ at ⊥. Also, the set of nodes is set-sized, so there are only set-many interpretations of f(σ) at the other nodes, so the range of ϕ on them can also be bounded. Since the standard ordinals are cofinal through the ordinals in all of the iterated ultrapowers, by picking κ large enough, V̂_{κ} suffices for bounding the range of ϕ on σ.

For Separation, given ϕ and σ, let Sep_{ϕ,σ} be {⟨proj_{Q}(p), τ⟩ | for some ⟨q, τ⟩ ∈ σ with p ≤ q we have p ⊩^{∗} ϕ(σ)}. By lemmas 8 and 10, this works.

Although this model does not satisfy FAN_{Δ}, it does satisfy ¬¬FAN_{Δ}, as the terminal nodes are dense. Admittedly this is a rather weak failure of FAN_{Δ}. In the final section, we will address the issue of getting stronger failures of FAN_{Δ}.

4 FAN_{Δ} does not imply FAN_{c}

We will need a tree similar to that of the last proof. In fact, we will need two trees: the c−bar C, and the decidable set C′ from which C is defined. (Both can be viewed as 2^{∗} with labels or as subtrees of 2^{∗}.) Mostly we will focus on C. Because FAN_{c} refers to eventual membership in a tree, the difference between IN and OUT nodes is no longer relevant: the bar is uniform beneath any OUT node. So we can describe the forcing in terms similar to those before, and with some simplifications introduced. The forcing partial order P will be the set of appropriate labelings of finitely many nodes from 2^{∗}. A labeling of nodes assigns to each one either IN or ∞, with the following restrictions. Any node labeled IN has no descendant, the idea being that once a node gets into the eventual bar so are all of its descendants automatically, so nothing more need be said. For any node labeled ∞, if both children are labeled, then at least one of them must be labeled ∞. Let G be P-generic through the condition labeling the empty sequence with ∞.

As before, we will need to look at weaker trees, ones with bigger bars.

Definition 7. H is a legal weakening of G if H can be constructed by choosing finitely many nodes labeled ∞ by G, whose siblings are also labeled ∞ by G, and changing those labels to IN and eliminating all descendants.

As before, each legal weakening H can be summarized by one forcing condition p, which consists of those nodes changed by H and their ancestors, labeled as in G. H is then the set of conditions in G each minimally changed to be consistent with p. Hence we refer to H as G_{p}.

Lemma 12. If G_{p} is a legal weakening of G then G_{p} is generic through p.

Proof. As in the corresponding lemma in the previous section.

Definition 8. Terms are defined inductively (through the ordinals) as sets of the form {⟨B_{i}, σ_{i}⟩ | i ∈ I}, where I is any index set, σ_{i} a term, and B_{i} a finite set of truth values. A truth value is a symbol of the form b^{+} or b′ or ¬b′, for b ∈ 2^{∗} a finite binary sequence.

Definition 9. Let C be the term {⟨{b^{+}}, b̂⟩ | b ∈ 2^{∗}}, and C′ be {⟨{b′}, b̂⟩ | b ∈ 2^{∗}}.

In our final model, (the interpretation of) C will be the c-bar induced by (the interpretation of) C′, and C will not be uniform, thereby falsifying FAN_{c}. Furthermore, we will show that FAN_{Δ} holds in this model.

We can now start to describe the ultimate Kripke model. Recall that G is generic for P over M and labels the empty sequence with ∞. The bottom node ⊥ of the Kripke model consists of the terms. At ⊥, b^{+} counts as true iff G(b) = IN, b′ always counts as true, and ¬b′ never counts as true. Later nodes will have different ways of counting the various literals as true. At any node, for σ = {⟨B_{i}, σ_{i}⟩ | i ∈ I}, if each member of some B_{i} counts as true, then at that node σ_{i} ∈ σ. This induces a notion of extensional equality among the terms. One way of viewing this is at any node to remove from a term σ any pair ⟨B_{i}, σ_{i}⟩ if some member of B_{i} is not true at that node. Then each remaining ⟨B_{i}, σ_{i}⟩ can be replaced by σ_{i}. Equality is then as given by the Axiom of Extensionality as interpreted in the model.

As for what the other nodes in the model are, there are two different kinds. As in the last section, let N be an ultrapower of M[G] using any non-principal ultrafilter on ω, with elementary embedding f : M[G] → N. This necessarily produces non-standard integers. In N, any forcing condition p which induces a legal weakening of f(G) will index a successor node to ⊥. At the node indexed by p, the universe will be the terms of N as interpreted by f(G)_{p}. That is, b^{+} is true if f(G)_{p}(b) = IN, b′ is always true, and ¬b′ never. Regarding the embeddings from ⊥, for a term σ ∈ M, f(σ) is a term in N, so send σ to f(σ). In addition, definably over M[G], any non-standard c ∈ 2^{∗} with f(G)(c) = ∞ also indexes a node. At such a node c, b′ counts as true iff b ≠ c, ¬b′ counts as true iff b = c, and b^{+} counts as true iff b ⊈ c (b is not an initial segment of c). Note that at ⊥ any b′ refers only to a standard b; for some b′ to be declared false at a later node c, b would have to equal c, and c indexes a node only if c is non-standard. Hence there is no conflict with the Kripke structure: once b′ is deemed true, it remains true. Similarly with b^{+}: G_{p} is a fattening of G. Hence membership, being based on finitely many truth values, is monotone.

Any node indexed by such a c ∈ 2^{∗} is terminal in the Kripke ordering. Also, among nodes of the other kind, there is one trivial condition p, the one with p(⟨⟩) = IN. This is also a terminal node, where each b^{+} and each b′ is true. At any other node, iterate. That is, suppose p is not the preceding condition. The model at p can be built in N. As an ultrapower of M[G], N internally looks like f(M)[f(G)]. The structure at node p could be built in f(M)[f(G)_{p}], where f(G)_{p} is generic through f(P) (and non-trivial). Hence the construction just described, using an ultrapower and legal weakenings and non-standard binary strings to get additional nodes, can be performed in f(M)[f(G)_{p}] just as above. This provides immediate successors to nodes indexed by (non-trivial) p’s. Iterate ω-many times.

The picture is that at ⊥ C looks like G, that is, those nodes G assigns to be IN. This tree gets fatter at later nodes that are legal weakenings. At terminal nodes c, C is everything but the branch up to c. At most nodes C′ looks like everything; at node c, where c is non-standard relative to its predecessor, we find the one thing not in C′, namely c.

It is easy to see that C is the c−set induced by C′: once b is forced into C, none of its descendants index terminal nodes, so no descendant is forced out of C′; similarly, if b is not forced into C, say at node p, then G_{p}(b) = ∞, and in N some non-standard extension c of b will also be labeled ∞ by f(G)_{p}, and that c will index a node at which c is not in C′. Clearly, C is not uniform, and C′ is decidable.

What remains to show is that C is bar, that FAN_{Δ} holds, and that IZF holds.

Lemma 13. ⊥ ⊧ C is a bar.

Proof. Suppose σ is forced to be an infinite binary path at some node. If that node is a terminal node, C contains cofinitely many members of 2^{∗}, and so certainly intersects σ. Else without loss of generality we can assume the node is ⊥. Then for some p ∈ G p ⊩ “⊥ ⊧ σ is an infinite binary path.” If it is not dense beneath p to force the standard part of σ (that is, σ applied to the standard integers) to be in the ground model, then extensions q and r of p force incompatible facts about σ. The only incompatible facts about σ are of the form b^{⌢}0 ∈ σ and b^{⌢}1 ∈ σ. The positive parts of q and r (that is, q^{−1}(IN) and r^{−1}(IN)) induce a legal weakening of G. That is, there is a canonical condition inpart(q, r), with domain dom(q) ∪ dom(r), that returns IN on any node that either q or r returns IN on, as well as on any node if inpart(q, r) returns IN on both children, else OUT. Because terms use only positive (i.e. IN) information, at the node f(G)_{inpart(q,r)}, both b^{⌢}0 and b^{⌢}1 are in σ. (More coarsely and perhaps more simply, at the node induced by the trivial condition sending the empty sequence to IN, the same conclusion holds for the same reason.) Hence ⊥ could not have forced σ to be a path in the first place. Therefore p forces σ on the standard binary tree to be in the ground model. It is easy to see that generically G labels some node in σ IN.

Lemma 14. ⊥ ⊧ FAN_{Δ} Proof. By arguments similar to the above. If a set of nodes B is forced by p to be decidable, then no extensions of p can force incompatible facts about B. Hence B is in the ground model. If B were not a bar in the ground model, there would be a ground model path missing B. This path would also be in the Kripke model. Hence B is a bar in the ground model. Since the ground model is taken to be classical, B is uniform.

Regarding getting IZF to be true, just as in the previous section, the problem is that truth in the Kripke model is on the surface determined by forcing conditions in the ground model, to which the Kripke model has no access. The essence is to capture truth at a node using those truth values that are allowed in the building of terms.

Definition 10. For a forcing condition p, B_{p} = {b^{+} | for some initial segment c of b p(c) = IN}.

For a set of truth values B, B^{+} = B ∩ {b^{+} | b ∈ 2^{∗}}. Also, B is positive if B contains no truth value of the form ¬b′.

Definition 11. 1. ¬b′ ⊩^{∗} B iff c^{+} ∈ B → c^{+} ⊈ b′, c′ ∈ B → c ≠ b, and ¬c′ ∈ B → c = b.

2. σ^{¬b′} = {σ_{i}^{¬b′} | for some ⟨B_{i}, σ_{i}⟩ ∈ σ ¬b′ ⊩^{∗} B_{i}}.

3. For ϕ(σ_{1}, ...σ_{n}) in the language of the Kripke model, that is, with parameters (displayed) terms, ϕ^{¬b′} = ϕ(σ_{1}^{¬b′}, ...σ_{n}^{¬b′}).

4. ¬b′ ⊩^{∗} ϕ, for ϕ in the language of the Kripke model, if ϕ^{¬b′} is true (i.e. in V.) Note that ϕ^{¬b′} is a formula with set parameters.

Definition 12. q ≤_{W} p (q is a weakening of p as conditions) if for b ∈ dom(p) either p(b) = ∞ or for some initial segment c of b q(c) = IN.

The idea behind this definition is the q may change some ∞’s to IN’s, as well as add other stuff (extend the domain). Notice that ≤_{W} is a partial order, and inpart(p, q), from lemma 14, is the glb of p and q.

Definition 13. p ⊩^{∗} ϕ, for ϕ in the language of the Kripke model, i.e. when ϕ’s parameters are terms, inductively on ϕ :

• p ⊩^{∗} σ ∈ τ if for some ⟨B_{i}, τ_{i}⟩ ∈ τ with B_{i} positive, B_{i}^{+} ⊆ B_{p} and p ⊩^{∗} σ = τ_{i}.

• p ⊩^{∗} σ = τ if i) for all ⟨B_{i}, σ_{i}⟩ ∈ σ and q ≤_{W} p if B_{i} is positive and B_{i}^{+} ⊆ B_{q} then there is an r ≤ q such that r ⊩^{∗} σ_{i} ∈ τ, and symmetrically between σ and τ, and ii) for all b ∉ dom(p), if for no initial segment c of b is c^{+} in B_{p}, then ¬b′ ⊩^{∗} σ = τ.

• p ⊩^{∗} ϕ ∧ θ if p ⊩^{∗} ϕ and p ⊩^{∗} θ.

• p ⊩^{∗} ϕ ∨ θ if p ⊩^{∗} ϕ or p ⊩^{∗} θ.

• p ⊩^{∗} ϕ → θ if i) for all q ≤_{W} p if q ⊩^{∗} ϕ then there is an r ≤ q such that r ⊩^{∗} θ, and ii) for all b ∉ dom(p), if for no initial segment c of b is c^{+} in B_{p}, then ¬b′ ⊩^{∗} ϕ → θ.

• p ⊩^{∗} ∃x ϕ(x) if for some term σ p ⊩^{∗} ϕ(σ).

• p ⊩^{∗} ∀x ϕ(x) if i) for all terms σ and q ≤_{W} p there is an r ≤ q such that r ⊩^{∗} ϕ(σ), and ii) for all b ∉ dom(p), if for no initial segment c of b is c^{+} in B_{p}, then ¬b′ ⊩^{∗} ∀x ϕ(x).

Proposition 15. If q ≤_{W} p ⊩^{∗} ϕ then q ⊩^{∗} ϕ.

Proof. Trivial induction on ϕ.

Lemma 16. ⊥ ⊧ ϕ iff for some p ∈ G p ⊩^{∗} ϕ.

Proof. Inductively on ϕ.

σ ∈ τ: ⊥ ⊧ σ ∈ τ iff for some ⟨B_{i}, τ_{i}⟩ ∈ τ every member of B_{i} is true at ⊥ and ⊥ ⊧ σ = τ_{i}. The former clause holds iff B_{i} is positive and for some p ∈ G B_{i} ⊆ B_{p}. Inductively, the latter clause holds iff, for some q ∈ G B_{q} ⊩^{∗} σ = τ_{i}. Given such p and q, p ∪ q suffices. The converse direction is immediate.

σ = τ: Suppose G ∋ p ⊩^{∗} σ = τ. If q ∈ f(P) indexes a node then q ≤_{W} p. If q ⊧ ρ ∈ σ then inductively there is a q′ ∈ f(G)_{q}, q′ ≤ q, such that q′ ⊩^{∗} ρ = σ_{i} ∧ σ_{i} ∈ f(σ) for some ⟨B_{i}, σ_{i}⟩ ∈ f(σ). By i) of the case hypothesis, there is an r ≤ q′ with r ⊩^{∗} ρ ∈ τ. Generically, there is such an r in f(G), so inductively q ⊧ ρ ∈ τ. If c indexes a node, then by ii) of the case hypothesis c ⊧ σ = τ. Hence ⊥ ⊧ σ = τ.

Conversely, suppose there is no such p ∈ G. If p ⊮^{∗} σ = τ because clause i) fails, then there is a witness q ≤_{W} p to that failure. We say that such a q is close to p if dom(q) ⊆ dom(p). That means that q comes from p by changing some ∞’s to IN’s and not adding anything else. Observe that if i) fails for p, then p can be extended to p′ so that i) fails for p′ via a witness q close to p′. That’s because dom(p′) can be taken to be dom(p) ∪ dom(q), for b ∈ dom(p) p′(b) can be taken to be p(b), and for b ∈ dom(q)\dom(p) p′(b) can be taken to be q(b). Therefore D = {p | p ⊩^{∗} σ = τ or p violates i) with a witness q close to p or p violates ii)} is dense.

Suppose there were a p ∈ G violating i) with a witness q close to p. Then q induces a legal weakening f(G)_{q} of f(G), and so indexes a node. By the choice of q, q ⊧ σ_{i} ∈ σ. If q ⊧ σ_{i} ∈ τ then inductively that would be ∗-forced by some r ≤ q. But by the choice of q there is no such r. Hence we would have q |̸= σ = τ.

If there is no such p then every p ∈ G violates ii). Let p ∈ f(G) be such that p ⊇ G. Since ii) fails for that p, then, with b from that failure, b indexes a node, b |̸= σ = τ. In either case, ⊥ |̸= σ = τ.

ϕ ∧ θ: Trivial.

ϕ ∨ θ: Trivial.

ϕ → θ: Suppose G ∋ p ⊩^{∗} ϕ → θ. If q ⊧ ϕ then inductively for some q′ ∈ f(G)_{q} q′ ⊩^{∗} ϕ. Since we can take q′ ≤ q ≤_{W} p, by i) of the hypothesis there is an r ≤ q such that r ⊩^{∗} θ. By genericity, there is such an r in f(G)_{q}. Hence q ⊧ θ. If c ⊧ ϕ then use ii) of the hypothesis.

Conversely, suppose there is no such p ∈ G. If p ⊮^{∗} ϕ → θ because clause i) fails, then there is a witness q ≤_{W} p to that failure, in which case p can be extended to p′ so that i) fails for p′ via a witness q close to p′, where closeness is as defined above in the case for =, for the same reason as above. Therefore D = {p | p ⊩^{∗} ϕ → θ or p violates i) with a witness q close to p or p violates ii)} is dense.

Suppose there were a p ∈ G violating i) with a witness q close to p. Then q induces a legal weakening f(G)_{q} of f(G), and so indexes a node. By the choice of q, q ⊧ ϕ. If q ⊧ θ then inductively that would be ∗-forced by some r ≤ q. But by the choice of q there is no such r. Hence we would have q |̸= ϕ → θ.

If there is no such p then every p ∈ G violates ii). Let p ∈ f(G) be such that p ⊇ G. Since ii) fails for that p, then, with b from that failure, b indexes a node and b |̸= ϕ → θ. In either case, ⊥ |̸= ϕ → θ.

∃x ϕ(x): Trivial.

∀x ϕ(x): As in the cases for = and → .

Lemma 17. ⊥ ⊧ IZF

Proof. Just as in the last section, most of the axioms have soft proofs in this model. The only issue is with Separation. Given ϕ and σ, let Sep_{ϕ,σ} be {⟨B, τ⟩ | for some ⟨B′, τ⟩ ∈ σ with B ⊇ B′ either i) B = B_{p} ⊩ ϕ(σ), or ii) ¬b′ ∈ B and ¬b′ ⊩^{∗} ϕ}. By the previous lemma, this works.

As in the previous section, this model does not satisfy FAN_{c}, but does satisfy ¬¬ FAN_{c}. For further discussion, see the questions at the end.

5 FAN_{c} does not imply FAN_{Π_{1}^{0}}

Let G be P -generic exactly as in the last section. By convention, we say that if G(α) = IN then G applied to any extension of α is also IN. Our goal is to hide G a bit better than before, so FAN_{c} remains true, but not too well, so that FAN_{Π_{1}^{0}} is false.

Let N be an ultrapower of M[G] using a non-principal ultrafilter on ω. The Kripke model has a bottom node ⊥, and the successors of ⊥ are indexed by the labels ⟨n, α⟩, where n is a non-standard integer, and α ∈ 2^{∗} either has non-standard length or G(α) = ∞.

Definition 14. A truth value is a symbol of the form ⟨n, α⟩, ¬⟨n, α⟩, or ⟨∀n, α⟩, for n a natural number (in the first two cases) and α ∈ 2^{∗}. Admittedly truth values of the first kind are also used to index nodes; whether truth values or nodes are intended in any particular case should be clear from the context. Terms are defined inductively (through the ordinals) as sets of the form {⟨B_{i}, σ_{i}⟩ | i ∈ I}, where I is any index set, σ_{i} a term, and B_{i} a finite set of truth values.

The sets at ⊥ will be the terms in M. The sets at any other node will be analogous, that is, the terms in what N thinks is the ground model, i.e. ⋃_{κ∈ORD} f(M_{κ}). At ⊥, ⟨n, α⟩ will always be true, ¬⟨n, α⟩ always false, and ⟨∀n, α⟩ true exactly when G(α) = IN. At node ⟨m, β⟩, ⟨n, α⟩ is true exactly when ⟨n, α⟩ ≠ ⟨m, β⟩, ¬⟨n, α⟩ is true exactly when ⟨n, α⟩ = ⟨m, β⟩, and ⟨∀n, α⟩ true exactly when α ≠ β. This interpretation of the truth values induces an interpretation of the terms at all nodes.

Let T_{n} be the term {⟨{⟨n, α⟩}, α̂⟩ | α ∈ 2^{∗}}. Let C be a term naming the function that on input n returns T_{n}. T_{n} at ⊥ looks like the full tree 2^{∗}; T_{n} at ⟨n, α⟩ looks like everything except α; and T_{n} at ⟨m, α⟩, m ≠ n, again looks like 2^{∗}. The term for ⋂_{n} C(n) is given by {⟨{⟨∀n, α⟩}, α̂⟩ | α ∈ 2^{∗}}, and is interpreted as {α | G(α) = IN } at ⊥ and 2^{∗}\{α} at ⟨n, α⟩. Notice that ⋂_{n} C(n) is not closed under extensions.

The proof will be finished once we show that, at ⊥, FAN_{c} holds, IZF holds, and ⋂_{n} C(n) is a counter-example to FAN_{Π_{1}^{0}}.

For the last fact, it is clear that T_{n} is decidable, and so ⋂_{n} C(n) is on the face of it Π_{1}^{0}. So to finish that part up, the next lemma suffices.

Lemma 18. ⊥ ⊩ “ ⋂_{n} C(n) is a bar.”

Proof. Let ⊥ ⊧ “Br is a branch through 2^{∗}.” Work beneath a condition forcing that, so we can assume Br consists of sets of the form ⟨B_{i}, α̂⟩, for various α ∈ 2^{∗}. If the standard part of Br, the part visible at ⊥, is in the ground model M, then by the genericity of G Br will hit G (i.e. for some α ∈ Br G(α) = IN), which is how ⊥ interprets ⋂_{n} C(n). If the standard part of Br were not in M, then contradictory facts about Br would be forced by different forcing conditions. In particular, we would have p, q, and α with p ⊩ “⊥ ⊧ α^{⌢}0 ∈ Br” and q ⊩ “⊥ ⊧ α^{⌢}1 ∈ Br.” That means there are ⟨B_{p}, α̂^{⌢}0⟩ ∈ Br and ⟨B_{q}, α̂^{⌢}1⟩ ∈ Br, with B_{p} and B_{q} consisting only of truth values automatically true at ⊥ save for some of the form ⟨∀n, α⟩. But at some node ⟨n, α⟩ with α non-standard, all of those latter truth values will be true. Hence ⟨n, α⟩ ⊧ “α̂^{⌢}0, α̂^{⌢}1 ∈ Br, ” so ⊥ could not force Br to be a path.

In order to prove the other facts, we will need to deal with truth at ⊥.

Definition 15. For a forcing condition p, let | p |, the length of p, be the length of the longest α ∈ dom(p). Let B_{p} be {⟨n, α⟩ | n, length(α) ≤| p |} ∪ {⟨∀n, α⟩ | length(α) ≤| p | and for some initial segment β of α p(β) = IN}.

Definition 16. 1. ¬⟨n, α⟩ ⊩^{∗} B iff ⟨n, α⟩ ∉ B, ⟨∀n, α⟩ ∉ B, and the only truth value of the form ¬⟨m, β⟩ in B is ¬⟨n, α⟩ itself.

2. σ^{¬⟨n,α⟩} = {σ_{i}^{¬⟨n,α⟩} | for some ⟨B_{i}, σ_{i}⟩ ∈ σ ¬⟨n, α⟩ ⊩^{∗} B_{i}}.

3. For ϕ(σ_{1}, ...σ_{n}) in the language of the Kripke model, that is, with parameters (displayed) terms, ϕ^{¬⟨n,α⟩} = ϕ(σ_{1}^{¬⟨n,α⟩}, ...σ_{n}^{¬⟨n,α⟩}).

4. ¬⟨n, α⟩ ⊩^{∗} ϕ, for ϕ in the language of the Kripke model, if ϕ^{¬⟨n,α⟩} is true (i.e. in V.) Note that ϕ^{¬⟨n,α⟩} is a formula with set parameters.

Definition 17. p ⊩^{∗} ϕ, for B a finite set of truth values and ϕ in the language of the Kripke model, i.e. when ϕ’s parameters are terms, inductively on ϕ :

• p ⊩^{∗} σ ∈ τ if for some ⟨B_{i}, τ_{i}⟩ ∈ τ, B_{i} ⊆ B_{p} and p ⊩^{∗} σ = τ_{i}.

• p ⊩^{∗} σ = τ if i) for all ⟨B_{i}, σ_{i}⟩ ∈ σ and q ≤ p if B_{i} ⊆ B_{q} then there is an r ≤ q such that r ⊩^{∗} σ_{i} ∈ τ, and symmetrically between σ and τ, and ii) if n >| p |, and if either length(α) >| p | or for no initial segment β of α do we have p(β) = IN, then ¬⟨n, α⟩ ⊩^{∗} σ = τ.

• p ⊩^{∗} ϕ ∧ θ if p ⊩^{∗} ϕ and p ⊩^{∗} θ.

• p ⊩^{∗} ϕ ∨ θ if p ⊩^{∗} ϕ or p ⊩^{∗} θ.

• p ⊩^{∗} ϕ → θ if i) for all q ≤ p if q ⊩^{∗} ϕ then there is an r ≤ q such that r ⊩^{∗} θ, and ii) if n >| p |, and if either length(α) >| p | or for no initial segment β of α do we have p(β) = IN, then ¬⟨n, α⟩ ⊩^{∗} ϕ → θ.

• p ⊩^{∗} ∃x ϕ(x) if for some term σ p ⊩^{∗} ϕ(σ).

• p ⊩^{∗} ∀x ϕ(x) if i) for all terms σ and q ≤ p there is an r ≤ q such that r ⊩^{∗} ϕ(σ), and ii) if n >| p |, and if either length(α) >| p | or for no initial segment β of α do we have p(β) = IN, then ¬⟨n, α⟩ ⊩^{∗} ∀x ϕ(x).

Proposition 19. If q ≤ p ⊩^{∗} ϕ then q ⊩^{∗} ϕ.

Proof. Trivial induction on ϕ.

Lemma 20. ⊥ ⊧ ϕ iff for some p ∈ G p ⊩^{∗} ϕ.

Proof. Inductively on ϕ.

σ ∈ τ: ⊥ ⊧ σ ∈ τ iff for some ⟨B_{i}, τ_{i}⟩ ∈ τ every member of B_{i} is true at ⊥ and ⊥ ⊧ σ = τ_{i}. The former clause holds iff B_{i} contains nothing of the form ¬⟨n, α⟩, and if ⟨∀n, α⟩ ∈ B_{i} then G(α) = IN. Given such a B_{i}, let p be a sufficiently long initial segment of G forcing “σ = τ_{i}.” Such a p suffices. The converse direction is immediate.

σ = τ: Suppose G ∋ p ⊩^{∗} σ = τ. Then any member of σ at ⊥ is equal at ⊥ to some σ_{i}, where ⟨B_{i}, σ_{i}⟩ ∈ σ and B_{i} ⊆ B_{q} for some q ∈ G. Then by the hypothesis and genericity there will be an extension r of q in G forcing σ_{i} to be in τ. At any other node ⟨n, α⟩, working in N, n is non-standard and so greater than | p |, and α also satisfies the conditions in ii) (of the definition of ∗-forcing equality), so “σ = τ” is true at these other nodes too.

Conversely, suppose there is no such p ∈ G. With reference to the definition of ∗-forcing equality, observe that {p | p satisfies clause i)} ∪ {p | for some ⟨B_{i}, σ_{i}⟩ ∈ σ B_{i} ⊆ B_{p} yet p has no extension ∗-forcing σ_{i} into τ} is dense. If G contains a member of the second set of that union, then the induced σ_{i} witnesses that ⊥ |̸= σ = τ. If not, then G contains p satisfying i). So no p ∈ G satisfies ii). This also holds in N. In N, take p to be an initial segment of G of non-standard length. The failure of ii) for that p produces an n and α which index a node at which σ ≠ τ, showing ⊥ |̸= σ = τ.

ϕ ∧ θ: Trivial.

ϕ ∨ θ: Trivial.

ϕ → θ: Suppose G ∋ p ⊩^{∗} ϕ → θ. Then it is direct that ⊥ ⊧ ϕ → θ.

Conversely, suppose there is no such p ∈ G. With reference to the definition of ∗-forcing implication, observe that {p | p satisfies clause i)} ∪ {p | p ⊩^{∗} ϕ yet p has no extension ∗-forcing θ} is dense. If G contains a member of the second set of that union, then inductively ⊥ ⊧ ϕ and ⊥ |̸= θ, hence ⊥ |̸= ϕ → θ. If not, then G contains p satisfying i). So no p ∈ G satisfies ii). This also holds in N. In N, take p to be an initial segment of G of non-standard length. The failure of ii) for that p produces an n and α which index a node at which ϕ → θ is false, showing ⊥ |̸= ϕ → θ.

∃x ϕ(x): Trivial.

∀x ϕ(x): As in the cases for = and → .

Lemma 21. ⊥ ⊧ IZF

Proof. As before, all of the axioms have soft proofs, save for Separation. Given ϕ and σ, let Sep_{ϕ,σ} be {⟨B_{i}∪B_{p}, τ⟩ | ⟨B_{i}, τ⟩ ∈ σ and p ⊩^{∗} ϕ(τ)}∪{⟨B, τ⟩ | for some ¬⟨n, α⟩ ∈ B and some B_{i}, ⟨B_{i}, τ⟩ ∈ σ, ¬⟨n, α⟩ ⊩^{∗} B_{i}, and ¬⟨n, α⟩ ⊩^{∗} ϕ(τ)}. By the previous lemma, this works.

Lemma 22. ⊥ ⊧ FAN_{c}

Proof. Suppose that at ⊥ we have a decidable set C ⊆ 2^{∗} inducing a c-bar. We would like to show that at ⊥ the c-bar is uniform, which means that for some k C contains every sequence of length at least k (in notation, C ⊇ 2^{≥k}).

Say that α ∈ 2^{∗} is good if there is a natural number k such that, whenever n ≥ k and β ⊇ α has length at least k, ¬⟨n, β⟩ ⊩ “C ⊇ 2^{≥k}.” Observe that if α^{⌢}0 and α^{⌢}1 are good then so is α (by taking k sufficiently large). So if the empty sequence ⟨⟩ is bad (i.e. not good) then there is a branch Br_{0} of bad nodes. For each α ∈ Br_{0}, by the definition of badness, taking k to be the length | α | of α, we have some β ⊇ α and n ≥| α | and γ ∈ 2^{≥k} such that ¬⟨n, β⟩ ⊩ “γ ∉ C.” By choosing α’s of increasing length, we can get infinitely many γ’s of increasing length, in particular infinitely many distinct γ’s. Hence there is a branch Br_{1} such that each node in Br_{1} has infinitely many γ’s as extensions.

That was all in M. Now in N, pick some non-standard α ∈ Br_{0} such that with regard to the induced fact that ¬⟨n, β⟩ ⊩ “γ ∉ C, ” γ extends some nonstandard node in Br_{1}. Since β ⊇ α and n ≥| α |, and α is non-standard, ⟨n, β⟩ indexes a node in the model. But at ⊥, C induces a c-bar, so ⊥ ⊧ “there is a node δ in Br_{1} such that every extension of δ is in C.” This contradicts the choice of γ.

We conclude from this that ⟨⟩ is good. Fix k witnessing this goodness. It is worth noting that, by the decidability of C, if α has standard length at least k then ⊥ ⊧ “α ∈ C.” So all that needs to be checked to show ⊥ ⊧ “C ⊇ 2^{≥k}” is the finitely many α’s not covered by ⟨⟩’s goodness. Namely, for those α’s of length less than k such that G(α) = ∞, we need to show that for all nonstandard n ⟨n, α⟩ ⊧ “C ⊇ 2^{≥k}”. For that, it suffices to show in M that there is a finite n such that for all m ≥ n ¬⟨m, α⟩ ⊩^{∗} “C ⊇ 2^{≥k}”.

Toward that end, suppose not. Then for infinitely many m there is a γ of length at least k such that ¬⟨m, α⟩ ⊩^{∗} “γ ∉ C”. If those γ’s are of bounded length then one occurs infinitely often. For that fixed γ, by overspill there is a non-standard m such that ¬⟨m, α⟩ ⊩^{∗} “γ ∉ C”. But ⟨m, α⟩ is a Kripke node, and that contradicts the decidability of C. Hence there are infinitely many different γ’s. That means there is a branch Br_{2} such that every node on Br_{2} has infinitely many different γ’s as extensions. Pick a non-standard m such that the induced γ extends a non-standard node of Br_{2}. But again, at ⊥ C induces a c-bar, so ⊥ ⊧ “there is a node δ in Br_{2} such that every extension of δ is in C.” This contradicts the choice of γ.

6 FAN_{Π_{1}^{0}} does not imply FAN_{full}

As usual, let G be generic as above. In M[G], the Kripke model will have bottom node ⊥, and successor nodes labeled by those α ∈ 2^{∗} such that G(α) = ∞. As is standard, terms are defined inductively, and always subject to the usual restrictions so as to have a Kripke model. That is, to define the full model over any partial order ⟨P, <⟩, at node p ∈ P a term σ is any function with domain P^{≥p} such that σ(q) is a set of terms at node q; furthermore, with transition function f_{qr} for q < r, if τ ∈ σ(q) then f_{qr}(τ) ∈ σ(r); finally, f_{pq} is extended to σ by restriction: f_{pq}(σ) = σ ↾ P^{≥q}. That is called the full model, because everything possible is being thrown in. For the current construction, we will take a sub-model of the full model by imposing one additional restriction: a term at any node α other than ⊥ must be in the ground model M.

Let C be the term such that ⊥ ⊧ “β̂ ∈ C” iff for some initial segment β ↾ n of β G(β ↾ n) = IN, and at node α ≠ ⊥ α ⊧ “β̂ ∈ C” iff β is not an initial segment of α.

Lemma 23. ⊥ ⊧ FAN_{Π_{1}^{0}}

Proof. If ⊥ ⊧ “B ⊆ 2^{∗} is decidable” then for any β ∈ 2^{∗} ⊥ ⊧ “β̂ ∈ B” iff for some node α ≠ ⊥ α ⊧ “β̂ ∈ B” iff the same holds for all α ≠ ⊥. Hence ⊥ ⊧ “B = B̂_{M}” for some set B_{M} ∈ M. So if ⊥ ⊧ “B_{n} is a sequence of decidable trees,” then that sequence is the image of a sequence of sets from M. Hence their intersection internally is the image of a set from M. So if ⋂_{n} B_{n} is internally a bar, it is the image of a bar, and by the Fan Theorem in M is uniform.

Lemma 24. ⊥ |̸= FAN_{full}

Proof. At ⊥, C is not uniform, so it suffices to show ⊥ ⊧ “C is a bar”. If ⊥ ⊧ “P is a path through 2^{∗}” then ⊥ ⊧ “P is decidable”, and as above P is then the image of a ground model path. Generically, for some β along that path, G(β) = IN. For that β, ⊥ ⊧ “P goes through β̂ and β̂ ∈ C.

Lemma 25. ⊥ ⊧ IZF

Proof. Immediate.

7 Questions

• We have seen that FAN_{full} holds in every topological model, and that FAN_{Π_{1}^{0}} holds in the model over any connected Heyting algebra. Are there any other sufficient or necessary properties for any of the various fan theorems we have been considering to hold or fail in a Heyting-valued model?

• As a particular instance of the previous question, if a Heyting algebra satisfies FAN_{Δ} (resp. FAN_{c}), does it automatically satisfy FAN_{c} (resp. FAN_{Π_{1}^{0}})?

• Although we were not able to make use of any Heyting algebras other than Ω, some seem worthwhile to investigate, as possibly separating some of these Fan Theorems, or perhaps having some other interesting properties. We would include among these K(T) for various natural spaces T, such as 2^{ℕ}. We would also include other ways of killing points, such as over a measure space τ with measure λ modding out by sets of measure 0:

U ∼ V ⟺ λ(U) = λ(V) = λ(V ∩ U)

(two opens are equivalent if their symmetric difference is of measure zero). The space τ/ ∼ should be a Heyting algebra, which we will denote by analogy with K as L(τ). Of particlar interest seem to be L(I) and L(I×I).

• In the models presented here, the principles in question were not true. That’s different from their being false (meaning their negations being true). We expect this could be done by iterating the constructions presented here. That is, to each terminal node of the model append another model of the same kind, starting with the ambient universe of that terminal node as the new ground model. By iterating this procedure infinitely often, one is left with a Kripke model with no terminal nodes. In order still to have a model of IZF, to get the Power Set Axiom for instance, terms for all of these bars from the iteration would have to be present at ⊥. So this suggestion would take some work to implement.

It would be even better, or at least different, if we had a model with one fixed counter-example. Maybe the models presented here could be so tweaked. For instance, for FAN_{Δ}, could we just throw away the terminal nodes? For FAN_{c}, it might work not to stop a node just because ¬b′ is true, but rather to continue extending the node to allow finitely many ¬b′s to be true. Or maybe a more radical idea is needed.

• Within reverse classical mathematics, many weakenings of Weak König’s Lemma (classically equivalent to the Fan Theorem) have been identified. Of interest to us here is Weak Weak König’s Lemma. Whereas WKL states that any bar (closed under extension, for simplicity) contains an entire level of 2^{∗}, WWKL states that any bar contains half of a level. (WWKL has been shown to be connected to the development of measure theory.) In our context, any of the principles we have been considering could be so weakened, yielding Weak FAN_{Δ}, Weak FAN_{c}, Weak FAN_{Π_{1}^{0}}, and Weak FAN_{full}. Clearly any principle implies its weak correlate (e.g. FAN_{Π_{1}^{0}} implies Weak FAN_{Π_{1}^{0}}), and any weak principle implies the weak principles lower down (e.g. Weak FAN_{Π_{1}^{0}} implies Weak FAN_{c}), forming a bit of a square. Are there any implications along the diagonal (e.g. between FAN_{c} and Weak FAN_{Π_{1}^{0}})? Are these weak principles even natural or interesting, by being equivalent with interesting theorems?

• Are there any other interesting principles to be found here, for instance Π_{n}^{0}-FAN for n > 1, or adaptations of reverse math principles beneath WKL other than WWKL?

References

[1] Michael Beeson, Foundations of Constructive Mathematics, Springer-Verlag, 1985.

[2] Josef Berger, The logical strength of the uniform continuity theorem, Logical approaches to computational barriers, 2006, pp. 35–39.

[3] , A separation result for varieties of brouwer’s fan theorem, Proceedings of the 10th asian logic conference (alc 10), kobe university in kobe, hyogo, japan, september 1-6, 2008, to appear.

[4] Errett Bishop and Douglas Bridges, Constructive Analysis, Springer-Verlag, 1985.

[5] Hannes Diener, Compactness under constructive scrutiny, Ph.D. Thesis, 2008.

[6] Hannes Diener and Iris Loeb, Sequences of real functions on [0, 1] in constructive reverse mathematics, Annals of Pure and Applied Logic 157(1) (2009), pp. 50-61.

[7] M. Fourman and J. Hyland, Sheaf models for analysis, Applications of Sheaves (Michael Fourman, Christopher Mulvey, and Dana Scott, eds.), Lecture Notes in Mathematics, vol. 753, Springer Berlin / Heidelberg, 1979, pp. 280-301.

[8] William Julian and Fred Richman, A uniformly continuous function on [0,1] that is everywhere different from its infimum, Pacific Journal of Mathematics 111(2) (1984), pp. 333-340.

[9] Stephen Simpson, Subsystems of Second Order Arithmetic, ASL/Cambridge University Press, 2009.