IKP and Friends

Robert S. Lubarsky^{∗} 1755 NE 18th St. Ft. Lauderdale, FL 33305 USA Robert.Lubarsky@alum.mit.edu Robert.Lubarsky@att.net

December 2001

1 Introduction

There has been increasing interest in intuitionistic methods over the years. Still, there has been relatively little work on intuitionistic set theory, and most of that has been on intuitionistic ZF. This investigation is about intuitionistic admissibility and theories of similar strength.

There are several more particular goals for this paper. One is just to get some more Kripke models of various set theories out there. Those papers that have dealt with IZF usually were more proof-theoretic in nature, and did not provide models. Furthermore, the inspirations for many of the constructions here are classical forcing arguments. Although the correspondence between the forcing and the Kripke constructions are not made tight, the relationship between these two methods is of interest (see [6] for instance) and some examples, even if only suggestive, should help us better understand the relationship between forcing and Kripke constructions. Along different lines, the subject of least and greatest fixed points of inductive definitions, while of interest to computer scientists, has yet to be studied constructively, and probably holds some surprises. Admissibility is of course the proper set-theoretic context for this study. Finally, while most of the classical material referred to here has long been standard, some of it has not been well codified and may even be unknown, so along the way we’ll even fill in a gap in the classical literature.

∗I would like to thank Anil Nerode for bringing the subject of intuitionistic set theory to my attention, Michael Rathjen for his encouragement in bringing this work to completion, and the referee for the careful reading and insistence on including the details, even when I didn’t think they were necessary.

The next section develops the basics of IKP, including some remarks on fixed points of inductive definitions. After that some classical theories related to KP are presented, and the question of which imply which others is completely characterized. While they are not equivalent in general, when restricted to initial segments of (classical) L they are. However, the section after that shows that in intuitionistic L this equivalence breaks down. We close with some questions.

2 IKP

The axioms of classical KP are: Empty Set, Pairing, Union, Extensionality, Foundation (as a schema for all definable classes), Δ_{0} Comprehension (also known as Δ_{0} Separation), and Δ_{0} Bounding (also known as Δ_{0} Collection). Often Infinity is adjoined; we will also use the axiomatisation with Infinity in this paper. There is not much trouble adapting these to an intuitionistic setting. The concept of a Δ_{0} formula needs no change. As usual, Foundation must be replaced by ∈-Induction: ∀x(∀y ∈ x ϕ(y) → ϕ(x)) → ∀x ϕ(x), where ϕ is a formula in the language of set theory. Also, the standard version of Infinity, as in [9] for instance (∃x [(∃y y ∈ x) ∧ (∀y ∈ x ∃z ∈ x y ∈ z)]), won’t do, because you need Power Set and Π_{1} Comprehension to get ω; instead, take the version of Infinity from [7] (∃x [0 ∈ x ∧ ∀y ∈ x ∃z ∈ x(z = y ∪ {y}) ∧ ∀y ∈ x(y = 0 ∨ ∃z ∈ x y = z ∪ {z})]), which axiomatizes ω straightforwardly. We take IKP to be KP with these few adaptations.

This choice can be further justified. Two other axiomatizations of KP are to replace Δ_{0} Bounding with either Σ Bounding or Σ Reflection. Taking the Σ formulas to be the closure of the Δ_{0} formulas under ∧, ∨, ∃, and bounded quantification, these equivalences hold intuitionistically, for the same reasons they do classically. Rather than repeating these completely standard arguments here, the reader is referred to [1], theorems I.4.3 and I.4.4, the proofs of which go through unchanged in IKP. In addition, under IKP every Σ formula is equivalent to a Σ_{1} formula, proven inductively on formulas.

One could also consider many of the standard consequences of KP. The ones of interest to us are:

1. Σ Replacement,

2. Strong Σ Replacement,

3. Δ Comprehension,

4. Σ Recursion,

5. the Second Recursion Theorem, and

6. Σ Inductive Definitions.

Σ Replacement and Strong Σ Replacement (∀x ∈ A ∃y ϕ(x, y) → ∃f ∀x ∈ A f(x) ≠ ∅ ∧ ∀y ∈ f(x) ϕ(x, y)) hold intuitionistically, by the same proofs as in the classical case; again, the reader is referred to [1], theorems I.4.6 and I.4.7. Δ Comprehension requires considerably more care. Usually a Δ property is defined as being given by a pair ϕ, ψ of Σ and Π formulas respectively, but when it’s used the first thing you do is deal with ¬ψ as a Σ formula. This won’t work intuitionistically. The next obvious guess at what a Δ property should be is a pair ϕ, ψ of Σ formulas such that ∀x [(ϕ(x) ∨ ψ(x)) ∧ ¬(ϕ(x) ∧ ψ(x))]. The problem here is that too much is being demanded: such a definition would be almost impossible to meet. Consider a very simple property, such as “x = ∅”. What would be a Δ definition of this, according to the above notion of Δ? If ϕ(x) is “x = ∅” and ψ(x) is “x ≠ ∅” then we certainly do not have ∀x (ϕ(x)∨ψ(x)). To address these (and other) problems, we will be content with defining Δ_{1}, noting that Σ resp. Π formulas are under IKP provably equivalent to Σ_{1} resp. Π_{1} formulas. A Δ_{1} property of a variable x is given by a pair of Δ_{0} formulas ϕ(x, y), ψ(x, y) with free variables x,y such that

∀x[∃y¬¬(ϕ(x, y) ∨ ψ(x, y)) ∧ ∀y¬(ϕ(x, y) ∧ ψ(x, y))].

With this notion of Δ_{1}, Δ_{1} Comprehension is provable in IKP; see [1] theorem I.4.5.

That a function defined by Σ recursion is Σ_{1} definable holds in both KP and IKP; again, the proof from [1], theorem I.6.4 holds. The Second Recursion Theorem, as stated and proved in [1] V.2, pretty much stands as is, except that when syntax and semantics are introduced in ch. III all of the standard Boolean connectives must be included as primitives (since, for instance, in our context → cannot be defined in terms of ¬ and ∨). The fact that the least fixed point of a positive inductive Σ definition is Σ_{1} definable actually requires a bit of care in one point, so the development of this theory will be summarized here, with the reader referred to [1] for the details.

In IZF, suppose Γ : P(X) → P(X) is a monotone inductive operator on X. Consider {Y |Γ(Y) ⊆ Y }. This set is non-empty, since it contains X itself as a member. Let Γ_{fix} = ⋂{Y |Γ(Y) ⊆ Y }. By the monotonicity of Γ, Γ(Γ_{fix}) ⊆ Γ_{fix}. Applying Γ again we get ΓΓ(Γ_{fix}) ⊆ ΓΓ_{fix}, so Γ(Γ_{fix}) ∈ {Y |Γ(Y) ⊆ Y }, and Γ_{fix} ⊆ Γ(Γ_{fix}). Hence Γ_{fix} = Γ(Γ_{fix}), and Γ_{fix} is a fixed point. Moreover, by its definition, Γ_{fix} is the least fixed point. Γ_{fix} can also be defined from the bottom up. Inductively on ordinals β, let Γ_{<β} = ⋃_{α<β} Γ_{α}, Γ_{β} = Γ(Γ_{<β}). (Note the standard way to induct on ordinals intuitionistically, which avoids the successor-or-limit case split.) Let Γ_{∞} = ⋃_{β∈ORD} Γ_{β}, which can be shown to be a set using Bounding. (Note that Replacement will not do! Let ψ(Y, β) be “Y = Γ_{β}”; since such a β cannot be uniquely chosen, we need (Comprehension and) Bounding in order to get a range for ψ, a set A of ordinals such that ∀Y ⊆ X if ∃β Y = Γ_{β} then ∃β ∈ A Y = Γ_{β}. Letting γ = TC(A), Γ_{∞} = Γ_{γ}. This is where the current argument differs from its classical version, and recurs when discussing admissible sets proper.) It’s easy to see that Γ_{β} ⊆ Γ_{fix}, inductively on β, and that Γ_{∞} is a fixed point, making Γ_{∞} equal to Γ_{fix}.

Now particularize to the case where Γ is given by an X-positive Σ formula ψ: Γ(Y) = { x ∈ X | ψ(x, X) }. (What follows is adapted from [1], VI.2.6.) If M is admissible (i.e. M ⊧ IKP), then, letting α = ORD(M), Γ_{∞} = Γ_{<α}, as follows. In M, the relation “x ∈ Γ_{β}” is a Σ_{1} relation, using the Second Recursion Theorem. So ϕ(x, Γ_{<α}) is a Σ relation, where “y ∈ Γ_{<α}” is interpreted as “∃β y ∈ Γ_{β}”. If ϕ(x, Γ_{<α}) holds, then, by Σ Bounding, there is a set of ordinals A ∈ M such that ϕ(x, ⋃_{β∈A} Γ_{β}) holds. Letting γ = TC(A), ϕ(x, Γ_{<γ}), and x ∈ Γ_{γ}. So Γ_{α} = Γ_{<α} is a fixed point. Since Γ_{<α} ⊆ Γ_{∞} too, Γ_{<α} = Γ_{∞}. It has already been observed that Γ_{<α} is Σ_{1} definable over M.

So where are the differences between KP and IKP? Typically properties that a classical set theorist identifies automatically become inequivalent in an intuitionistic setting. No one would believe that every property around admissibility has the same status in IKP.

If one of the pleasures of intuitionism is to surprise our intuitions, then you’re in for a treat. You would have expected to find some difference between KP and IKP among the most common properties, those already cited. So there’s no use having the differences there, where you’re already looking for them. Rather, the differences show up where you’d never think to check, right under your nose. Consider the basic axiom, Δ_{0} Bounding:

∀x ∈ A ∃y ϕ(x, y) → ∃B ∀x ∈ A ∃y ∈ B ϕ(x, y), ϕ ∈ Δ_{0}.

Consider the contrapositive with the negations pushed through (the “classical contrapositive”, with ϕ absorbing the negation):

∀B ∃x ∈ A ∀y ∈ B ϕ(x, y) → ∃x ∈ A ∀y ϕ(x, y), ϕ ∈ Δ_{0}.

We call this latter property Δ_{0} Uniformity. Of course classically Δ_{0} Uniformity and Δ_{0} Bounding are equivalent as contrapositives, but intuitionistically they’re not, as we’ll see later.

An alternative to Δ_{0} Bounding classically is Σ Reflection:

ϕ → ∃A ϕ^{(A)}, ϕ ∈ Σ,

where the superscript means bound all as yet unbound quantifiers by the superscript. The classical contrapositive is:

∀A ϕ^{(A)} → ϕ, ϕ ∈ Π.

The latter property is called Π Persistence. Finally, regarding the last alternative axiomatization of KP, Σ Bounding, its classical contrapositive is Π Uniformity.

Proposition 2.0.1 Over IKP - Δ_{0} Bounding, the following are equivalent:

1. Π Persistence

2. Π Uniformity

3. Δ_{0} Uniformity.

proof: In what follows, we will rely heavily on the fact that, for ϕ a Π formula, if B ⊆ A then ϕ^{(A)} → ϕ^{(B)}. This is proved by induction on Π formulas. The same also holds for A = V: if B is a set, then ϕ → ϕ^{(B)}.

(1) → (2) Suppose that ∀B ∃x ∈ A ∀y ∈ B ϕ(x, y), ϕ a Π formula. By the above mentioned fact, ∀B ∃x ∈ A ∀y ∈ B ϕ(x, y)^{(B)}, i.e. ∀B (∃x ∈ A ∀y ϕ(x, y))^{(B)}. By Π Persistence, ∃x ∈ A ∀y ϕ(x, y), as was to be shown.

(2) → (3) trivial

(3) → (1) We show that Π Persistence holds for all Π formulas ϕ by induction on ϕ.

The base case, ϕ Δ_{0}, is trivial, since ϕ^{(A)} = ϕ.

Suppose ϕ = ψ_{0} ∨ψ_{1}. Assume ∀A(ψ_{0} ∨ψ_{1})^{(A)}, which equals ∀A(ψ_{0}^{(A)} ∨ψ_{1}^{(A)}). We claim that ∀B ∃x ∈ {0, 1} ∀y ∈ B ((x = 0 ∧ ψ_{0}^{(y)}) ∨ (x = 1 ∧ ψ_{1}^{(y)})). To see this, by assumption ∀A(ψ_{0}^{(A)} ∨ ψ_{1}^{(A)}); letting be A be ⋃ B, we have

ψ_{0}^{(⋃ B)} ∨ ψ_{1}^{(⋃ B)}. If ψ_{0}^{(⋃ B)} let x be 0, and note that ψ_{0}^{(⋃ B)} → ψ_{0}^{(y)} since

y ⊆ ⋃ B. Similarly if ψ_{1}^{(⋃ B)}. Applying Δ_{0} Uniformity to the claim, we get ∃x ∈ {0, 1} ∀y ((x = 0∧ψ_{0}^{(y)})∨(x = 1∧ψ_{1}^{(y)})). If the value of x which witnesses this sentence is 0, then ∀y ψ_{0}^{(y)}, and by induction ψ_{0}. Similarly, if the value of x which witnesses this sentence is 1, we get ψ_{1}. Since either 0 or 1 witnesses this sentence, ψ_{0} ∨ ψ_{1}, as was to be shown.

Suppose ϕ = ∃u ∈ v ψ. Assume ∀A(∃u ∈ v ψ)^{(A)}, which equals ∀A ∃u ∈ v ψ^{(A)}. We claim ∀B ∃u ∈ v ∀y ∈ B ψ^{(y)}. To see this, again use the assumption with A = ⋃B. By Δ_{0} Uniformity, ∃u ∈ v ∀y ψ^{(y)}, and by induction ∃u ∈ v ψ.

The other cases are easier. If ϕ = ψ_{0} ∧ ψ_{1}, ∀A(ψ_{0} ∧ ψ_{1})^{(A)} = ∀A(ψ_{0}^{(A)} ∧ ψ_{1}^{(A)}) → ∀Aψ_{0}^{(A)} ∧∀Aψ_{1}^{(A)} → (by induction) ψ_{0} ∧ψ_{1}. If ϕ = ∀u ∈ v ψ, ∀A (∀u ∈ v ψ)^{(A)} = ∀A ∀u ∈ v ψ^{(A)} → ∀u ∈ v ∀A ψ^{(A)} → (by induction) ∀u ∈ v ψ. Finally, if ϕ = ∀u ψ, suppose ∀A (∀u ψ)^{(A)} which equals ∀A (∀u ∈ A ψ^{(A)}). It follows that ∀u ∀B ψ^{(B)}: for arbitrary values v and C for u and B respectively, let A = C ∪ {v} in the assumption above, yielding ∀u ∈ C ∪ {v} ψ^{(C∪{v})}(u). In particular, for u = v, ψ^{(C∪{v})}(v), and, shrinking the bound, ψ^{(C)}(v). So ∀u ∀B ψ^{(B)}(u), and, by induction, ∀u ψ(u).

In what follows, Π Persistence will refer to the theory IKP - Δ_{0} Bounding + Π Persistence (or Π Uniformity or Δ_{0} Uniformity, from the proposition), as well as to the axiom scheme, except when such an ambiguity might cause confusion.

Although KP and Π Persistence are equivalent classically, intuitionistically they are (implicationally) incomparable, as follows. To see that IKP does not imply Π Persistence, consider the partial order that has a bottom element ⊥ and ω-many incomparable nodes n (n ≥ 1) larger than it. Let the Kripke structure M have L_{ω_{1}^{CK}} at ⊥, L_{ω_{n}^{CK}} (ω_{n}^{CK} being the nth admissible ordinal) at n, and Id for transition functions. ⊥ ⊧ IKP, as follows. M_{⊥} already contains ∅ and ω, and the universe at each node is closed under pairing and union. These universes are also transitive sets, and the ∈-relation of M is merely a restriction of ∈ (of V), so Extensionality and Foundation hold. Both Δ_{0} Comprehension and Δ_{0} Bounding are based on the fact that sets in M don’t grow, or, to put it more formally, M_{n} is an end-extension of M_{⊥}. As a consequence, Excluded Middle holds in M for Δ_{0} formulas. So for Δ_{0} Comprehension, suppose ϕ(x) is a Δ_{0} formula with parameters from M_{⊥} = L_{ω_{1}^{CK}}, and X ∈ M_{⊥}. Let A = { x ∈ X | ϕ(x)}. A ∈ L_{ω_{1}^{CK}} = M_{⊥}, and ⊥ ⊧ “ A = { x ∈ X | ϕ(x)}”. Regarding Δ_{0} Bounding, if ⊥ ⊧ “f is total” then 1 ⊧ “f is total”, and L_{ω_{1}^{CK}} ⊧ “f is total”. By the admissibility of L_{ω_{1}^{CK}}, A = rng(f) ∈ L_{ω_{1}^{CK}}. By Excluded Middle and Absoluteness for Δ_{0} formulas, ⊥ ⊧ “A = rng(f)”. But Δ_{0} Uniformity fails: ⊥ ⊧ ∀a (∃n ∈ ω ∀x ∈ a if x is a sequence of admissible ordinals then length(x) < n), but ⊥ |̸= ∃n ∈ ω ∀x (if x is a sequence of admissible ordinals then length(x) < n).

In the other direction, consider ω as a partial order, and let α_{n} be an ωsequence cofinal in ω_{1}^{CK}. Let the Kripke model M have L_{α_{n}} at node n (with Id as the transition functions). It is easy to see that no node forces IKP: given n, just pick a witness that L_{α_{n}} is not admissible, such a witness being a Δ_{0} function unbounded in L_{α_{n}}. But Π Persistence holds: Suppose for a node n, n ⊧ “∀A ϕ^{(A)}” (and hence the same for all nodes m, m ≥ n). For A ∈ L_{α_{n}}, ϕ^{(A)} is Δ_{0}, and M_{m} is an end-extension of M_{n} for m ≥ n; this means that the truth of ϕ^{(A)} can be determined locally, i.e. L_{α_{n}} ⊧ ϕ^{(A)}. “A” ranges over all sets in L_{α_{m}} for all m ≥ n, hence over L_{ω_{1}^{CK}}, so we have L_{ω_{1}^{CK}} ⊧ ∀A ϕ^{(A)}. By Π Persistence classically, L_{ω_{1}^{CK}} ⊧ ϕ. In showing that n ⊧ ϕ, when unraveling ϕ choices will have to be made, with ∃ and ∨. Use the truth of ϕ in L_{ω_{1}^{CK}} as a guide.

So we have two different theories, IKP and Π Persistence. Is there a difference between the mathematics you can do in them? Yes, again by duality. We have already seen that in IKP the least fixed point of a positive inductive Σ definition is Σ_{1} definable. Classically it would follow that the greatest fixed point of a positive inductive Π definition is Π_{1} definable. However, intuitionistically, this latter property seems to require Π Persistence as well as IKP.

In a bit more detail, if Γ : P(X) → P(X) is a monotone inductive operator on X, let A be {Y |Y ⊆ Γ(Y)} and Γ_{fix} = ⋃ A. By the monotonicity of Γ, Γ_{fix} ⊆ Γ(Γ_{fix}). Applying Γ again, Γ(Γ_{fix}) ⊆ Γ(Γ(Γ_{fix})), so Γ(Γ_{fix}) ∈ A and Γ(Γ_{fix}) ⊆ Γ_{fix}. Hence Γ_{fix} = Γ(Γ_{fix}), and Γ_{fix} is a fixed point. Moreover, by its definition, Γ_{fix} is the greatest fixed point. From the bottom up, let Γ_{<β} = ⋂_{α<β} Γ_{α}, Γ_{β} = Γ(Γ_{<β}), and Γ_{∞} = ⋂_{β∈ORD} Γ_{β}. Γ_{fix} ⊆ Γ_{β}, by induction on β, and Γ_{∞} is a fixed point, so Γ_{fix} = Γ_{∞}. If Γ is given by a Π formula ϕ, then, over IKP + Π Persistence, “x ∈ Γ_{β}” is a Π relation, by the duals of the arguments for the Σ case. (This can be seen by adapting [1], III.1 and V.1 and 2. The satisfaction relation M ⊧ ϕ[s] is Δ_{1} over IKP. That the universal Π predicate Π-Sat(ϕ, s) can be defined as “∀Aϕ^{(A)}[s]” uses Π Persistence. This fact is then plugged into the dual to the proof of the Second Recursion Theorem to get that for all R-positive Π formulas ϕ(x, y, R) there is a Π formula ψ(x, y) such that ψ(x, y) iff ψ(x, y, λx.ψ(x, y)). This suffices to get “x ∈ Γ_{β}” to be a Π relation of x and β.) Let M ⊧ IKP + Π Persistence, and α = ORD(M). The claim is that Γ_{<α} = Γ_{α}. To see this, suppose x ∈ Γ_{<α}, i.e. M ⊧ ∀βϕ(x, Γ_{<β}), a Π relation. Letting Γ_{A} be ⋂_{α∈A∩ORD} Γ_{α}, M ⊧ ∀Aϕ(x, Γ_{A}) (because β can be chosen to be TC(A) ∩ ORD, and then Γ_{<β} ⊆ Γ_{A}), and M ⊧ ∀A ϕ^{(A)}(x, Γ_{A}). By Π Persistence, M ⊧ ϕ(x, Γ_{<α}), so x ∈ Γ_{α} and Γ_{<α} ⊆ Γ_{α}. On general principles Γ_{α} ⊆ Γ_{<α}, so Γ_{α} = Γ_{<α}, and Γ_{<α} is a fixed point. Since Γ_{<α} ⊇ Γ_{∞}, Γ_{<α} = Γ_{∞}.

So, while IKP suffices to get least fixed points to be Σ_{1} definable, it seems as though Π Persistence is necessary to get greatest fixed points to be Π_{1} definable (although, to be fair, such necessity has yet to be proven). Furthermore, the second of the models above, intended to show that Π Persistence does not imply IKP, also shows that Π Persistence doesn’t prove that lfp’s are Σ_{1} definable (Kleene’s O has an appropriate inductive definition but is not Σ_{1} definable over M.). So these two constructions, least and greatest fixed point, so near to each other classically, are apparently more easily splittable intuitionistically. This matter will be pursued in the questions at the end of this paper.

It bears observation that Π Persistence, as a theory, is quite weak, in that one cannot easily construct sets in it. For instance, it does not even prove the totality of the function α ↦ L_{α}, as the following model shows. Let ⟨ α_{n} | n ∈ ω ⟩ be a strictly increasing sequence of limit ordinals cofinal in ω_{1}^{CK}. For X a set, let Pair(X) be the set of all pairs from X (including singletons, as degenerate pairs), Union(X) the set of all unions from X (i.e. {⋃ x | x ∈ X}), and Δ_{0}(X) the set of all Δ_{0}-definable subsets of members of X (assume here that X is transitive, just for simplicity). Let Close(X) be X ∪ Pair(X) ∪ Union(X) ∪ Δ_{0}(X). The Kripke model under construction has for its partial order an increasing ω-sequence. For node n, start with X_{0} = L_{α_{n}} ∪ α_{n+1}, and let X_{m+1} = Close(X_{m}). The n^{th} node is ⋃_{m}X_{m} (with the inclusion function as the transition functions). IKP - Δ_{0} Bounding is easily seen to hold, as is Π Persistence, by the same argument as in the second model above. But α_{n} is an ordinal at every node n and L_{α_{n}} isn’t a set until node n+1. (To see that L_{α_{n}} is not a set at node n, show inductively on m that for all finite Y ⊆ X_{m} L_{α_{n}} ⊈ TC(Y).)

It is an interesting question whether IKP + Π Persistence - Δ_{0} Bounding proves the Π_{1} definability of greatest fixed points of positive inductive Π definitions, or whether the full power of IKP + Π Persistence is needed. The status of Π Persistence will be further pursued in the questions at the end.

3 Classical Friends

In the following section we will turn to the intuitionistic versions of various theories related to KP. Since these classical theories are not all well known, though, a brief discussion of them for their own sakes is in order.

The axioms of interest to us are:

1. Σ_{1} Dependent Choice: If ϕ(x, y) is Σ_{1}, and ∀x ∃y ϕ(x, y), then there is a function f with domain ω such that ∀n ϕ(f(n), f(n+1)).

2. Resolvability: There is a Δ_{1} definable function f on the ordinals such that V = ⋃range(f).

3. Π_{2} Reflection: If ∀x ∃y ϕ(x, y), ϕ ∈ Δ_{0}, then for every A there is a B ⊇ A such that ∀x ∈ B ∃y ∈ B ϕ(x, y).

4. Δ_{0} Bounding: from KP.

The implicational relations among these theories are as follows:

Σ_{1} DC + KP

↘

Π_{2} Reflection + KP → KP ↗

Resolvability + KP

Over the base theory KP - Δ_{0} Bounding, Resolvability alone implies nothing of interest; after all, L_{λ} for any arbitrary limit λ is resolvable. Similarly, Σ_{1} DC alone is rather weak, as L_{ω_{1}·2} models Σ_{1} DC (because cf(ω_{1} · 2) > ω). However, over this base theory Π_{2} Reflection itself picks up Δ_{0} Bounding.

All of these implications are easy to prove; for details see [1]. Furthermore, in L they are all equivalent; this is also easy, and can be found in [1]. However, if an implication does not follow from the preceding then it is not in general true. Some of these non-implications are easy to see, and must certainly already be known if not written down; others are actually a bit tricky. In any event these proofs are not so easy to find in the literature, and they also provide the models for the proofs in the next section, so it is well to include them here. (For background on forcing, as well as arguments similar to those that follow, including the use of symmetric submodels to falsify the Axiom of Choice, the reader is referred to [4] and [5].)

1. Resolvability + KP + ¬Σ_{1} DC: Adjoin to L_{ω_{1}^{CK}} (or, for that matter, to L ⊧ ZF, for the stronger result Resolvability + ZF + ¬Σ_{1} DC) ω-many Cohen reals (that is, reals generic for the forcing partial order 2^{<ω}), as well as the set (not sequence!) G consisting of all those reals. This is a symmetric submodel of the model obtained by the set forcing to add an ω-sequence of Cohen reals, hence is admissible. It is already a standard argument (see [5]) that not even all of ZF is enough to build an ω-sequence of distinct elements of G. This violation of the Axiom of Choice is actually a violation of Σ_{1} DC: let ϕ(x, y) be “if x is a sequence of distinct elements of G then y is one also and is a proper end-extension of x”. The function which shows Resolvability is f(α) = L_{α}[G].

2. Σ_{1} DC + KP + ¬Resolvability: Adjoin to L_{ω_{1}^{CK}} any finite subset G_{fin} of a countable set G of Cohen reals, and take the union of all such adjunctions: M = ⋃_{G_{fin}⊆G, G_{fin}finite} L_{ω_{1}^{CK}} [G_{fin}]. Σ_{1} DC and Δ_{0} Bounding hold, as follows. It suffices to consider formulas of the form ∃yϕ(x, y), with ϕ(x, y) a Δ_{0} formula. If ∃yϕ(x, y) holds for a particular set x, then let G_{fin} ⊆ G be the finite set of those reals used in the construction of x and of ϕ’s parameters (i.e. ∃yϕ(x, y) is a formula over L_{ω_{1}^{CK}} [G_{fin}]). We claim there is a witness y not merely in M, as hypothesized, but already in L_{ω_{1}^{CK}} [G_{fin}]. To see this, let y witness ∃yϕ(x, y) in M. Let G_{y} ⊇ G_{fin} be a finite set such that y ∈ L_{ω_{1}^{CK}} [G_{y}]. By the absoluteness of Δ_{0} formulas, L_{ω_{1}^{CK}} [G_{y}] ⊧ ϕ(x, y); again by absoluteness, L_{α}[G_{y}] ⊧ ϕ(x, y) for some α < ω_{1}^{CK}. G_{y}\ G_{fin} is generic over L_{ω_{1}^{CK}} [G_{fin}] (for the forcing p.o. which is the product of finitely many copies of 2^{<ω}), hence the last assertion is forced over L_{ω_{1}^{CK}} [G_{fin}] by some condition p: p |⊢ “L_{α}[G_{y}] ⊧ ϕ(x, ẙ)”, where ẙ is a name for y. In L_{ω_{1}^{CK}} [G_{fin}] a generic over L_{α}[G_{fin}] through p can be built (by the countability of L_{α}[G_{fin}] in L_{ω_{1}^{CK}} [G_{fin}]); let G_{α} be such a generic. Then L_{α}[G_{fin}, G_{α}] ⊧ ϕ(x, ẙ(G_{α})), where “ẙ(G_{α})” refers to the interpretation of ẙ with the canonical name for the generic interpreted as G_{α}. By the absoluteness of Δ_{0} formulas L_{ω_{1}^{CK}} [G_{fin}] ⊧ ϕ(x, ẙ(G_{α})), and L_{ω_{1}^{CK}} [G_{fin}] ⊧ ∃y ϕ(x, y). Now it’s easy to see that Σ_{1} DC holds in M. If M ⊧ “∀x∃yϕ(x, y)”, ϕ ∈ Δ_{0}, then L_{ω_{1}^{CK}} [G_{fin}] models the same. L_{ω_{1}^{CK}} [G_{fin}] also satisfies Σ_{1} DC, so contains an appropriate ω-sequence, which by absoluteness also works in M. Δ_{0} Bounding is similar.

Resolvability fails, as follows. Let f be a function over M (given via a Δ_{1} definition) with domain ORD^{M}. Let G_{fin} be a finite subset of G such that all of f’s parameters are in L_{ω_{1}^{CK}} [G_{fin}]. By the same argument as in the last paragraph, since f is total over M, the same Δ_{1} definition produces the same total function over L_{ω_{1}^{CK}} [G_{fin}]. So ⋃ range(f) ⊆ L_{ω_{1}^{CK}} [G_{fin}], which itself is a proper subset of M, so ⋃ range(f) ≠ M.

3. Π_{2}-Reflection + ¬Σ_{1}DC + ¬Resolvability: This is a combination of the previous two arguments. To construct M, first adjoin an infinite set G of Cohen reals, then all possible finite subsets of another such infinite set H. Σ_{1} DC and Resolvability fail as before. Π_{2} Reflection holds for much the same reason that Σ_{1} DC did in the previous example. If M ⊧ ∃yϕ(x, y) then all you need to build such a y is G and the finite subset H_{fin} of H used for x and ϕ. So if M ⊧ “∀x∃y ϕ(x, y)”, ϕ ∈ Δ_{0}, and if A ∈ M, then L_{ω_{1}^{CK}} [G, H_{fin}] ⊧ “∀x∃y ϕ(x, y)” (H_{fin} merely being large enough to contain all of the reals in H needed to construct ϕ’s parameters and A). Since L_{ω_{1}^{CK}} [G, H_{fin}] satisfies Π_{2} Reflection, it contains an appropriate B ⊇ A, as desired.

4. KP + ¬Π_{2}-Reflection: The model from [8] suffices, and will be described briefly here. A Steel generic tree over L_{ω_{1}^{CK}} is not well-founded but has no infinite descending sequence in the generic extension. This forcing can be modified slightly to include a distinguished path through the tree which does not destroy admissibility. Force an ω-sequence of such trees < T_{n} > and paths < B_{n} >. Let W be a recursive linear ordering of ω which is not well-founded but has no hyperarithmetic infinite descending sequence. Think of the trees as ordered by W. Let M_{i} be L_{ω_{1}^{CK}} [< T_{n} | n ∈ ω >, < B_{n} | n ≥_{W} i >]. M = ⋃_{i∈I} M_{i} for I some final segment of W with no least element, chosen exactly so that M is admissible. In [8] it was observed that M falsifies Σ_{1} DC; in fact it’s even Π_{2} Reflection that fails: M ⊧ “∀j if there is a branch through T_{j} then ∃i <_{W} j and a branch through T_{i}”, but any set in M is a set in some M_{i}, in which W is still well-founded.

4 Intuitionistic Models

As remarked in the introduction, even though the constructions just given show that none of these theories are equivalent to each other in general, in L they all are. However, intuitionistically the ordinals do funny things. With Kripke models there is an extra degree of freedom, the choice of the partial order. If the underlying partial order is chosen to be some forcing partial order, then by coding forcing conditions as small ordinals one could reasonably hope to get a generic G, although still not in V, actually in L^{V [G]}. This is basically the approach followed in the upcoming arguments. Notice, though, that these intuitions are not made precise. In particular, of the four constructions from the preceding section, only three are adapted here, because we couldn’t see how to do the fourth. The omitted one is Σ_{1} DC + KP + V=L + ¬Resolvability, the problem being Σ_{1} DC. There’s no trouble picking some least set in classical L, but IL does not apparently come equipped with a well-founded linear order.

4.1 General Considerations

There will be some common constructions in these models. It would be well to isolate them, as well as to give some of the standard background on IORD and IL.

4.1.1 Intuitionistic Ordinals

Intuitionistically, an ordinal is a transitive set of transitive sets. The standard weak counter-example to show that the ordinals are not linearly ordered goes as follows. Let α = {0 | ϕ}. α is an ordinal. If the ordinals are linearly ordered, then α ∈ 0, α = 0, or 0 ∈ α. The first case is not possible, since 0 is the empty set. In the second case, ¬ϕ. In the last case, ϕ. So ϕ ∨ ¬ϕ. Hence if Excluded Middle is to fail, then the ordinals are not linearly ordered. It is not hard to give examples of non-classical ordinals in Kripke models. Let P be any partial order. A trivial Kripke structure on P has some universe of sets M (with M’s ∈-relation) at each node and the identity function as the transition functions. (Think of M as a model of ZF, or a weaker set theory, or even the universe V for a class-sized Kripke structure. A class-sized Kripke structure is like a Kripke structure, but rather than requiring that the relations and functions in question (e.g. “is a set at node σ”, or the transition functions between nodes) be sets, they must merely be definable relations on a definable subset of V.) Consider a larger or ambient Kripke structure, that is, a structure with the same partial order P but more sets at each node. Any set in this ambient structure which at each node contains only ordinals from the trivial Kripke structure is an intuitionistic ordinal which cannot be construed as classical.

4.1.2 Intuitionistic Definability

Regarding IL, definability can be developed within IZF much as it is classically, so def(X), the set of definable subsets of a set X, makes perfect sense. As usual, the definition of L_{α} cannot depend on whether α is a limit or a successor, since intuitionistically not every ordinal is a limit or a successor. So L_{α} is ⋃_{β∈α} def(L_{β}). For details see [7]. In what follows, however, we will typically not be dealing with L as an inner model of an already given model of IZF, which is merely the semantic version of L’s axiomatic development in IZF, hence implicit in [7]. Rather, L will be handled sui generis: given a Kripke structure M for the language of set theory, we will have occasion to consider def(M). While not difficult, this could stand some exposition.

So suppose M is an extensional (x = y iff ∀z z ∈ x ↔ z ∈ y) Kripke structure (with relations ∈ and =), with underlying partial order P, universe M_{σ} at node σ, and transition functions f_{στ} : M_{σ} → M_{τ}. In def(M), a set at node σ is named by a formula ϕ(x) with free variable x and parameters from M. A set is actually an equivalence class of such formulas, in which ϕ ∼_{σ} ψ if σ ⊧_{M} ∀x [ϕ(x) ↔ ψ(x)]. f_{στ} : def(M_{σ}) → def(M_{τ}) is given by the equation

f_{στ} ([ϕ(x, y_{1}, ..., y_{n})]_{σ}) = [ϕ(x, f_{στ} (y_{1}), ..., f_{στ} (y_{n}))]_{τ} ,

where y_{1}, ..., y_{n} are the parameters, and the notation f_{στ} is used ambiguously for transition functions in both M and def(M). f_{στ} is well-defined, because if ϕ ∼_{σ} ψ, that is, if σ ⊧_{M} ∀x [ϕ(x, y_{1}, ..., y_{n}) ↔ ψ(x, z_{1}, ..., z_{m})], then, by general lemmas on Kripke models, τ ⊧_{M} ∀x [ϕ(x, f_{στ} (y_{1}), ..., f_{στ} (y_{n})) ↔ ψ(x, f_{στ} (z_{1}), ..., f_{στ} (z_{m}))] (σ ≤ τ), or ϕ ∼_{τ} ψ. M_{σ} can be embedded in def(M_{σ}), with y being identified with the formula “x ∈ y”. This much being said, ∈ can now be interpreted: [ϕ]_{σ} ∈ [ψ]_{σ} iff [ϕ]_{σ} = [y]_{σ} for some y ∈ M_{σ} and σ ⊧_{M} ψ(y). (Notice that this definition is independent of the choice of representative for [ψ]_{σ}, by the definition of the equivalence relation; furthermore, there is at most one y such that y ∼_{σ} ϕ, by the extensionality of M.) Extensionality holds in def(M): σ ⊧_{def(M)} ∀x (x ∈ [ϕ]_{σ} ↔ x ∈ [ψ]_{σ}) iff ∀τ ≥ σ ∀x ∈ M_{τ} τ ⊧_{def(M)} [x] ∈ [ϕ]_{τ} ↔ [x] ∈ [ψ]_{τ} iff ∀τ ≥ σ ∀x ∈ M_{τ} τ ⊧_{M} ϕ(x) ↔ ψ(x) iff σ ⊧_{M} ∀x [ϕ(x) ↔ ψ(x)] iff [ϕ]_{σ} = [ψ]_{σ}.

To summarize, if M is an extensional Kripke structure for the language of set theory, so is def(M), and M can be canonically embedded in def(M). Furthermore, def(M) can be construed as an end-extension of M, since if σ ⊧_{def(M)} [ϕ]_{σ} ∈ [y]_{σ} then [ϕ]_{σ} = [z]_{σ} for some z ∈ M_{σ} and σ ⊧_{M} z ∈ y. Also, this process can be iterated through the transfinite: starting with M_{0} = M, let M_{α+1} = def(M_{α}) and M_{λ} = →^{lim} {M_{α} | α < λ} (or, more colloquially, ⋃_{α<λ} M_{α}). M_{λ} is also an extensional Kripke model end-extending each M_{α}.

Indeed, this process can be iterated not only along a well-founded linear order, but also along a well-founded partial order. Suppose that X is a Kripke structure (for the language of set theory) with underlying partial order P, and that the partial order defined by

(σ, x) ≥ (τ, y) ↔ σ ≤_{P} τ ∧ τ ⊧ y ∈ f_{στ} (x)

(σ, τ ∈ P, x ∈ X_{σ}, y ∈ X_{τ}) is well-founded. Then “def” can be iterated along this p.o., as follows. Suppose inductively that for all (τ, y) ≤ (σ, x) def(M_{(τ,y)}) is well-defined as a Kripke structure on the partial order P_{≥τ}. Then M_{(σ,x)} can be defined as follows:

(M_{(σ,x)})_{τ} = ⋃_{{y|τ⊧y∈f_{στ} (x)}}(def(M_{(τ,y)}))_{τ} .

Regarding the transition functions, consider [ϕ(z, y_{1}, ..., y_{n})]_{τ} ∈ (M_{(σ,x)})_{τ}. Then

[ϕ(z, y_{1}, ..., y_{n})]_{τ} ∈ (def((M_{(τ,y)}))_{τ}

where τ ⊧ y ∈ f_{στ} (x). Then let

f_{τρ}([ϕ(z, y_{1}, ..., y_{n})]_{τ}) := [ϕ(z, f_{τρ}(y_{1}), ..., f_{τρ}(y_{n}))]_{ρ},

since

[ϕ(z)]_{ρ} ∈ (def(M_{(ρ,f_{τρ}(y))}))_{ρ} ⊆ (M_{(σ,x)})_{ρ},

the latter inclusion because ρ ⊧ f_{τρ}(y) ∈ f_{τρ}(f_{στ} (x)) = f_{σρ}(x).

With M_{(σ,x)} now defined, def(M_{(σ,x)}) follows, using the “def” operator developed earlier in this section. The final structure M_{X} is then given by

(M_{X})_{σ} = ⋃_{x∈X_{σ}}(def(M_{(σ,x)}))_{σ}.

At this point a few words about absoluteness are in order. For starters, the external concept “def” developed above is equivalent to the internal concept “def”. In more detail, suppose that V is some classical meta-universe, and M∈V is an extensional Kripke structure for the language of set theory, and N = def(M), again in V. Suppose that K is a Kripke structure with the same underlying partial order as M and N such that M, N ∈ K (so M and N are sets in the sense of K). Then K ⊧ N = def(M), where of course “def” in this case is the traditional, internal concept of definability. We will not prove this here; hopefully the external development of “def” was transparent enough to make this assertion clear. This allows us in the following to be ambiguous as to which version of “def” is intended.

Furthermore, the same holds for the iterations of “def”, both into the transfinite as well as along a well-founded partial order. In the first case, suppose α is an ordinal and K a Kripke structure for the language of set theory (both in our classical meta-universe V, of course). Suppose that there is an α_{K} ∈ K_{σ}, σ ∈ P, such that (α, ∈_{V}) and (α_{K}, ∈_{K_{σ}}) are isomorphic, and that, for all τ ≥ σ, f_{στ} : α_{K} → f_{στ} (α_{K}) is an isomorphism. Then σ ⊧ “α_{K} is an ordinal”, and α_{K} can be identified with α. Notice that this is nothing other than the extension of the already common practice of using the notation “0” to denote the empty set both in V and in a Kripke model, “1” as {0} again in V or in a Kripke model, etc., and even “ω” for the ω of a Kripke model, so long as it contains only the internalizations of the standard natural numbers. In addition, for M, N ∈ K_{σ}, if N = M_{α} (the α-fold iteration of def, as defined above, of course interpreted in V), then σ ⊧ N = M_{α_{K}}. (This applies, of course, only when K has enough set-theoretic power to express α-fold iteration of definability, e.g. in models of IKP (see [7]).) In such a case we will feel free to use the notation α for both the external and internal ordinal.

Regarding iterations along well-founded partial orders, let X be as above (that is, a Kripke structure over P well-founded in the manner previously described). Let N = M_{X}, of course in V, and let K be a Kripke structure containing X, M, and N as members. If K satisfies a sufficiently large fragment of IZF then the X-fold iteration of def (notation: X-def) would be definable and provably total. The inductive definition of “X-def” is none other than the already well-known notion of the iteration of definability along an ordinal (i.e. L_{α}), the point being that α’s ordinalhood is unnecessary for the intelligibility of the notion: X-def(M) = ⋃_{Y ∈X} def(Y-def(M)). The result, again stated without proof, is that K ⊧ N = X-def(M).

A case of particular interest is when K ⊧ “X is an ordinal”. Under this circumstance we will use the more common notation α instead of X. For M take the structure 0 = ∅^{K} (equivalently, let 0 be the unique function from P to {∅}). Then there is already standard notation for α-def(0), namely L_{α}. This being the case, we will use the notation “L_{α}” for 0_{α} for those α’s as above which are ordinals in some Kripke structure, even if such Kripke structure has not yet been introduced in the exposition. Then “L_{α}” can be interpreted either externally or internally, as the occasion demands. (To keep the reader from being distracted by concerns that any given α will indeed turn out to be an ordinal in some ambient Kripke structure introduced in some unspecified future section, please observe that ordinality is a Δ_{0} property for transitive sets, the only kind we will be considering, and hence can be determined locally. We will even go so far as to say that a transitive Kripke structure α is an ordinal (or a Kripke ordinal) when it satisfies the intuitionistic definition of such, a transitive set of transitive sets, even in the absence of an ambient Kripke universe, knowing that such an α will be an ordinal in any ambient Kripke structure.)

4.1.3 General Constructions

In the following sections we will be constructing several Kripke models. Here we bring together several steps common to them, in order not to have to do them more than once. In every case we will begin by giving the underlying partial order P; the steps given here are generic and applicable to all P’s, assuming only that P has a bottom element ⊥. (After corollary 4.1.3, we will impose more restrictions on P. Of course for the constructions themselves in future sections, we will specify P explicitly.) Then we will define certain Kripke ordinals with underlying partial order P. These ordinals will be based on the generic reals from the classical forcing constructions of the last section; they will be a kind of internalization of these reals, and will be very low in the power set hierarchy (being collections of subsets of 1 = {0}). It should be noted that the constructions here and in the coming sections take place of necessity in V: the only Kripke structures in sight are those being built, and so of no use in their own definitions.

Given a node σ in P, let 1_{σ} be the set (Kripke set, if you will, as 1_{σ} will end up being a set in a Kripke structure) that looks like 0 unless you’re past or incompatible with σ, where it’s 1:

[τ ⊧ x ∈ 1_{σ}] ↔ [σ < τ ∨ σ ⊥ τ] ∧ [τ ⊧ x = ∅],

or, if you prefer,

(1_{σ})_{τ} = ∅ ↔ τ ≤ σ
(1_{σ})_{τ} = {∅} ↔ [σ < τ ∨ σ ⊥ τ],

with the only possible transition functions (cf. the remark after definition 4.1.5). 1_{σ} is an ordinal: ⊥ ⊧ “if x ∈ 1_{σ} then x = ∅”; since nothing is in ∅, 1_{σ} is transitive, and ∅ is transitive. (Recall that the intuitionistic definition of an ordinal as a transitive set of transitive sets is Δ_{0} for transitive sets, and so can be determined locally, without an ambient Kripke structure.) So L_{1_{σ}} is well-defined. What is L_{1_{σ}}? If τ ⊧ x ∈ L_{1_{σ}}, then, for some β, τ ⊧ x ∈ def(L_{β}) ∧ β ∈ 1_{σ}. If τ ≤ σ then τ |̸= β ∈ 1_{σ}, so τ |̸= x ∈ L_{1_{σ}} for any x, and L_{1_{σ}} looks empty. Otherwise τ ⊧ β ∈ 1_{σ} iff τ ⊧ β = ∅. ⊥ ⊧ L_{0} = ∅, and ⊥ ⊧ def(L_{0}) = {∅}. So if τ ⊧ x ∈ L_{1_{σ}} then τ ⊧ x = ∅. In short, L_{1_{σ}} = 1_{σ}.

Furthermore, what’s definable over 1_{σ}? Recall that when taking definitions over a set, truth is evaluated in that set: a definable subset of 1_{σ} is one of the form { x ∈ 1_{σ} | 1_{σ} ⊧ ϕ(x) }, where ϕ’s parameters must also come from 1_{σ}. So if both τ_{0}, τ_{1} ≤ σ then τ_{0} ⊧ “1_{σ} ⊧ ϕ(x)” iff τ_{1} ⊧ “1_{σ} ⊧ ϕ(x)”; i.e. τ_{0} and τ_{1} force the same atomic facts about definable subsets of 1_{σ}. Similarly if both τ_{0} and τ_{1} extend or are incompatible with σ. Since 1_{σ}’s only possible member is ∅, the only possible member of a subset of 1_{σ} is ∅; by the preceding remarks, either ∅ is in a given subset at all nodes beyond or incompatible with σ or it’s not. So def(L_{1_{σ}}) = {0, 1_{σ}}.

Let T be {1_{σ} | σ ∈ P} (in V). Let T̂ be a Kripke subset of T, that is, T̂_{σ} ⊆ T and the transition functions are all the identity. Let T̂_{0} be such that (T̂_{0})_{σ} = T̂_{σ} ∪ {0}. T̂_{0} is an ordinal: T is a set of ordinals, so T̂ ⊆ T is also, as is T̂_{0}. So T̂_{0} is a set of transitive sets. It is also transitive itself: if τ ⊧ x ∈ y ∈ T̂_{0}, then either τ ⊧ y = 0, which contradicts τ ⊧ x ∈ y, or τ ⊧ y ∈ T̂, i.e. τ ⊧ y = 1_{σ} for some σ, and τ ⊧ x = 0, and 0 ∈ T̂_{0}.

Lemma 4.1.1 LT̂_{0} = T̂_{0}

proof: LT̂_{0} = ⋃_{α∈T̂_{0}} def(L_{α}) = [⋃_{α∈T̂} def(L_{α})] ∪ def(L_{0}) = [⋃_{1_{σ}∈T̂} def(L_{1_{σ}})] ∪ {0} = ⋃_{1_{σ}∈T̂}{0, 1_{σ}} ∪ {0} = T̂_{0}

Corollary 4.1.2 T̂ is definable over LT̂_{0}.

proof: T̂ = T̂_{0} − {0} = {x | x ≠ 0} as a definition over T̂_{0}, since, for all σ, ⊥ ⊧ 1_{σ} ≠ 0.

Corollary 4.1.3 Suppose {T̂_{i} | i ∈ I} is a collection of Kripke subsets of T. Then {T̂_{i0} | i ∈ I} ∪ ⋃ {T̂_{i0} | i ∈ I} is an ordinal, say ξ, and ∀i T̂_{i} ∈ L_{ξ}.

Now suppose that P (the underlying partial order of the Kripke structure to be built) is a tree of height ω. Also assume that P is nowhere degenerate, meaning that each node has incompatible extensions. Much of what follows would work in a more general context, but we have no need of such a detailed investigation. We would like some internal notion of a branch through P; that is, a Kripke set that behaves as such. Given an external branch B (that is, a branch through P in the classical sense), the obvious internalization of B would be {1_{σ} | σ ∈ B}. But if τ is perpendicular to any member of B, then at node τ this looks like {1}. Even worse, ¬¬ B = {1}, and it’s not possible to get two such branches forced at any node to be unequal. Hence we would like branches that reappear even after you’ve fallen off of them.

In the following, we explicitly distinguish between those definitions and lemmas that of necessity are to be evaluated in V (labeled “external”), because they refer to non-Kripke objects, and those, labeled “internal”, that can be evaluated in an appropriate Kripke structure (meaning one containing certain parameters or satisfying certain exioms from IZF).

Definition 4.1.4 (external) P̂ is the full Kripke subset of T; that is, P̂_{σ} = T.

The following Kripke-internal definition is Δ_{0}, and hence can be evaluated and applied (such as in the definition and lemma thereafter) in any transitive Kripke set containing P̂ even without an ambient Kripke universe. (Cf. the comments on ordinality at the end of section 4.1.2.)

Definition 4.1.5 (internal) B ⊆ P̂ is a branch through P̂ if

1. α ⊇ β ∈ B → α ∈ B,

2. ∀α, β ∈ B α ⊆ β ∨ β ⊆ α, and

3. ∀γ ∈ P̂ ((∀β ∈ B (γ ⊆ β ∨ β ⊆ γ)) → γ ∈ B).

The reader may have wondered why 1_{σ} was taken as being 1 at nodes incompatible with σ, instead of 0, which might first have come to mind. The answer is clause 1) in the definition above. Otherwise, if we had defined (1_{σ})_{τ} = ∅ for τ ⊥ σ, then consider what would hold of a branch, i.e. let ρ ⊧ “B is a branch through P̂”. By clause 3) ρ ⊧ “B ≠ ∅”, so let σ be such that ρ ⊧ “1_{σ} ∈ B”. In practice it will be easy to extend ρ to τ ⊥ σ; then τ ⊧ “1_{σ} ∈ B”. τ ⊧ “1_{σ} = 0” because P is a tree (i.e. ∀τ′ ≥ τ τ′ ⊥ σ), so τ ⊧ “0 ∈ B”. By clause 1) then τ ⊧ “B = P̂”, which would then run afoul of clause 2). So in order to have branches at all, 1_{σ} needed to be defined as it was.

Definition 4.1.6 (external) If σ ⊧ U ⊆ P̂ then for τ ≥ σ ext_{τ} (U) = {ρ ≥ τ | τ ⊧ 1_{ρ} ∈ U}: “the externalisation of U at τ”.

Lemma 4.1.7 (external) σ ⊧ “B is a branch through P̂” iff for all τ ≥ σ ext_{τ} (B) is a branch through P_{≥τ} and 1_{⊥} ∈ B_{σ}.

proof: Recall that the notation Tr_{≥τ} for a tree Tr means the subtree of nodes extending τ (including τ itself) and the notation X_{σ} for a Kripke set X refers to the collection of elements forced at σ into X. Recall also that a branch of a tree classically is a non-empty, linearly ordered subset of a tree which is closed downwards and (if the tree has no terminal leaves, as in our context) has no final element.

→ : Suppose τ ≥ σ.

a) ext_{τ} (B) is non-empty: For τ = ⊥ ⊥ ⊧ “∀β ∈ P̂ β ⊆ 1_{⊥}”. By clause 3) in the definition of a branch, ⊥ ⊧ “1_{⊥} ∈ B”, so ⊥ ∈ ext_{⊥}(B). For τ ≠ ⊥ τ ⊧ “∀β ∈ P̂ β = 1 ∨ β ⊆ 1_{τ} ”. Again by clause 3), τ ⊧ “1_{τ} ∈ B”, and τ ∈ ext_{τ} (B).

b) ext_{τ} (B) is linearly ordered: Suppose ρ, ξ ∈ ext_{τ} (B). Then τ ⊧ “1_{ρ}, 1_{ξ} ∈ B”. By clause 2) in the definition of a branch, τ ⊧ “1_{ρ} ⊆ 1_{ξ} ∨ 1_{ξ} ⊆ 1_{ρ}”. If ρ and ξ were incompatible, then ρ |̸= “1_{ξ} ⊆ 1_{ρ}” and ξ |̸= “1_{ρ} ⊆ 1_{ξ}”. This, however, contradicts the semantics of “∨” in Kripke structures, by which one of the two disjuncts must hold. Hence ρ and ξ are compatible.

c) ext_{τ} (B) is closed downwards: Suppose ρ ∈ ext_{τ} (B) and τ ≤ ξ ≤ ρ. Then τ ⊧ “1_{ρ} ∈ B” and τ ⊧ “1_{ρ} ⊆ 1_{ξ}”. By clause 1) in the definition of a branch, τ ⊧ “1_{ξ} ∈ B”, and ξ ∈ ext_{τ} (B).

d) ext_{τ} (B) has no final element: Suppose to the contrary that ρ is the final element of ext_{τ} (B). Consider ext_{ρ}(B). From the proof of part a) above, ρ ∈ ext_{ρ}(B). If ext_{ρ}(B) = {ρ}, then let π be an immediate successor of ρ (which exists since P was assumed to have an ordinal height and no degenerate nodes; see the comments after corollary 4.1.3). Again from part a), we have already seen that π ⊧ “∀β ∈ P̂ β = 1 ∨ β ⊆ 1_{π}”; since branches are, by definition, subsets of P̂, we have in particular π ⊧ “∀β ∈ B 1_{π} ⊆ β ∨ β ⊆ 1_{π}”. At an extension ξ of ρ incompatible with π, ξ ⊧ “1_{π} = 1”, so ξ ⊧ “∀β ∈ B β ⊆ 1_{π}”. Finally, at ρ itself, the only element forced at ρ into B is, by hypothesis, 1_{ρ}, and ρ ⊧ “1_{π} ⊆ 1_{ρ}”. To summarize, ρ ⊧ “∀β ∈ B 1_{π} ⊆ β ∨ β ⊆ 1_{π}”. By clause 3), ρ ⊧ “1_{π} ∈ B”, and π ∈ ext_{ρ}(B), contrary to hypothesis. So ext_{ρ}(B) ≠ {ρ}.

Let π ≠ ρ be some member of ext_{ρ}(B). We will show that π ∈ ext_{τ} (B), contradicting the choice of ρ as the final element of ext_{τ} (B). This argument, once again, uses clause 3). Our goal is to show that τ ⊧ “∀β ∈ B 1_{π} ⊆ β ∨ β ⊆ 1_{π}”. Once that is accomplished, it follows that τ ⊧ “1_{π} ∈ B”, which means π ∈ ext_{τ} (B).

So let ξ ≥ τ. If ξ and ρ are incompatible, then so are ξ and π (π extends ρ). So ξ ⊧ “1_{π} = 1”, and 1 is a superset of every member of P̂. If ξ and ρ are compatible, then either ρ ≤ ξ or τ ≤ ξ < ρ. In the first case, ξ ⊧ “1_{π} ∈ B”, because ρ models the same. By clause 2) in the definition of a branch, ξ ⊧ “∀β ∈ B 1_{π} ⊆ β ∨ β ⊆ 1_{π}”. In the second case, τ ≤ ξ < ρ, we have in any case ξ ⊧ “1_{ρ} ∈ B”, because τ models the same. If ξ ⊧ “β ∈ B”, then by clause 2) ξ ⊧ “1_{ρ} ⊆ β ∨ β ⊆ 1_{ρ}”. If ξ ⊧ “1_{ρ} ⊆ β” then ξ ⊧ “1_{π} ⊆ β”, because ξ ⊧ “1_{π} ⊆ 1_{ρ}”. If, on the other hand, ξ ⊧ “β ⊆ 1_{ρ}”, then ρ ⊧ “β ⊆ 1_{ρ}”. That implies that β = 1_{μ} for some μ ≥ ρ. Furthermore, by clause 2), ρ ⊧ “1_{π} ⊆ 1_{μ}” or ρ ⊧ “1_{μ} ⊆ 1_{π}”. In the first case we have π ≥ μ, in the second μ ≥ π, and in either case ξ ⊧ “1_{π} ⊆ 1_{μ}” or ξ ⊧ “1_{μ} ⊆ 1_{π}”.

Finally, for this direction of the proof it remains to show that 1_{⊥} ∈ B_{σ}. ⊥ ⊧ “∀β ∈ P̂ β ⊆ 1_{⊥}”. By clause 3), σ ⊧ “1_{⊥} ∈ B”.

←:

1. σ ⊧ “α ⊇ β ∈ B → α ∈ B”: Suppose σ ⊧ “1_{τ} ⊇ 1_{ρ} ∈ B”. If τ⊥σ or τ < σ then σ ⊧ “1_{τ} = 1 = 1_{⊥} ∈ B”. Otherwise τ ≥ σ. Then τ ≤ ρ, because otherwise τ ⊧ “1_{ρ} = 1” and τ |̸= “1_{τ} = 1”. Since ρ ∈ ext_{σ}(B), which is by hypothesis a branch, and hence closed downwards, we have τ ∈ ext_{σ}(B), i.e. σ ⊧ “1_{τ} ∈ B”.

2. σ ⊧ “∀α, β ∈ B α ⊆ β ∨ β ⊆ α”: Suppose σ ⊧ “1_{τ} , 1_{ρ} ∈ B”. If τ⊥σ or τ < σ then σ ⊧ “1_{τ} = 1 ⊇ 1_{ρ}”. Similarly if ρ⊥σ or ρ < σ. So τ, ρ ≥ σ. By hypothesis τ, ρ ∈ ext_{σ}(B), which is a branch, and hence linearly ordered; therefore τ ≤ ρ or ρ ≤ τ, implying ⊥ ⊧ “ρ ⊆ τ” or ⊥ ⊧ “τ ⊆ ρ” respectively.

3. σ ⊧ “∀γ ∈ P̂ (∀β ∈ B γ ⊆ β ∨ β ⊆ γ → γ ∈ B)”: Suppose σ ⊧ “∀β ∈ B 1_{τ} ⊆ β ∨ β ⊆ 1_{τ} ”. If τ⊥σ or τ < σ then σ ⊧ “1_{τ} = 1 = 1_{⊥} ∈ B”. Otherwise τ ≥ σ. If τ were incompatible with some ρ ∈ ext_{σ}(B), then τ |̸= “1_{ρ} ⊆ 1_{τ} ” and ρ |̸= “1_{τ} ⊆ 1_{ρ}”, yielding σ |̸= “1_{τ} ⊆ 1_{ρ} ∨ 1_{ρ} ⊆ 1_{τ} ”, contrary to the hypothesis. Since ext_{σ}(B) as a branch is a maximal linearly ordered subset of P_{≥σ}, τ ∈ ext_{σ}(B), and σ ⊧ “1_{τ} ∈ B”.

4.2 Resolvability + IKP + V=L + ¬Σ_{1} DC

To be perfectly clear, we really should state what Resolvability means in this context. The standard definition, that there is a Δ_{1}-definable function f : ORD → V such that V = ⋃ rng(f), is perfectly coherent, but could be contested as not being the appropriate correlate to classical resolvability in an intuitionistic setting. After all, maybe the linearity of the domain is what’s vital, so a resolution should have domain some linearly ordered set of ordinals, presumably a Δ_{1} definable set of ordinals. We will take the latter as the definition of a resolution, because it seems to be a more difficult definition to fit (although it is not clear that a function defined on a Δ_{1} set of ordinals could be extended to all the ordinals), and point out that if V = L then α ↦ L_{α} shows resolvability according to the former notion of a resolution. In fact, the resolution we will be offering will even be extendable to a Δ_{1} function on the whole model.

The underlying partial order of the model will be 2^{<ω}, with the order being end-extension (σ < τ iff τ is a proper end-extension of σ.). For each real R : ω → 2 there is a canonical branch B(R) through T:

ext_{τ} (B(R)) = {ρ ≥ τ | ∀j length(τ) ≤ j < length(ρ) → τ(j) = R(j)},

or, equivalently,

B(R)_{τ} = {1_{ρ} | ρ < τ ∨ ρ ⊥ τ ∨ (ρ ≥ τ ∧ ∀j length(τ) ≤ j < length(ρ) → τ(j) = R(j))}.

B(R) is a branch by the preceding lemma. Notice that if R_{0} and R_{1} differ cofinally then ⊥ ⊧ B(R_{0}) ≠ B(R_{1}).

Start with a model V of classical ZF. Let G := {G_{i} | i ∈ ω} be a set of reals mutually Cohen-generic over V (that is, reals generic for the forcing partial order 2^{<ω}). Actually, the rest of this section save the last lemma applies just as well to any set of (mutually cofinally differing) reals. (This last fact we will use in section 4.4, where many constructions and lemmas similar to those below are used, often with the offered proof being merely a reference to the corresponding proof here, even though the real there is not even generic.) In V[G], construct the (Kripke) branches B(G_{i}), i ∈ ω. For convenience, call the branch B(G_{i}) just B_{i}. Consider {B_{i} | i ∈ ω} ∪ {P̂}. Let ξ be the (Kripke) ordinal from corollary 4.1.3 applied to this set; in particular, each B_{i} and P̂ is a member of L_{ξ}.

Lemma 4.2.1 {B_{i} | i ∈ ω} is definable over L_{ξ}, as the set of branches through P̂.

proof: L_{ξ} = ⋃_{α∈P̂_{0}} def(L_{α}) ∪ ⋃_{i∈ω} def(L_{B_{i0}}) ∪ def(LP̂_{0}). The first union is just P̂_{0}, by lemma 4.1.1, which doesn’t contain a branch. Each term in the second union, def(L_{B_{i0}}), is just def(B_{i0}), again by 4.1.1. No branch contains 0, because, if it did, by clause 1) in the definition of a branch, it would then contain all of P̂, contradicting clause 2). So any branch which is a subset of B_{i0} is also a subset of B_{i}. But B_{i} is itself a branch, and no proper subset of a branch is a branch, because of clause 3), as follows. Suppose B is a branch, B̂ ⊆ B, and B̂ is also a branch. If γ ∈ B and β ∈ B̂, β ∈ B too; using that B is a branch, γ ⊆ β or β ⊆ γ by clause 2). Since B̂ is a branch, γ ∈ B̂ by clause 3). So B ⊆ B̂, and B = B̂. In the final case, def(LP̂_{0}), or, more simply, again by 4.1.1, def(P̂_{0}), consider any definition, say ϕ(x), over P̂_{0}. It contains only finitely many parameters 1_{σ}. Go to a node τ beyond or incompatible with all such σ’s. τ ⊧ ϕ(1_{ρ}) for some extension ρ of τ iff τ ⊧ ϕ(1_{ρ}) for all extensions ρ of τ of the same length, by symmetry. (There is an automorphism of P̂_{0} switching any given pair of ρ’s.) So ϕ does not define a branch.

The model M can now be defined inductively:

M_{0} = L_{ξ};

M_{α+1} = def(M_{α});

M_{λ} = ⋃_{α<λ} M_{α}; and

M = M_{ω_{1}^{CK}} .

Lemma 4.2.2 M ⊧ IKP. proof: Most of the axioms depend on the fact that if β > α then M_{β} is an endextension of M_{α}. For instance, as has already been mentioned, M_{α} is proven to be extensional inductively on α, using this end-extension property for the limit cases. As another example, consider Pairing. If y, z ∈ M, let α be such that y, z ∈ M_{α}. Now consider [“x = y ∨ x = z”] ∈ M_{α+1}. This set is the pair {y, z} in M_{α+1}; since M end-extends M_{α+1}, the same fact holds in M. Empty and Union are similar. Δ_{0} Comprehension also depends on this, being the reason Δ_{0} formulas are absolute between M_{α} and M. (So if ϕ(x) is Δ_{0}, and all of its parameters, as well as X, are in M_{α}, then [x ∈ X ∧ ϕ(x)] ∈ M_{α+1} is the desired subset in M.) Even Foundation uses end-extensionality. Suppose M |̸= Foundation. Let ϕ and σ be such that σ ⊧ ∀x((∀y ∈ x ϕ(y)) → ϕ(x)) and σ |̸= ∀x ϕ(x). Let τ ≥ σ and x ∈ (M_{α})_{τ} be such that τ |̸= ϕ(x); moreover, assume that α is the least such ordinal. By the choice of α, if y ∈ (M_{β})_{ξ} (β < α) then ξ ⊧ ϕ(y). By end-extensionality, if ξ ⊧ y ∈ x then y ∈ M_{β}, some β < α. So τ ⊧ ∀y ∈ x ϕ(y), hence, by hypothesis, τ ⊧ ϕ(x), a contradiction. So M ⊧ Foundation.

For Δ_{0} Bounding, M can be considered to be constructed by a Σ_{1} induction over the standard L_{ω_{1}^{CK}} [G], so any Δ_{0}(M) formula ϕ is equivalent to a Δ_{0}(L_{ω_{1}^{CK}} [G]) formula ϕ^{∗}. (This would be proven inductively on formulas, with, for instance, ϕ → ψ going to ∀σ ∈ 2^{<ω}σ ⊧ ϕ → σ ⊧ ψ. The important observation is that only bounded quantifiers are added.) So if M ⊧ “∀x ∈ A ∃y ϕ(x, y)” then in L_{ω_{1}^{CK}} [G] ∀x ∈_{M} A ∃α ∃y ∈ M_{α} ϕ^{∗}(x, y), and by the admissibility of L_{ω_{1}^{CK}} [G] the α’s needed can be bounded.

M also satisfies Infinity. To see this, define inductively on n ∈ ω the set \overline{n} ∈ M, the internal version of n, as follows: \overline{0} = ∅^{M}, \overline{n + 1} = (n ∪ \{n\})^{M}. Inductively, \overline{n} ∈ M_{n}; in fact, \overline{n + 2} ∈ M_{n}. Definably over M_{ω}, let \overline{ω} be \{α | α is an ordinal, and either α = 0 or α is a successor, and ∀β ∈ α β is 0 or a successor\}. \overline{ω} witnesses that M ⊧ Infinity; moreover, one can show inductively that \overline{ω} ∩ M_{n} = \{\overline{m} | m ≤ n + 2\}, so \overline{ω} = \{\overline{n} | n ∈ ω\}.

Lemma 4.2.3 M is resolvable.

proof: The resolution of M will be along \overline{ω_{1}^{CK}}, which is meant as the internalization of ω_{1}^{CK}, as \overline{ω} is for ω. \overline{ω_{1}^{CK}} is defined (in V[G]) as \{ \overline{α} | α < ω_{1}^{CK} \}, where \overline{α} ∈ M is \{ \overline{β} | β < α \}. We need to show that for α < ω_{1}^{CK} \overline{α} ∈ M. Say that an M-ordinal is standard if it’s 0, the successor of a standard ordinal, or an \overline{ω}- limit of standard ordinals. Notice that this definition is internal to M. By the Second Recursion Theorem, there is a Σ definition of standardness in M. Inductively on α ≥ ω, the standard ordinals in M_{α} are a subset of \overline{α}. To show that for α < ω_{1}^{CK}, \overline{α} ∈ M, assume inductively that for β < α \overline{β} ∈ M. By the admissibility of the ambient universe (i.e. L_{ω_{1}^{CK}} [G]), there is a γ such that for each β < α both \overline{β} and a witness that \overline{β} is standard are in M_{γ}. (Here, a witness to standardness is a witness to the Σ definition of standardness.) Then either \overline{α} is definable over M_{γ} as the set of standard ordinals, or \overline{α} is already in M_{γ}. Hence \overline{ω_{1}^{CK}} ⊆ M.

In order to have a resolution along \overline{ω_{1}^{CK}}, we need it Δ_{1} definable. It’s already Σ definable, as the set of standard ordinals. But the witnesses to standardness are not really far away from \overline{α} itself. That is, classically, a witness to the standardness of α, consisting of suitable predecessors and cofinal ω-sequences, could be found in L_{α+ω}. So to see whether \overline{α} is standard in M, look in L_{\overline{α}+\overline{ω}}. The function α ↦ L_{α} is total in M⊧ IKP (see [7]), so the Σ_{1} definition of “α is not standard” is “there is a set L_{α+\overline{ω}} and there is no witness in that set that α is standard”. The Σ definition of standardness is equivalent to a Σ_{1} formula. Now we need to check that this suffices for the notion of Δ_{1} defined earlier. Recall that toward the beginning of section 2 a Δ_{1} property of a variable x was defined as being given by a pair of Δ_{0} formulas ϕ(x, y), ψ(x, y) with free variables x, y such that

∀x[∃y¬¬(ϕ(x, y) ∨ ψ(x, y)) ∧ ∀y¬(ϕ(x, y) ∧ ψ(x, y))].

So let ϕ(x, y) be

x ∈ ORD ∧ y = ⟨z_{0}, z_{1}⟩ ∧ z_{1} witnesses that z_{0} = L_{x+\overline{ω}}
∧ ∃w ∈ z_{0} w witnesses that x is standard,

and ψ(x, y) be

(x ∉ ORD) ∨ (x ∈ ORD ∧ y = ⟨z_{0}, z_{1}⟩ ∧ z_{1} witnesses that z_{0} = L_{x+\overline{ω}}

∧ ∀w ∈ z_{0} w does not witness that x is standard),

where “x + α” is defined inductively on α even for non-ordinals x in the obvious way. For ordinals x there is certainly a y as desired, and it is also clear that ∀x ¬¬(x ∈ ORD ∨ x ∉ ORD). The challenge presented by the formalism as set up is that the y must be chosen before it is decided whether x is an ordinal or not. Here we have to use the development from the penultimate paragraph of section 4.1.2, in which iterations of definability along well-founded (and not necessarily well-ordered) lengths were developed. Let z_{0} be (x + \overline{ω})-def(0) and z_{1} an appropriate construction of such. If x ever turns out to be an ordinal, then z_{0} is automatically L_{x+\overline{ω}}. With this ϕ and ψ, the notion “α is standard” is shown to be Δ_{1} definable.

From here, the resolution of M is its very definition. L_{ξ} is needed as a parameter, which is no problem because it exists as a set in M: L_{ξ} is definable over M_{0} = L_{ξ} as { x | x = x }, and so is in M_{1}. “Y = ⋃X” is a Σ relation, as is “Y = def(X)” (for details on the latter, see [7]). So α → M_{α} is definable via Σ recursion as a Σ relation, hence Σ_{1} also. Any Σ_{1} definable function is Δ_{1}, even with the notion of Δ_{1} operable here, for the same reason as in the classical context, as follows. Suppose the relation f(x) = y is definable as ∃z ϕ(x, y, z). Then let ψ(x, y, w, z) be ϕ(x, w, z) ∧ y ≠ w. Then indeed

∀x, y[∃w, z¬¬(ϕ(x, y, z) ∨ ψ(x, y, w, z)) ∧ ∀w, z¬(ϕ(x, y, z) ∧ ψ(x, y, w, z))].

Hence M is resolvable.

Lemma 4.2.4 M ⊧ V=L.

proof: First observe that L^{M} ⊧ IKP. Extensionality and Foundation hold, because L^{M} is a definable sub-class of a model of Extensionality and Foundation. Pairing is simple: if x ∈ L_{α} and y ∈ L_{β} then x, y ∈ L_{α∪β}, and {x, y} ∈ def(L_{α∪β}) = L_{(α∪β)+1}. Union is similar: if x ∈ L_{α} then ⋃ x ∈ def(L_{α}) = L_{α+1}. ∅ ∈ def(L_{0}) = L_{1}, and \overline{ω} ∈ def(L\overline{ω}) = L_{\overline{ω}+1} to satisfy Infinity; for details on the latter, see [7]. For Δ_{0} Comprehension, consider { x ∈ X | ϕ(x) }, ϕ a Δ_{0} formula. Let α be such that L_{α} contains X as well as ϕ’s parameters. Then { x ∈ X | ϕ(x) } ∈ def(L_{α}) = L_{α+1}. Even Δ_{0} Bounding is smooth. Suppose ∀x ∈ X ∃y ∈ L^{M} ϕ(x, y), ϕΔ_{0}. In M, ∀x ∈ X ∃α ∃y ∈ L_{α} ϕ(x, y). By Σ Bounding in M, let A be a set of ordinals such that ∀x ∈ X ∃α ∈ A ∃y ∈ L_{α} ϕ(x, y). Let β = A ∪ ⋃A. ∀x ∈ X ∃y ∈ L_{β} ϕ(x, y), and L_{β} ∈ L^{M}, showing Δ_{0} Bounding.

For any α < ω_{1}^{CK}, since \overline{α} ∈ M, L\overline{α} ∈ M. \overline{α} is definable over L\overline{α}, so \overline{α} ∈ L^{M}. Also, {B_{i} | i ∈ ω} ∈ M, as is P̂, so ξ ∈ M, and L_{ξ} ∈ L^{M}. Finally, induction shows that any admissible set containing L_{ξ} as well as each \overline{α} < \overline{ω_{1}^{CK}} must contain all of M. The crucial fact needed in this induction is that the function X ↦ def(X) is Δ_{1} definable, provably in IKP. This was essentially done in [7], even though it was not flagged as such. There it was shown, in IZF, that this function in Δ_{1} over all β > α_{aug} + 7, where X ∈ L_{α_{aug}} and α_{aug} is defined inductively as ⋃{γ_{aug} | γ ∈ α} ∪ {α} ∪ (ω + 1). (The purpose of this definition is to get ω into α, hereditarily, as the carrier of syntax.) The proof is that a witness to “Y = def(X)” is definable over L_{α_{aug}+7}, so IZF isn’t necessary; all you need is some ordinal containing as a member α_{aug} + 7. Moreover, the recursion theorem shows that in IKP + Infinity the function α ↦ α_{aug} + 7 is total. So in IKP, X ↦ def(X) is Δ_{1}. This allows the inductive proof that M_{α} ∈ L^{M}, α ∈ ω_{1}^{CK}.

Lemma 4.2.5 M ⊧ ¬Σ_{1} DC.

proof: This is where we will use the particular choice of the G_{i}’s. Consider the relation ϕ(X, Y) “if X is an n-tuple of distinct elements of {B_{i} | i ∈ ω} then Y is an end-extension of X also of distinct elements”. Any function f with domain ω satisfying ϕ(f(i), f(i+1)) (and starting from ∅) would easily produce an ω-sequence through {G_{i} | i ∈ ω} of distinct elements, of which there are none in V[G], much less L_{ω_{1}^{CK}} [G], to say nothing of M.

4.3 Π_{2}-Reflection + IKP + V=L + ¬Σ_{1}DC + ¬Resolvability

Recall the definition of a resolution (see section 4.2) as being a Δ_{1}-definable function f : O→V such that V = ⋃rng(f) and O ⊆ ORD is Δ_{1}-definable and linearly ordered. In the last section, the argument works just as well for this definition as for the classical one (O = ORD, of course not mentioning the requirement of the linear order). Here, though, it wouldn’t. If V = L then f(α) = L_{α} is a classical resolution of V. Hence the need here for a non-classical notion of a resolution.

The underlying partial order is 2^{<ω}, as before.

Let G and H be countable sets of mutual Cohen generics. The ambient universe will be ⋃_{H_{fin}} L_{ω_{1}^{CK}} [G ∪ H_{fin}], where H_{fin} ranges over the finite subsets of H. Within this universe the full intuitionistic model M_{big} can be defined inductively, just like forcing: a set at stage α is a function that, for each node σ ∈ 2^{<ω}, picks out a collection of sets from stages < α (and this collection must grow as σ grows).

More precisely, suppose M is an extensional Kripke model (for the language of set theory) with underlying partial order P and transition functions f_{στ} within a classical universe V. P(M), the power set of M, can be defined similarly to the way def(M) was defined in section 4.1. A set in P(M) at a node σ is a function f with domain P_{≥σ} such that f(τ) ⊆ M_{τ}, and if x ∈ f(σ) then f_{στ} (x) ∈ f(τ). The transition function f_{στ} is restriction: f_{στ} (f) = f ↑ P_{≥τ}. M can be embedded in P(M), with x ∈ M_{σ} being identified with the function f such that f(τ) = { y ∈ M_{τ} | y ∈ f_{στ} (x) }. By the extensionality of M, this embedding is 1-1. σ ⊧ “f ∈ g” if f is the image of some x under this embedding, and x ∈ g(σ). P(M) is easily seen to be extensional, and an end-extension of M. Furthermore, this process of taking the power set can be iterated transfinitely: M_{0} = M, M_{α+1} = P(M_{α}), and M_{λ} = →^{lim} {M_{α} | α < λ} (or, more colloquially, ⋃_{α<λ} M_{α}). If α > β then M_{α} is an extensional end-extension of M_{β}.

In the current context, V is ⋃_{H_{fin}} L_{ω_{1}^{CK}} [G ∪ H_{fin}]. V ⊧ KP, but V does \underline{not} satisfy Power Set, so some care must be taken in the construction of P(M). We start with M being the empty structure – M_{σ} = ∅ – but we do not claim that each M_{α} is a set. Rather, the generation of the M_{α}-hierarchy is given by a Σ_{1} induction, so the relation “f ∈ (M_{α})_{σ}” is Σ_{1}. Let M_{big} be M_{ω_{1}^{CK}}. The final model M is L^{M_{big}}; that this definition makes sense (i.e. that α ↦ L_{α} is a total Δ_{1}-definable function via the standard definitions) is implied by the following lemma.

Lemma 4.3.1 M_{big} ⊧ IKP.

proof: For Empty, the function f(σ) = ∅ is in M_{1}. For Infinity, defining \overline{ω} as in the previous section, the function f(σ) = \overline{ω} is in M_{ω+1}. For Pairing, if x, y ∈ M_{α}, let f(σ) in M_{α+1} be {x, y}. For Union, if x ∈ M_{α}, then f(σ) = ⋃x(σ) is also in M_{α}. Extensionality was already remarked as holding. For Δ_{0} Comprehension, by end-extensionality a Δ_{0} formula over M_{big} is equivalent to a Δ_{0} formula in V, and Δ_{0} Comprehension in V suffices. For Foundation, suppose to the contrary that σ ⊧ ∀x(∀y ∈ x ϕ(y) → ϕ(x)), but σ |̸= ∀xϕ(x). Let α be the least ordinal such that for some x ∈ M_{α}, τ ≥ σ τ |̸= ϕ(x). But if ξ ⊧ y ∈ x then y ∈ M_{β}, so ξ ⊧ ϕ(y). Hence τ ⊧ ∀y ∈ x ϕ(y), and τ ⊧ ϕ(x), a contradiction. Finally, for Δ_{0} Bounding, suppose σ ⊧ ∀x ∈ A ∃y ϕ(x, y), ϕ a Δ_{0} formula. Then in V ∀τ ≥ σ ∀x ∈ A_{τ} ∃α ∃y ∈ M_{α} τ ⊧ ϕ(x, y). By Δ_{0} Bounding in V, the αs needed can be bounded, say by β, and again by Δ_{0} Bounding in V a bounding set B in M_{β+1} can be constructed.

Corollary 4.3.2 M ⊧ V=L.

proof: This is the basic result of [7].

Lemma 4.3.3 M ⊧ IKP + Π_{2} Reflection.

proof: The minor axioms of IKP are all easy. (For Extensionality, use the fact that M is a transitive sub-class of the extensional M_{big}. For Foundation, use the definability of M inside of the well-founded M_{big}.) Δ_{0} Comprehension follows from the definition of L and the absoluteness of Δ_{0} formulas, just as in the classical case. Δ_{0} Bounding follows from Π_{2} Reflection. For Π_{2} Reflection, suppose M ⊧ ∀x ∃y ϕ(x, y), ϕ a Δ_{0} formula, and A is a set in M. We will enlarge A to a transitive model of the same sentence. Work in the ambient universe V. All of the parameters in sight (i.e. A and those of ϕ) are members of L_{ω_{1}^{CK}} [G ∪ H_{fin}] for a fixed H_{fin}. Moreover, for any Δ_{0}(M) formula ϕ, there is an equivalent Δ_{0}(V) formula ϕ^{∗}, exactly as in 4.2.2. By standard symmetry arguments, no more members of H are needed to find witnesses y in V. So for each x in A let α_{x} be an ordinal such that a witness for x is in L_{α_{x}}[G ∪ H_{fin}]. Moreover, L_{α_{x}}[G ∪ H_{fin}] should also include all the relevant evidence that the witness is in M. Using the admissibility of the ambient universe, let α_{0} bound the α_{x}’s needed. Of course, this must be iterated to account for the new sets in L_{α_{0}}[G ∪ H_{fin}] which are in L^{M} (via an ordinal also in L_{α_{0}}[G ∪ H_{fin}]). Iterate ω-many times. Let α be ⋃ α_{n}, and β be {x | x is an ordinal in M_{big}} over L_{α}[G ∪ H_{fin}]. L_{β} reflects ϕ.

Lemma 4.3.4 M ⊧ ¬Σ_{1}DC.

proof: As in 4.2.5, there can be no sequence of distinct members of {B(R) | R ∈ G}, which is a set in L.

Lemma 4.3.5 M ⊧ ¬Resolvability.

proof: This argument is somewhat technical, but since the idea is rather simple we will give a quick overview of it. Suppose there were such a resolution. Since M is definable in the ambient universe, so is this resolution. Any definition can use only finitely many parameters, in particular only finitely many members of H. Consider branches of the form B(R), R ∈ H. Which ordinal each gets attached to is determined by some forcing condition. Furthermore, beyond the finitely many parameters, such a forcing condition need mention only (that is, is an initial segment of) R. By mutual genericity, for every initial segment of a real there are infinitely many R’s that share that initial segment. So any forcing condition attaching B(R) to an ordinal forces infinitely many different B(R)’s to that same ordinal. Therefore there is a set which contains infinitely many B(R)’s, R ∈ H, a contradiction.

The following proof makes essential use of the definability of the forcing relation “p |⊢ ϕ” over the ground model L_{ω_{1}^{CK}} [G] for the forcing partial order to get the set H. The forcing partial order is { p | p : ω → 2^{<ω}, supp(p) finite}, where supp(p), the support of p, is { n ∈ ω | p(n) ≠ ∅}. The resulting generic is (trivially identifiable with) a function f_{H} with domain ω and range H. We will assume that the forcing language has a constant H_{n} for each n ∈ ω, which is interpreted in the generic extension as f_{H}(n), as well as constants for f_{H} itself and for the range of f_{H}, for which we will ambiguously use the symbols f_{H} and H respectively (f_{H} and H being also sets in the generic extension; in effect, the constant H will be interpreted as the set H and similarly for f_{H}; whether the constant symbol or its interpretation is meant every time we say “H” of “f_{H}” should be clear from the context). To name the elements in the generic extenion L_{ω_{1}^{CK}} [G, H] it suffices to consider the language generated by the symbols H and the H_{n}’s; f_{H} is not necessary. To name the elements in M it suffices to consider the language generated by the H_{n}’s; H is not necessary. (Recall the definition of V, over which M was defined.)

M is a structure definable over L_{ω_{1}^{CK}} [G, H], and so the truth predicate over M, “σ ⊧ ϕ”, is also definable over L_{ω_{1}^{CK}} [G, H]. It follows that the forcing relation p |⊢ “σ ⊧ ϕ” is definable over L_{ω_{1}^{CK}} [G]. If the reader feels uncomfortable with the indirectness hidden behind the simple notation (M being a definable sub-class of M_{big}, itself a union not of sets but of definable classes), then to save the trouble of the detailed argument needed to prove the definability of the forcing relation, with just a tad more set-theoretic power we can take the ground model to be L_{ω_{2}^{CK}} [G], ω_{2}^{CK} the first admissible ordinal after ω_{1}^{CK}. (Our claim is, ultimately, that the results here are theorems of ZF.) In L_{ω_{2}^{CK}} [G, H] M is a set, so the forcing relation p |⊢ “σ ⊧ ϕ” for statements about M is definable, Δ_{1} even. So take the ground model U to be L_{ω_{1}^{CK}} [G] or L_{ω_{2}^{CK}} [G], whichever you feel more comfortable with.

Suppose for a contradiction that Resolvability were to hold in M: σ ⊧ “f is a resolution”. Let p ∈ f_{H} force such: p |⊢ “σ ⊧ f is a resolution”. Let supp(f) be { n | H_{n} occurs in the definition of f}. f mentions only finitely many paramters, each of which is ultimately evaluated in L_{ω_{1}^{CK}} [G ∪ H_{fin}] for some finite H_{fin} ⊆ H. Hence supp(f) is finite, and without loss of generality supp(f) ∪ supp(σ) ⊆ supp(p).

Not only does M satisfy the Axiom of Foundation, it is even well-founded in the sense of U[H]; that is, the relation (σ, x) < (τ, y) if (σ ≥ τ ∧ σ ⊧ “x ∈ y”) is well-founded in U[H]. It would be shown inductively on γ that each M_{γ} has this property in U[H], hence M_{big} too as the union of the M_{γ}’s, and finally M as a submodel of M_{big}. Therefore, not only do we have that σ ⊧ “dom(f) is a wellfounded linear order”, but also { α | σ ⊧ “α ∈ dom(f)”} (a collection in U[H] of Kripke sets) is also a well-founded linear order (with the order relation being that induced by M). We will refer to this set as ext_{σ}(dom f), the externalization of the domain of f as σ.

So let q ≤ p, q ∈ f_{H}, α, and H_{i} be such that

q |⊢ “[α is the least member of ext_{σ}(dom f) such that for some X ∈ H σ ⊧ (⋀_{n∈supp(p)} B(H_{n}) ≠ B(X) ∧ B(X) ∈ f(α))] ∧ [σ ⊧ (⋀_{n∈supp(p)} B(H_{n}) ≠ B(H_{i}) ∧ B(H_{i}) ∈ f(α))]”. Without loss of generality supp(α) ∪{i} ⊆ supp(q). Consider j ∉ supp(q).

Let ρ_{j} be the permutation of ω which interchanges i and j. ρ_{j} can be extended to a permutation of terms in the forcing language which interchanges all occurrences of H_{i} with H_{j}. This permutation we denote also as ρ_{j}. Such a permutation on terms induces a permutation on sentences (by merely permuting the parameters), and this permutation is truth-preserving (for the language describing U[H], i.e. without f_{H}):

r |⊢ ϕ ↔ r ∘ ρ_{j} |⊢ ρ_{j}(ϕ).

(For a development of focing and symmetric models, see [5] for instance.) The sentence forced by q above is in this restricted language, hence

q ∘ρ_{j} |⊢ “[ρ_{j}(α) is the least member of ext_{σ}(dom f) such that

for some X ∈ H σ ⊧ (⋀_{n∈supp(p)} B(H_{n}) ≠ B(X) ∧ B(X) ∈ f(ρ_{j}(α)))] ∧ [σ ⊧ (⋀_{n∈supp(p)} B(H_{n}) ≠ B(H_{j}) ∧ B(H_{j}) ∈ f(ρ_{j}(α))]”.

(Of course we are using the fact that ρ_{j}(f) = f.)

Let r ≤ q, q∘ρ_{j}. Since r forces that both α and ρ_{j}(α) are the least M-ordinals with a certain property, r |⊢ α = ρ_{j}(α). Hence r |⊢ “B(H_{i}), B(H_{j}) ∈ f(α)”.

Let J ⊆ ω\ supp(q), |J| = n finite. Let q ∘ρ_{J} be { q ∘ρ_{j} | j ∈ J } and r_{J} be inf(q ∘ρ_{J} ∪ {q}). Then r_{J} |⊢ “B(H_{i}) ∈ f(α) ∧ ⋀_{j∈J} B(H_{j}) ∈ f(α)”. The set R_{n} = { r_{J} | J ⊆ ω\ supp(q), |J| = n } is definable and pre-dense in the forcing partial order, so f_{H}∩ R_{n} ≠ ∅. This means that f(α) contains at least n+1-many distinct Kripke sets of the form B(H_{j}). Since this holds for all n, f(α) contains infinitely many such Kripke sets. This, though, is a contradiction. According to the definition of a resolution, σ ⊧ “f(α) is a set”, and each Kripke set in M is in L_{ω_{1}^{CK}} [G ∪ H_{fin}] for some finite H_{fin}.

4.4 IKP + V=L + ¬Π_{2}-Reflection

This construction is weaker than the others in that the model produced will not satisfy ¬Π_{2}-Reflection, but merely will not satisfy Π_{2}-Reflection. In fact it will be a model of ¬¬Π_{2}-Reflection. This suffices to show that IKP + V=L does not prove Π_{2}-Reflection, but it is still open whether IKP + V=L proves ¬¬Π_{2}-Reflection.

The partial order of this model will be ω-many copies of 2^{<ω} next to each other, with two consecutive bottom elements. That is, there is a first node ⊥⊥, followed by another node ⊥, itself followed by ω-many incompatible nodes ⊥_{n}, each of which is the bottom node of a copy of 2^{<ω}. We will really be working with the subtree above ⊥; the role of bottom is merely that ⊥ ⊧ “1_{⊥⊥} = 1”, i.e. ⊥ ⊧ “1 ∈ P̂”. Let P̂_{n} be the nth subtree, internally: [σ ⊧ y ∈ P̂_{n}] ↔ [∃τ compatible with ⊥_{n} σ ⊧ y = 1_{τ}]; notice that for σ incompatible with ⊥_{n}, σ ⊧ P̂_{n} = {1}. (By way of notation, let the numbering of these trees start with 1 instead of 0, because 0 as a subscript is already in use, to indicate including 0 as a member.)

We need the ω-sequence < P̂_{n} | n ≥ 1 > in the model. To this end, let α_{n} be P̂_{n} ∪\overline{n + 1}, where, as before, \overline{n + 1} is the internalization of n+1. Notice that α_{n} is an ordinal, and L_{α_{n}} = P̂_{n} ∪ L\overline{n+1} (using lemma 4.1.1 here). Let α be P̂ ∪ \overline{ω} ∪ \{T_{n0} | n ≥ 1\} ∪ \{α_{n} | n ≥ 1\}. So

L_{α} = P̂ ∪ L\overline{ω} ∪ ⋃\{def(T_{n0}) | n ≥ 1\} ∪ ⋃\{def(P̂_{n} ∪ L_{n+1}) | n ≥ 1\}.

Over L_{α} let ϕ(x, y) iff

0 ≠ x ∈ \overline{ω} ∧ 0 ≠ y ⊆ 1
∧ ∃z(x, y ∈ z)
∧ ∀z(x + 1 ∈ z ∧ y ∈ z → y = 1).

We claim that ∀x ⊥ ⊧ “∀y ϕ(x, y) ↔ y ∈ P̂_{x}”. To see this, go through the members of L_{α}. There is no z in P̂ with a non-0 member. In L\overline{ω} the only possible y (i.e. the only non-0 subset of 1) is 1 itself, and indeed for all x ≥ 1 ϕ(x, 1); since ⊥ ⊧ 1 ∈ P̂_{x}, this is fine. The only members of \overline{ω} also in P̂_{n0} are 0 and 1, so if z ∈ def(P̂_{n0}) has a legal x as a member then x = 1. In fact this is subsumed by the final case: the common members of \overline{ω} and (P̂_{n} ∪ L\overline{n+1}) are 0, 1, ... , \overline{n}; the non-0 subsets of 1 are exactly the members of T_{n}; so the appropriate < x, y > candidates are < m, y >, y ∈ P̂_{n} and m≤n. If m<n and ¬σ ⊧ y = 1 then {m+1, y} shows that ¬σ ⊧ ϕ(m, y). Hence the only time σ ⊧ ϕ(x, y) is when σ ⊧ y ∈ P̂_{x}.

Keeping in mind that P̂_{x} ∈ L_{α}, the functional relation “f(\overline{n}) = P̂\overline{n}” (as a two-place relation ψ(\overline{n}, Z)) can be defined over L_{α} as “∀y y ∈ Z ↔ ϕ(\overline{n}, y)”. There is a small integer m such that this function f is actually a member of L_{α+\overline{m}}. (L_{α} is available as a parameter already in L_{α+1}, and all else you need are some ordered pairs.)

Next comes an extension of the notion of a branch to include a branch through P̂_{n}. If Q ⊆ P̂ is closed downwards (i.e. closed under taking supersets), then by requiring in the definition of a branch that B ⊆ Q and restricting the γ’s in clause (3) to Q, we get a branch through Q. The proof of lemma 4.1.7 goes through with Q in place of P̂. In the case at hand, any branch through P̂_{n}, externally at some σ compatible with ⊥_{n}, is a branch through P̂_{σ}, and externally at some σ incompatible with ⊥_{n} is just {1}. Let R be any real, and B_{n} the corresponding branch through P̂_{n}.

Let W be a recursive ordering of ω which is not well-founded but which has no hyperarithmetic infinite descending sequence. For the convenience of the reader, we review some basic facts about W which will be used.

For every i there is a W-least j ≤_{W} i such that the W-interval [j,i]_{W} has order-type some α < ω_{1}^{CK}. To see this, work in L_{ω_{1}^{CK}}. Define f(0) = ⟨i, 0, 0⟩, f(n+1) = the L-least triple ⟨j, α, g⟩ such that j <_{W} proj_{0}(f(n)) and g is an order-isomorphism between [j,i]_{W} and the ordinal α. Set j_{n} = proj_{0}(f(n)). f is a Σ_{1}-definable function on an initial segment of ω. By the admissibility of L_{ω_{1}^{CK}}, f ∈ L_{ω_{1}^{CK}}. If dom f = ω then i = j_{0} >_{W} j_{1} >_{W} ... would be a hyperarithmetic infinite descending sequence, in contrast to the choice of W. Let n = max(dom f). Then [j_{n},i]_{W} is isomorphic to some α ∈ ω_{1}^{CK}, but for all j < j_{n} [j,i]_{W} is not well-founded. Call this j_{n} corresponding to a given i 0_{i} (“0 in the sense of i”).

In the other direction, ∀i ∈ ω, α ∈ ω_{1}^{CK} ∃j_{α} ∈ ω such that [i, j_{α})_{W} has order-type α (except possibly for those i’s belonging to a final segment of W of order-type some β < ω_{1}^{CK}). To see this, for a given i, if this fails, let α be the least ordinal for which this fails. By the admissibility of L_{ω_{1}^{CK}}, {j_{β} | β < α} ∈ L_{ω_{1}^{CK}}. If this set is a final segment of W, then the end-segment starting at 0_{i} (as constructed above) is an end-segment of order-type γ = o.t.[0_{i}, i)_{W} + α < ω_{1}^{CK}. In the other case, there is a j >_{W} j_{β} for all β < α. In fact, there is a least such j, or else the function f(0) = j > j_{β} (for all β simultaneously) arbitrary, f(n+1)

= the least (in the standard ordering of ω) j such that j <_{W} f(n) and j > j_{β} (∀β) would produce a hyperarithmetic infinite descending sequence. This least such j witnesses that [i,j) has order-type α, in contrast to the choice of α.

Combining these two results, we see that every i is contained in a maximal interval of order-type an ordinal, and this interval starts at 0_{i} ≤_{W} i and has order-type ω_{1}^{CK} (or some β < ω_{1}^{CK} on a final segment). We will call this interval i’s standard neighborhood, with the notation sn(i). If i_{1} >_{W} i_{0} is not in i_{0}’s standard neighborhood, then ∀j ∈ sn(i_{0}) i_{1} >_{W} j; we will use the notation i_{1} >_{W} sn(i_{0}) in this case and say that i_{1} is a non-standard distance above i_{0}. Notice that in this case there is an î such that i_{1} >_{W} sn(î) and î >_{W} sn(i_{0}). To see this, notice that { j | sn(i_{0}) <_{W} j <_{W} 0_{i_{1}} } is non-empty, else sn(i_{0}) would be a member of L_{ω_{1}^{CK}} (definable as [0_{i_{0}}, 0_{i_{1}})_{W}) and f(j) = order-type([0_{i_{0}}, j)_{W}) would then be a total function from sn(i_{0}) onto ω_{1}^{CK}. Let î be any element such that sn(i_{0}) <_{W} î <_{W} 0_{i_{1}}.

With these preliminaries behind us, we can now return to the construction of the model M. Given a final segment of W with least element i, let ξ_{i} be {B_{j0} | j ≥_{W} i} ∪ α ∪ {α}. As in section 4.2, iterate definability ω_{1}^{CK}-many times on top of L_{ξ_{i}}, to get M_{i}. As has already been observed, lemmas 4.2.2 - 4.2.4 did not use any particular facts about the reals used to define the branches, and so in the following we will freely omit details of the proofs, referring the reader to the proofs of these previous lemmas.

M will be ⋃_{i∈I} M_{i}, for some final segment I of W with no least element. The exact choice of I will be given in lemma 4.4.8, the only place where it’s used.

Lemma 4.4.1 M_{i} ⊧ IKP.

proof: As in lemma 4.2.2.

Lemma 4.4.2 L_{α} ∈ L^{M_{i}}.

proof: α_{n} is definable over L_{α_{n}} as the set of all ordinals, so α_{n} ∈ L_{α} and α ⊆ L_{α}. Since M_{i} is admissible, γ = { β ∈ L_{α} | def(L_{β}) ⊆ L_{α} } ∈ M_{i}. α ⊆ γ, so L_{α} ⊆ L_{γ}. By the definition of γ, L_{γ} ⊆ L_{α}.

Corollary 4.4.3 f ∈ M_{i}.

proof: f ∈ L_{α+\overline{n}}, and since L_{γ} = L_{α}, L_{γ+\overline{n}} = L_{α+\overline{n}}.

Lemma 4.4.4 In M_{i}, if ⊥ ⊧ “B is a branch through f(j)” then j ≥_{W} i.

proof: Suppose j <_{W} i. Consider M_{i} at node ⊥_{j}. For any definition ϕ(x) at any stage in the construction of M_{i}, consider the structure which consists of all of the relevant information: at first this includes the stage α at which ϕ is being evaluated, (M_{i})_{α}, the formula ϕ, and ϕ’s parameters, but these parameters can themselves be unpacked, until the only parameters left are from P̂_{j}. This uses of course that at ⊥_{j} all of the branches included in ξ_{j} are {1}. The parameters are all of the form 1_{σ}. Let τ be any node beyond or incompatible with all such σ’s. Then τ ⊧ ϕ(1_{ρ}) for some ρ extending τ iff τ ⊧ ϕ(1_{ρ}) for every ρ extending τ of the same length. (The proof of this would use an automorphism of the model interchanging any two such ρ’s.) So ϕ could not possibly define a branch through P̂_{j}.

Lemma 4.4.5 If k ≤_{W} i then L_{ξ_{i}} ∈ L^{M_{k}}.

proof: In M_{k}, let B_{full} be { B ∈ L_{ξ_{k}} | B is a branch through f(j) for some j ≥_{W} i }. Letting δ be { B_{0} | B ∈ B_{full} } ∪ T, and letting γ be as in lemma 4.4.2, L_{ξ_{i}} = L_{δ∪γ∪{γ}}.

Corollary 4.4.6 If k ≤_{W} i then M_{i} ⊆ M_{k}.

proof: As in lemma 4.2.3.

Corollary 4.4.7 M_{i} ⊧ V=L.

proof: As in lemma 4.2.4.

Lemma 4.4.8 M ⊧ IKP.

proof: As the union of transitive models of IKP (see lemma 4.4.1), M automatically satisfies Empty Set, Infinity, Union, and Δ_{0}-Comprehension. One of the more difficult axioms to check, surprisingly enough, is Pairing. That is the point of the penultimate corollary, which also implies Extensionality. Foundation holds because M is well-founded in V.

The only other axiom is Δ_{0} Bounding. The choice of I will be exactly to ensure this. The construction is really the same as in [8]; we replicate the main idea here to make this paper self-contained. Notice that for any choice of I any node other than ⊥ forces IKP, because ⊥_{i} ⊧ M = M_{i} if i ∈ I, and ⊥_{i} ⊧ M = “M_{i} without the branch” which also models IKP, if i ∉ I. So we need concern ourselves only with functions forced to be total by ⊥. There are countably many Δ_{0} definitions (with parameters) which might define a total function on a set. We’ll handle the nth, ϕ_{n}(x, y), at stage n. Assume inductively we have max_{n} a non-standard distance above min_{n} in W (max_{0} and min_{0} being arbitrary elements of W a non-standard distance apart). By the discussion about W (just before the lemmas of this section), let m be a non-standard distance above min_{n} and a non-standard distance below max_{n} (i.e. sn(min_{n}) < m and sn(m) < max_{n}). In M_{m} either ϕ_{n} defines a total function or it doesn’t. In the former case, M_{m} contains a bounding set (by lemma 4.4.1), which is also a bounding set in any model extending M_{m}, so let max_{n+1} = m (and let min_{n+1} = min_{n}). In the latter case, ϕ_{n} is not total in M_{m}, or, for that matter, in any transitive submodel thereof (by the absoluteness of Δ_{0} formulas among transitive models). So let min_{n+1} = m (and let max_{n+1} = max_{n}). Let I = {i | ∃n i ≥ max_{n}}.

Lemma 4.4.9 M ⊧ V=L.

proof: The union of models of V=L is also a model of V=L.

Lemma 4.4.10 M |̸= Π_{2}-Reflection.

proof: The assertion “B is a branch through S” is Δ_{0}, hence absolute in all transitive sets containing the parameters. So if ⊥ ⊧ “B is a branch through f(j)” then j ∈ I. Moreover, if j ∈ I, then ⊥ ⊧ “there is a branch through f(j)”. So ⊥ ⊧ “∀j, B_{j} ∃i, B_{i} if B_{j} is a branch through f(j) then either f(j) = {1} or (i<_{W} j and B_{i} is a branch through f(i))”. But this does not reflect to any set, because each set is a member of some M_{i}, which is constructible in L_{ω_{1}^{CK}}, in which W has no infinite descending sequence.

5 Questions

1. Is there a model of Σ_{1} DC + IKP + V=L + ¬Resolvability?

2. Is there a model of IKP + V=L + ¬Π_{2}-Reflection?

3. Does IZF prove that admissible sets are unbounded (that is, for each set X is there a transitive admissible set containing X)? Does IZF prove the existence of an admissible set with ω? The usual constructions of admissible sets use either reflection or the linearity of the ordinals, neither of which is available to us here.

4. Does IZF_{Rep} (that is, IZF with the Bounding Schema substituted by the Replacement Schema) prove IKP? With some better technology (see question 6) it should be possible to show that IZF_{Rep} - Power does not prove IKP. Also,

[3] (with a minor alteration) shows that IZF_{Rep} does not prove Π_{1} Bounding. But whether IZF_{Rep} proves Δ_{0} Bounding is apparently unknown.

5. As has already been observed, least fixed points and greatest fixed points are closely connected classically, but not so intuitionistically. How much can they be separated? Can IKP be strengthened so that even more least fixed points become definable, without picking up Π Persistence or any greatest fixed points? Conversely, can Π Persistence by extended to get more greatest fixed points, without picking up IKP or least fixed points? There are connections between least and greatest fixed points and their categorical analogues, initial algebras and final co-algebras of functors, so these matters could be pursued from this angle; but not so much is known even there, and the connections are not yet so clear. These considerations suggest a similar yet simpler question, involving the first order quantifiers: has anyone investigated existential intuitionistic logic (with ∃, even ¬∃¬, but not ∀), or universal intuitionistic logic?

6. Are there other natural examples of the difference between IKP and Π Persistence?

7. Another variant on IKP yet to be mentioned is the weakening of Δ_{0} Bounding to Σ_{1} Replacement. It can be shown that classically Σ_{1} Replacement does not imply Δ_{0} Bounding; in fact, it is possible to build a classical model of full Replacement + ¬Δ_{0} Bounding. It would have been nice to have included in this paper an adaptation of this model to IL. However, this project brings up a host of new problems. All of the models presented here which use forcing do so only in an ambient classical universe to get some particular desired property. For instance, a failure of Σ_{1} DC in a classical model is imported to become a failure of Σ_{1} DC in the intuitionistic model. In order to get Δ_{0} Bounding to fail, the forcing has to be done internally. Unfortunately, intuitionistic forcing technology is not yet well enough developed to carry such a burden. Certainly some work has already been done in this area; see [2] for instance. But not enough has been done yet to provide a robust enough theory to carry through the construction envisioned here. This should be possible, but would take us too far beyond the scope of the current paper.

References

[1] Jon Barwise, Admissible Sets and Structures, Springer- Verlag, 1975.

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

[3] Harvey Friedman and Andrej Scedrov, The lack of definable witnesses and provably recursive functions in intuitionistic set theories, Advances in Math, 1985, p. 1-13.

[4] Thomas Jech, Multiple Forcing, Cambridge University Press, 1986

[5] Thomas Jech, Set Theory, Academic Press, 1978

[6] Jim Lipton, Realizability, Set Theory, and Term Extraction, in The Curry-Howard Isomorphism (Ph. de Groote, ed.), Volume 8 of the “Cahiers du Centre de logique” (Université catholique de Louvain), Academia, 1995, pp. 257-364.

[7] Robert Lubarsky, Intuitionistic L, in Logical Methods in Computer Science: The Nerode Conference(Crossley et al., eds.), Birkhauser, 1993, p. 555-571.

[8] Robert Lubarsky, Sacks forcing sometimes needs help to produce a minimal upper bound, Journal of Symbolic Logic, 1989, p. 490-498.

[9] William Powell, Extending Godel’s negative interpretation to ZF, Journal of Symbolic Logic, 1975, p. 221-229.