Independence Results around Constructive ZF

Robert S. Lubarsky

July 10, 2006

1 Introduction

When making the transition from a classical to an intuitionistic system, one is compelled to reconsider the axioms chosen. For instance, it would be natural to re-formulate those that imply Excluded Middle. In the context of set theory, typically the Axiom of Foundation is substituted by the Axiom of Set Induction, the two being equivalent classically but the latter not yielding Excluded Middle intuitionistically. Even axioms that do not return classical logic must be reevaluated, as classically equivalent variants may not remain so in a different logic. An example of this is Collection, which, over the other ZF axioms, is equivalent to Replacement and to Reflection, but not over intuitionistic ZF (see [4]).

A different reason to re-evaluate axioms is to take more seriously the program of constructivism. IZF is basically ZF with classical logic replaced by intuitionistic. Since, though, the axioms of ZF were never meant to be constructive, they’re still not even with a different logic. This issue was addressed by Myhill (see [7]), who re-formulated by the axioms and framework of ZF to come up with CST (Constructive Set Theory). Among the changes he made was to eliminate the Power Set Axiom as non-constructive; as an alternative, he included Exponentiation, the hypothesis of the existence of the set of functions from a set A to a set B, as adequately strong to do most of ordinary mathematics yet still sufficiently constructive.

Later on, Aczel ([1], see also [2] and [3]) picked up the thread and re-cast CST in a more conventional framework, christening this revamped version CZF (Constructive ZF). He also provided a constructive justification for the enterprise, by interpreting CZF in Martin-Löf type theory ([5], [6]). In so doing, he uncovered a principle apparently stronger than Exponentiation, Subset Collection. Subset Collection is most easily understood via an equivalent, Fullness. A set C of total relations from A to B is said to be full if every total relation from A to B can be thinned to one in C. The Fullness Axiom says that every pair of sets has a full set of relations. This principle is valid in Aczel’s interpretation, and so is included in CZF.

This all leads to asking what the exact relationship among these axioms actually is. It is easily seen that Power Set implies Subset Collection, which itself implies Exponentiation. What about the reverse implications? SC was chosen over Exponentiation because it’s presumably stronger, and Power Set not because it’s presumably not Martin-Löf interpretable. Presumably. In this paper, we show that the presumed non-implications are indeed correct. In the next section, it is show that SC does not imply Power Set, and in the one after that, that Exponentiation does not imply SC. In the final section, we observe that a result about Reflection is a by-product of the earlier work.

In fact, although these questions came up in the context of CZF, slightly more than independence over the remaining CZF axioms is shown. The other difference between CZF and IZF is that CZF contains Restricted Separation (i.e. Separation for Δ_{0} definable properties), whereas IZF has full Separation. The independece results below include full Separation, and so are actually independence results over IZF - Power Set.

For the record, the axioms of IZF are: Empty, Infinity, Pair, Union, Extensionality, Set Induction, Power Set, Separation, and Collection. CZF consists of Empty, Strong Infinity, Pair, Union, Extensionality, Set Induction, Subset Collection, Δ_{0} Separation, and Strong Collection. Strong Infinity is a variant of Infinity that more directly produces ω without resort to Power Set or full Separation. Similarly, Strong Collection is a variant of Collection useful in the absence of full Separation. Collection asserts the existence of a bounding set (for a total function on a set defined by a formula). In the presence of Separation, one can take those elements of a postulated bounding set that come from something in the domain. Strong Collection is the assertion that there is a bounding set consisting only of range values for something in the domain.

2 Subset Collection does not imply Power Set

We will provide a Kripke model of CZF + ¬ Power Set (within the meta-theory ZF). Furthermore, full Separation will hold.

Given a partial order P, the full Kripke model M on P is defined inductively on α ∈ ORD as follows. At node σ, the universe M_{σ}^{α} consists of those functions f with domain P_{≥σ} such that for τ ≥ σ f(τ) ⊆ ⋃_{β<α} M_{τ}^{β} and for ρ ≥ τ f_{τρ}”f(τ) ⊆ f(ρ) (where f_{τρ} is the transition function from node τ to node ρ). f_{στ} is then extended from ⋃_{β<α} M_{σ}^{β} to M_{σ}^{α} as restriction: f_{στ} (f) = f ↑ P_{≥τ}. The universe at σ, M_{σ}, is defined as ⋃_{α∈ORD} M_{σ}^{α}. Then ∈ and = are as easy as pie to define: σ ⊢ f ∈ g iff f ∈ g(σ), and σ ⊢ f = g if f = g.

Equivalently, one could simplify the inductive generation of the Kripke sets and the transition functions, at the expense of ∈ and =, by having the Kripke sets have domain all of P: M^{α} = {f : P → ⋃_{β<α} M^{β} | f is monotonically non-decreasing (i.e. σ < τ → f(σ) ⊆ f(τ))}. Then M_{σ} is just ⋃_{α∈ORD} M^{α} (which, note, is independent of σ), and the transition functions are just the identity. The complication pops up again when defining ∈ and =, since at σ all nodes not extending σ are unimportant but still in the domains and hence need to be actively disregarded: σ ⊢ f ∈ g if ∃h ∈ g(σ) σ ⊢ f = h, and σ ⊢ f = g if ∀τ ≥ σ [∀h ∈ f(τ) τ ⊢ h ∈ g(τ) ∧ ∀h ∈ g(τ) τ ⊢ h ∈ f(τ)].

The model we ultimately want to consider differs from that above in that the Kripke sets are to be, as functions, eventually constant. There are several ways this could be achieved. The formalism developed below will be to have P be a class; in particular, ORD. Since every Kripke set is a set, it can give information about only a finite initial segment of P, after which it is assumed to be constant. Alternatively, P could be taken to be ω and the Kripke sets to be eventually hereditarily constant. In fact, this latter approach could be read off from the former by taking a cofinal ω-sequence through ORD (from outside of V, naturally) and cutting the full model down to those nodes. (That this works might be construed as a reminder that ω is still the largest large cardinal of all.) Neither approach seems essentially easier than the other, so, perhaps arbitrarily, we will henceforth deal only with the former.

At this point it would be prudent, instead of formalizing the ideas above in their full generality, to particularize to the partial order of interest. So let P be ORD. The nodes in P will typically be referred to with letters from the middle of the Greek alphabet (κ, λ, μ, ν and so on) so as not to cause confusion with the use of α, β, and γ used in inductions.

Both constructions above can be adapted to this choice of P. The adaptation of the second construction will be described informally, followed by a thorough description using the first construction, which we remain the basis of this paper. So inductively a Kripke set is a function from P = ORD to the class of previously defined Kripke sets, which is not only monotonic but also eventually constant: M^{α} = {f : ORD → ⋃_{β<α} M^{β} | f is monotonically non-decreasing and ∃κ∀λ > κ f(λ) = f(κ)}. Since f(κ) is set-sized, not only is each of its elements eventually constant (inductively), but there is a uniform point of stability: ∃κ∀g ∈ T C(f) (transitive closure) g is constant beyond κ. The transition functions, as well as membership and equality, as are above.

To formalize this as stated, an axiomatic theory of classes would be necessary. To work within a more conventional framework, meaning a theory of sets (the framework of this paper being, after all, ZF), an element f will have to be a function on a (necessarily) set-sized initial segment of ORD, beyond which f is implicitly constant. The technical work here is to define the transition functions f_{κλ} on f, even when λ ∉ dom(f). Since this involves mucking with the domains anyway, it’s easier to adapt the former of the constructions above. The reader with a clear intuition who is willing to trust that these matters can be formalized may safely skip to the proposition.

The full Kripke model M on P is defined inductively on α ∈ ORD as follows. At node κ, the universe M_{κ}^{α} consists of those functions f with domain λ\κ (for some λ > κ) such that for μ ∈ dom(f) f(μ) ⊆ ⋃_{β<α} M_{μ}^{β} and for ν ∈ dom(f), ν ≥ μ, f_{μν}”f(μ) ⊆ f(ν) (where f_{μν} once again is the transition function from node μ to node ν). Without loss of generality we can also require that for all μ ∈ dom(f) and g ∈ f(μ) dom(f) ⊇ dom(g). (“WLOG” means here that this additional stipulation does not exclude any sets. More precisely, if f satisfies the definition for a set in the Kripke structure except for the condition on the domain, then there is a Kripke set g satisfying the domain condition such that κ ⊧ “f=g”. Such a g would be constructed as an end-extension of f, whereby for μ ∈ dom(g)\dom(f), g(μ) would be taken as f_{κμ}(f), using the transition functions about to be defined.)

f_{κμ} is then extended from ⋃_{β<α} M_{κ}^{β} to M_{κ}^{α} as follows. If μ ∈ dom(f), then f_{κμ} is restriction: f_{κμ}(f) = f ↑ dom(f)\μ. If μ ∉ dom(f), then f_{κμ}(f) will have domain {μ} (in the notation from the last paragraph, λ will be μ + 1), and (f_{κμ}(f))(μ) will be (working inductively here) ⋃_{ν∈dom(f)} f_{νμ}”f(ν). It is left to the reader to show that the transition functions compose as they are supposed to (i.e. f_{λμ}∘ f_{κλ} = f_{κμ}).

The universe at node κ, M_{κ}, can now be defined as ⋃_{α∈ORD} M_{κ}^{α}. The transition functions f_{κμ} defined along the way on M_{κ}^{α} cohered, which is why the dependence on α was dropped from the notation; the ultimate f_{κμ} defined on M_{κ} is the union of the partial f_{κμ}’s defined along the way.

We will need that the model M is definable in V, so we may as well check each building block in the development of M when it’s first introduced. Notice that M_{κ}^{α} cannot be a function of α, since M_{κ}^{α} is not even a set! However, the relation “f ∈ M_{κ}^{α}” (as a relation on f, α, and κ), as well as “f_{κμ}(f) = g” (as a relation on f, g, κ, and μ) is Δ_{1}. This can be shown via a simultaneous Σ_{1} induction. The central point in this argument is that the definitions (as given above) contain only bounded quantification and recursive calls.

∈ and = must then be defined via a mutual induction to make sure that Extensionality holds in the end. The problem here, which does not come up in the case of a set-sized underlying p.o., is illustrated by the fact that both {⟨0, ∅⟩} and {⟨0, ∅⟩, ⟨1, ∅⟩} stand for the empty set yet are not themselves equal as sets. The reader uninterested in such details can safely skip to the main proposition.

Assume that ∈_{β} and =_{β} are defined on M_{κ}^{β} for all nodes κ and, inductively, for all stages β < α. For f, g ∈ M_{κ}^{α}, κ ⊧ “f ∈_{α} g” iff for some h ∈ g(κ) and β < α, κ ⊧ “f=_{β}h”. Notice that the sequence of ∈_{α}s is monotonically non-decreasing, that is, if f ∈_{α} g and γ > α then f ∈_{γ} g. This holds because the defining condition of ∈_{α} remains true if α is increased. Regarding =, κ ⊧ “f=_{α}g” iff for all λ ∈ dom(f) ∪ dom(g), h ∈ (f_{κλ}(f))(λ), λ ⊧ “h ∈_{α} f_{κλ}(g)”, and for all h ∈ (f_{κλ}(g))(λ), λ ⊧ “h ∈_{α} f_{κλ}(f)”. Notice that the sequence of =_{α}s is non-decreasing, because, in the defining condition, α appears only in ∈_{α}, ∈_{α} appears only positively, and ∈_{α} is already known to be non-decreasing. Furthermore, ∈_{α} and =_{α} are non-increasing for a fixed collection of sets. That is, for α = max(rk f, rk g), κ ⊧ “f ∈_{α} g” iff for some γ > α κ ⊧ “f ∈_{γ} g”, and similarly for =_{α}. This can be proved by a mutual induction. Finally, let ∈ be ⋃_{β∈ORD} ∈_{β}, i.e. κ ⊧ “f ∈ g” iff for some β κ ⊧ “f ∈_{β} g”, and similarly for =.

Considering definability again, both ∈ and = are Δ_{1}-definable ternary relations (i.e. κ ⊧ f ∈ g and κ ⊧ f = g). This is based on two facts. First, for α = max(rk f, rk g), κ ⊧ “f ∈ g” iff κ ⊧ “f ∈_{α} g”, and similarly for =. Second, ∈_{α} and =_{α} are defined by a simultaneous recursion which contains only bounded quantification and recursive calls.

Lemma 2.0.1 The transition functions respect the primitive relations ∈ and =.

proof: It suffices to show that the transition functions respect ∈_{α} and =_{α}. This can be done by a simultaneous induction on α. The case of ∈_{α} is trivial. To show κ ⊧ f=_{α}g implies μ ⊧ f_{κμ}(f)=_{α}f_{κμ}(g), if μ ∈ dom(f) ∪ dom(g), then this is trivial, since the only effect of f_{κμ} is to shrink the set of λ’s that need be considered. Otherwise one has to unravel the definition of f_{κμ}, which again brings us to consider those λs in dom(f) ∪ dom(g). The details are left to the reader.

Lemma 2.0.2 = (as defined above) satisfies the equality axioms.

proof: 1. 0 ⊧ ∀x x = x: Assume inductively that for all x ∈ M_{κ}^{β} (β < α) κ ⊧ x=_{β}x and that f ∈ M_{κ}^{α}. We need to show that κ ⊧ f=_{α}f, i.e. for all λ ∈ dom(f), h ∈ (f_{κλ}(f))(λ), λ ⊧ “h ∈_{α} f_{κλ}(f)”. Since λ ∈ dom(f), f_{κλ} operates via restriction, so the condition to be proved simplifies to for all λ ∈ dom(f), h ∈ f(λ), λ ⊧ “h ∈_{α} f_{κλ}(f)”. Given such a λ and h, by the definition of ∈_{α}, we need a g ∈ f(λ) and β so that λ ⊧ “h=_{β}g”. Letting g be h and β be rk(h), the inductive hypothesis gives exactly this.

2. 0 ⊧ ∀x, y x = y → y = x: Trivial, because the definition of ∈_{α} was symmetric in f and g.

3. 0 ⊧ ∀x, y, z x = y ∧ y = z → x = z: As in 1, the transitivity of =_{α} is proven inductively on α. The technical difficulty here is that we must consider the domains of arbitrary Kripke sets f, g, and h, which might all differ. Possibly the easiest way to do this is to start with the observation that, for arbitrary λ ≥ κ, (f_{κλ}(f))(λ) = ⋃_{μ≤λ,μ∈dom(f)} f_{μλ}”f(μ). So when evaluating κ ⊧ f=_{α}h, after being led to consider i ∈ (f_{κλ}(f))(λ), we can conclude that i ∈ f_{μλ}”f(μ) for some μ ∈ dom(f). Using a pre-image i_{μ} of i in f(μ) and the postulated equality of f and g, one finds a ν ∈ dom(g), ν ≤ μ, a pre-image i_{ν} of i_{μ}, and a j_{ν} ∈ g(ν) such that i_{ν} =_{β} j_{ν}. Then one finds a ξ ≤ ν, j_{ξ} ∈ g(ξ), k_{ξ} ∈ h(ξ) such that j_{ξ} =_{γ} k_{ξ}. At this point one uses the monotonicity of = to move up to δ = max(β, γ), the inductively assumed transitivity of =_{δ} to get that i_{ξ} =_{δ} k_{ξ}, and the fact that the transition functions respect the primitive relations to conclude λ ⊧ “i ∈_{α} h”. The details are left to the reader.

4. 0 ⊧ ∀x, y, z x = y ∧ x ∈ z → y ∈ z: If κ ⊧ “f=g ∧ f ∈ h”, then κ ⊧ “f=i” for some i ∈ h(κ). By the transitivity of =, κ ⊧ “g=i”.

5. 0 ⊧ ∀x, y, z x = y ∧ z ∈ x → z ∈ y: If κ ⊧ “f=g ∧ h ∈ f”, then for some i ∈ f(κ) κ ⊧ “h=i”, and also κ ⊧ “i ∈ g”. That means that for some j ∈ g(κ) κ ⊧ “i=j”. By the transitivity of =, κ ⊧ “h=j”, and hence also “h ∈ g”.

With ∈ and = defined, the description of the model M is complete. The definability of M follows automatically from the work above. Since the universes at each node and the primitive relations (there being no primitive functions) are definable, the definability of the satisfaction relation κ ⊧ ϕ comes directly from the inductive determination of satisfaction in Kripke models. Furthermore, while we make no claim along the lines of Σ_{n}-satisfaction being Σ_{n} definable, it is true that Δ_{0}-satisfaction (i.e. κ ⊧ ϕ, ϕ a Δ_{0} formula) is Δ_{1} definable, as follows. In the inducive definition of satisfaction in Kripke models (when restricting to Δ_{0} formulas), the only times an unbounded quantifier is introduced are for the clauses ∀ and →, when the collection of nodes is quantified over. Such quantification can be eliminated by restricting it to the maximum κ of the domains of the parameters, because the formula is true at κ iff it’s true at any later node, this last fact being provable inductively. (A different proof, which shows the same fact without the restriction of ϕ being Δ_{0}, is that there is an isomorphism between the Kripke model from κ on and the model from λ on, where λ is any ordinal > κ. This latter argument is given in detail in the proof of Separation later in this section.)

What remains is to show that M has the desired properties.

Theorem 2.0.3 M ⊧ CZF + ¬ Power Set

proof: The simpler axioms of CZF are Pairing, Union, and Infinity, and the proofs that they hold in M are left to the reader. What we will show are Extensionality, Set Induction, Restricted Separation, Subset Collection, Strong Collection, and, of course ¬ Power Set. As promised above, we will go beyond CZF and show full Separation.

Extensionality: What needs to be shown is ∀x ∀y (x = y ↔ ∀z (z ∈ x ↔ z ∈ y)). The implication → follows easily from equality property 5. in the previous proposition. For the implication ←, given sets f and g and node κ, let α = max(rk f, rk g). To show that f=_{α}g is precisely, by definition, ∀λ ∈ dom(f) ∪ dom(g), h ∈ (f_{κλ}(f))(λ), λ ⊧ “h ∈_{α} f_{κλ}(g)”, and vice versa. So let h be a member of (f_{κλ}(f))(λ). By assumption, we have κ ⊧ “∀z (z ∈ f ↔ z ∈ g))”. This holds in particular for h: λ ⊧ “h ∈ (f_{κλ}(f)) ↔ h ∈ (f_{κλ}(g))”. In order to use this, we need that λ ⊧ “h ∈ (f_{κλ}(f))”, when what we have is merely h ∈ (f_{κλ}(f))(λ). Unraveling the definition of λ ⊧ x ∈_{β} y and making the obvious choices along we way, this reduces to showing that λ ⊧ h=_{β}h for some β. Letting β be rk(h), this follows from the proof (albeit not the statement) of the first equality axiom (previous proposition). Hence we can conclude that λ ⊧ “h ∈ (f_{κλ}(f)) ↔ h ∈ (f_{κλ}(g))”. What we still need is that λ ⊧ “h ∈_{α} f_{κλ}(g)”. That this is the case was already observed while defining ∈_{α} and =_{α}. The other direction (“vice versa”) is symmetric in f and g. The details are left to the reader.

Set Induction: This is easy, because the Kripke sets were defined inductively. That is, given an appropriate property ϕ(x), one would show that ϕ(x) holds for all members of M^{α} inductively on α.

Restricted Separation: In fact, full Separation holds. Let κ be a node, a a set in M_{κ}, and ϕ a formula (with free variable x) over (i.e. with parameters from) M_{κ}. Let λ > κ include not only dom(a) but also the domains of all of ϕ’s parameters. For μ > κ we will use the notation f_{κμ}(ϕ)(x) to mean ϕ(x, f_{κμ}(b_{0}), ... , f_{κμ}(b_{n−1})), where the b_{i}’s list all of ϕ’s parameters. In V, let Sep_{a,ϕ} be a function with domain λ + 1\κ such that for all μ in this domain

Sep_{a,ϕ}(μ) = {x ∈ (f_{κμ}(a))(μ) | μ ⊧ f_{κμ}(ϕ)(x)}.

This function Sep_{a,ϕ} is definable in V because M is, and it should be clear that for all μ ∈ dom(Sep_{a,ϕ}), x ∈ M_{μ},

μ ⊧ “x ∈ f_{κμ}(Sep_{a,ϕ}) ↔ x ∈ f_{κμ}(a) ∧ f_{κμ}(ϕ)(x)”.

We need only show why the same holds also for μ > λ. The idea is that beyond λ nothing relevant (i.e. a or ϕ) is changing anymore, and so Sep_{a,ϕ} need not change either. In detail, for any such μ, by the choice of λ, f_{λμ} is an isomorphism on f_{κλ}(a), f_{κλ}(ϕ), and f_{κλ}(Sep_{a,ϕ}), the nature of which is replacing the domains in the transitive closures of the sets in question, which are all {λ}, with {μ}. This isomorphism can be extended to one between M_{λ} and M_{μ} by hereditarily replacing ordinals in the domains, necessarily of the form λ+ξ, with μ + ξ. Under this isomorphism, {x ∈ M_{λ} | λ ⊧ “x ∈ f_{κλ}(a) ∧ f_{κλ}(ϕ)(x)”}, i.e. Sep_{a,ϕ}(λ), gets mapped to {x ∈ M_{μ} | μ ⊧ “x ∈ f_{λμ}(f_{κλ}(a)) ∧ f_{λμ}(f_{κλ}(ϕ))(x)”}. By the composition property of transition functions (f_{στ} ∘ f_{ρσ} = f_{ρτ}, a necessary condition on all Kripke models), we have the desired result.

Subset Collection: Let κ ∈ ORD, a, b ∈ M_{κ}. Let λ ⊇ dom(a), dom(b). SubColl_{a,b} will have domain λ + 1\κ. For all μ in this domain, let

SubColl_{a,b}(μ) = {x ∈ M_{μ} | μ ⊧ “x is a total relation from a to b”}.

It is immediate that for all μ ∈ dom(SubColl_{a,b}), x ∈ M_{μ},

μ ⊧ “x ∈ f_{κμ}(SubColl_{a,b}) ↔ x is a total relation from a to b”.

For μ > λ, the idea is that from λ to μ neither a nor b has changed. So if node μ forces x to be a total relation from a to b, then any ordered pairs that might enter x at a later node can be disregarded and x would still remain total, since a doesn’t grow any more. Furthermore, the ordered pairs at node μ can be “pulled back” to node λ, since neither a nor b grew from λ to μ. This (possibly truncated) version of x was put into SubColl_{a,b} by at latest node λ, and is indeed a total sub-relation of x.

In more detail, observe that for any such μ, by the choice of λ, f_{λμ} is an isomorphism on f_{κλ}(a) and f_{κλ}(b). Let μ ⊧ “x is a total relation from f_{κμ}(a) to f_{κμ}(b)”. Then x(μ) is a total relation from (f_{κμ}(a))(μ) to (f_{κμ}(b))(μ). This induces via the isomorphism a total relation from (f_{κλ}(a))(λ) to (f_{κλ}(b))(λ); let z be the function with domain {λ} and z(λ) being this relation. λ ⊧ “z is total” since a doesn’t change beyond λ, so λ ⊧ “z ∈ SubColl_{a,b}”. By the construction of z, μ ⊧ f_{λμ}(z) ⊆ x.

Strong Collection: Let κ be a node, a a set in M_{κ}, and ϕ a formula (with free variable x) over (i.e. with parameters from) M_{κ}, such that κ ⊧ “∀x ∈ a ∃y ϕ(x, y)”. Let λ > κ include not only dom(a) but also the domains of all of ϕ’s parameters. As above, the notation f_{κμ}(ϕ)(x) means ϕ(x, f_{κμ}(b_{0}), ... , f_{κμ}(b_{n−1})), where the b_{i}’s list all of ϕ’s parameters. In V, a function StrColl_{a,ϕ} with domain λ + 1\κ can be constructed so that for all μ and ν in this domain with μ < ν,

∀x ∈ a(μ) ∃y ∈ StrColl_{a,ϕ}(μ) μ ⊧ ϕ(x, y),
∀y ∈ StrColl_{a,ϕ}(μ) ∃x ∈ a(μ) μ ⊧ ϕ(x, y),

and f_{μν}”StrColl_{a,ϕ}(μ) ⊆ StrColl_{a,ϕ}(ν). StrColl_{a,ϕ} clearly acts as a bounding set at all nodes through λ. Beyond λ the idea is that nothing relevant (i.e. a or ϕ) is changing anymore, and so StrColl_{a,ϕ}need not change either. The argument is essentially the same as that for Restricted Separation, and is left to the reader.

¬ Power Set: For κ ∈ ORD, let 1_{κ} be the Kripke set with domain κ + 1 such that for λ < κ 1_{κ}(λ) = ∅ and 1_{κ}(κ) = ⟨κ, ∅⟩. 0 ⊧ “1_{κ} ⊆ 1 =_{def} {0}”, but by the set-sized nature of the members of M, no set contains all of the 1_{κ}’s. Therefore 1 has no power set in M.

3 Exponentiation does not imply Subset Collection

We will provide a Kripke model of CZF - Subset Collection + Exponentiation + ¬ Subset Collection. Furthermore, full Separation will hold.

The model to be built in this section is an extension of that from the previous section, and ultimately can be defined only in a generic extension of V. These sets, though, will be named by terms in V and so we will work in V at first to identify the terms. When the terms are interpreted, they will be functions just as in the last section, and so their domains will also be given during their inductive generation.

The terms are defined inductively on the ordinals. At stage 0, at any node κ, there is a term f_{0κ}(G_{λ}), which will be interpreted as a function with domain [κ, max(κ, λ)]. (For κ = 0, these will be referred to more simply as G_{λ}.) (Of course, in this context the symbol “f_{0κ}” is just a piece of syntax. It should, however, remind you of the transition function from node 0 to κ. In an attempt to reduce notation, we will use the same notation for a term as for its interpretation, hence the double meaning of “f_{0κ}”.) At any later stage, if a is a term at node κ, then so is Union(a) (with the same domain); if a is a term at node κ, ϕ is a Δ_{0} formula (in which all of the parameters are terms at node κ), and λ > κ, then Sep_{a,ϕ,λ} is a term at node κ with domain [κ, λ); and if a function is build via the inductive construction of the previous section (given at the bottom of p. 3), then it is also a term in which the node and domain of definition are explicit.

Concerning the interpretation of these terms, we introduce some notation. For an integer n and node κ, n_{κ}^{M} is the internal version of n; that is, 0_{κ}^{M} = ⟨κ, ∅⟩ and n+1_{κ}^{M} = ⟨κ, n_{κ}^{M} ∪ {n_{κ}^{M}}⟩. Let N_{κ}^{M} be {n_{κ}^{M} | n ∈ N}. (Notice that N_{κ}^{M} is not actually a set M; if we had instead wanted to define the internal version of the natural numbers, say, that would be ⟨κ, N_{κ}^{M}⟩ (or a variant thereof).)

Let G be a generic relation on N. That is, G is generic over V for the forcing partial order which consists of functions from finite subsets of N × N to 2; p extends q (written “p ≥ q”) if p extends q as a function, i.e. p ⊇ q. A generic can be identified with a total function F : N × N → 2; letting G be { ⟨m, n⟩ | F(⟨m, n⟩) = 1 }, G is then a generic relation on N. Notice that by genericity, both G and G^{−1} are total.

In V[G], let G_{κ}^{M} be { ⟨m_{κ}^{M}, n_{κ}^{M}⟩^{M} | ⟨m, n⟩ ∈ G } (where ⟨, ⟩^{M} means the M-internal ordered pair function) . Similarly, let (N×N)_{κ}^{M} be { ⟨m_{κ}^{M}, n_{κ}^{M}⟩^{M} | m, n ∈ N_{κ}^{M} }.

Using the G_{κ}^{M}s, we can now provide an interpretation for the terms. (Remember, we are using the same notation for the interpretation of a term as for the term itself; whether a term or its interpretation is meant should be clear from the context.) For f_{0κ}(G_{λ}), f_{0κ}(G_{λ})(μ) = G_{μ}^{M} for μ < λ (the internal version of G), and f_{0κ}(G_{λ})(λ) = (N×N)_{κ}^{M} otherwise (the full relation on N). Union(a)(κ) (where κ ∈ dom(a)) is ⋃_{f∈a(κ)} f(κ). The interpretation of Sep_{a,ϕ,λ} is similar to that of Sep_{a,ϕ} in the previous section (See the proof of Restricted Separation), only there an essentially arbitrary λ was chosen (the only requirement being that λ be big enough), whereas here the λ in question is a part of the term and the size restriction is dropped. So for μ ∈ [κ, λ),

Sep_{a,ϕ,λ}(μ) = {x ∈ (f_{κμ}(a))(μ) | μ ⊧ f_{κμ}(ϕ)(x)}.

The interpretation of a function is straightforward: mod the above mentioned identification of terms with their interpretations, there is literally nothing to do.

Of course, to have a Kripke model, we need some other facts and definitions; indeed, the interpretation above is dependent upon some of these, which would therefore need to be proven and defined simultaneously with this inductive interpretation. That is, we need to define transition functions f_{κμ}, show that they cohere (i.e. f_{λμ}∘ f_{κλ} = f_{κμ}), and show that the Kripke sets are non-decreasing (i.e. if κ ⊧ a ∈ b then μ ⊧f_{κμ}(a) ∈ f_{κμ}(b)). We will leave the details to the reader, and content ourselves with one observation. Since λ was pointedly left out of the domain of Sep_{a,ϕ,λ}, for all μ ≥ λ including λ itself

Sep_{a,ϕ,λ}(μ) = ⋃_{ν∈[κ,lambda)} f_{νμ}”Sep_{a,ϕ,λ}(ν).

Notice that M (i.e. κ ⊧ ϕ) is definable in V[G]. In particular, as in the previous section, Δ_{0}-satisfaction is Δ_{1}. Furthermore, since G is set-generic over V, by general forcing technology, p |⊢ “κ ⊧ ϕ” is definable in V, and, in particular, p |⊢ “κ ⊧ ϕ”, ϕ Δ_{0}, is Δ_{1}.

Theorem 3.0.4 M ⊧ CZF - Subset Collection + Exponentiation + ¬ Subset Collection

proof: Extensionality, Set Induction, and Infinity are left to the reader.

Union: This follows from the presence (and meaning) of the terms of the form Union(a).

Pairing: Given a, b ∈ M_{κ}, let λ include dom(a) and dom(b). For μ ∈ λ\κ let f(μ) be {f_{κμ}(a), f_{κμ}(b)}, which suffices. Notice that f is definable even if a or b is just a term, so that f exists at least as a term in V (even if inductively uninterpretable in V).

Restricted Separation: This follows from the presence (and meaning) of the terms of the form Sep_{a,ϕ,λ}, with the proof being essentially that in the previous section. The one change is that the isomorphism given there must be extended to account for terms of the form Gκ (the other terms already being accounted for inductively). Under this isomorphism, G_{λ+ξ} is to be sent to G_{μ+ξ}.

In fact, full Separation holds, even though the separation terms are only for Δ_{0} formulas. The first guess as to how to proceed is as follows. Given a and ϕ a term and formula in (resp. over) M_{κ}, let λ > κ include the domains of a and of ϕ’s parameters. Let μ > λ be such that V_{μ}[G] contains a, ϕ’s parameters, and is a Σ_{n} elementary substructure of V[G] for n sufficiently large (i.e. large enough to reflect the truth of ϕ(x) in M). Let f be the function with domain μ\κ such that f(ν) = { g ∈ V_{μ} | g is a term naming an element of M_{ν} }. The notation “ϕ^{f}” means “ϕ with all of the unbounded variables bounded by f”. By the choice of μ, ϕ(x) is interpreted in M (in V[G]) just as ϕ(x) would be in V_{μ}[G]’s version of M. If in turn that could be captured as Sep_{a,ϕ^{f} ,μ} (in V[G]), then we’d be done.

The problem is that, while f reflects the restriction to M^{μ}, it cannot reflect the restriction of P from ORD to μ. To give a concrete example, let ϕ be the sentence “∀x ∀y x = y ∨ x ≠ y”. In M, this sentence is never true, and so any separation set for ϕ should be the empty set. However, for any choice of f, ϕ^{f} eventually becomes true (at latest beyond f’s domain), so Sep_{a,ϕ^{f} ,μ} eventually becomes a.

We need some way of saying “don’t look beyond this node.” This can be done with a technique developed in its essence by Friedman and Scedrov. In [4], they consider a particular formula ψ (in the notation to be introduced) and a particular Kripke model; moreover, their model was a two-node model, so their M_{pre−ψ} (see below) was a classical and not even a Kripke structure. Nonetheless, their work is easily generalized to all formulas and all models. To have this generalization shown, and to keep this paper self-contained, we develop the details.

Let ψ be a sentence, possibly with parameters from the universe at the bottom node ⊥ in some Kripke model M. Using ψ, a transformation on the formulas can be defined inductively. If ϕ is atomic (including ⊥, the always false statement), then ϕ^{∗} is ϕ ∨ ψ. The inductive clauses are transparent to this construction: (ϕ_{0} → ϕ_{1})^{∗} = (ϕ_{0}^{∗} → ϕ_{1}^{∗}), ∀x ϕ(x) = ∀x ϕ^{∗}(x), etc. It is easy to see inductively on ϕ that for all formulas ϕ and all nodes σ with σ ⊧ ψ, σ ⊧ ϕ^{∗}. Let M_{pre−ψ} be M with all the nodes where ψ holds thrown out. That is, M_{pre−ψ}’s underlying partial order is the initial sub-order of M’s P consisting of {σ|σ |̸= ψ} =_{def} P_{pre−ψ} (which is assumed to be non-empty, i.e. ⊥ |̸= ψ). The universe of M_{pre−ψ} at σ is the same as for M, the transition functions are the same, the atomic relations and functions have the same interpretation. Because nodes in M_{pre−ψ} are also nodes in M, we will distinguish notationally truth in M_{pre−ψ} from truth in M with ⊧_{M_{pre−ψ}} versus ⊧_{M}.

Lemma 3.0.5 σ ⊧_{M} ϕ^{∗} iff σ ⊧_{M_{pre−ψ}} ϕ.

proof: By induction on ϕ.

• ϕ atomic: σ ⊧_{M} ϕ^{∗} iff σ ⊧_{M} ϕ ∨ ψ. Since by hypothesis σ |̸=_{M} ψ, this is equivalent to σ ⊧_{M} ϕ, which is itself equivalent to σ ⊧_{M_{pre−ψ}} ϕ, since M_{pre−ψ} is a restriction of M and the atomic relations are defined locally. (Although this lemma is very general, the reader can be excused for thinking of models of set theory, and ask whether equality as defined by “same members” really holds. Note we do not claim that Extensionality is preserved! The equality in M is taken as primitive.)

• ϕ_{0} ∨ ϕ_{1}: σ ⊧_{M} ϕ_{0}^{∗} ∨ ϕ_{1}^{∗} iff σ ⊧_{M} ϕ_{0}^{∗} or σ ⊧_{M} ϕ_{1}^{∗} iff (inductively) σ ⊧_{M_{pre−ψ}} ϕ_{0} or σ ⊧_{M_{pre−ψ}} ϕ_{1} iff σ ⊧_{M_{pre−ψ}} ϕ_{0} ∨ ϕ_{1} .

• ϕ_{0} ∧ ϕ_{1}: Analogous to ∨.

• ϕ_{0} → ϕ_{1}: It has already been observed that:

for τ ∈ P\P_{pre−ψ}τ ⊧_{M} ϕ_{0}^{∗} ∧ ϕ_{1}^{∗}.

So for σ ∈ P_{pre−ψ}, σ ⊧_{M} ϕ_{0}^{∗} → ϕ_{1}^{∗} reduces to:

for all extensions τ ∈ P_{pre−ψ} of σ, if τ ⊧_{M} ϕ_{0}^{∗} then τ ⊧_{M} ϕ_{1}^{∗}.

Inductively, this is equivalent to:

for all extensions τ ∈ P_{pre−ψ} of σ, if τ ⊧_{M_{pre−ψ}} ϕ_{0} then τ ⊧_{M_{pre−ψ}} ϕ_{1}, i.e. σ ⊧_{M_{pre−ψ}} ϕ_{0} → ϕ_{1}.

• ∀x ϕ(x): It has already been observed that:

for τ ∈ P\P_{pre−ψ} and x ∈ M_{τ} , τ ⊧_{M} ϕ^{∗}(x). So for σ ∈ P_{pre−ψ}, σ ⊧_{M} ∀x ϕ^{∗}(x) reduces to: for all extensions τ ∈ P_{pre−ψ} of σ and x ∈ M_{τ} , τ ⊧_{M} ϕ^{∗}(x). Inductively, this is equivalent to: for all extensions τ ∈ P_{pre−ψ} of σ, and x ∈ M_{τ} , τ ⊧_{M_{pre−ψ}} ϕ(x), i.e. σ ⊧_{M_{pre−ψ}} ∀x ϕ(x).

• ∃x ϕ(x): σ ⊧_{M} ∃x ϕ^{∗}(x) iff for some x ∈ M_{σ} σ ⊧_{M} ϕ^{∗}(x) iff (inductively) for some x ∈ M_{σ} σ ⊧_{M_{pre−ψ}} ϕ(x) iff σ ⊧_{M_{pre−ψ}} ∃x ϕ(x).

To return to the issue at hand, let ψ be the sentence “0 ∈ 1_{μ}”, where μ is as above. (Recall that 1_{μ} is defined so that ψ is true exactly at nodes μ and beyond.) This choice of ψ determines a *-transformation on formulas. Then Sep_{a,ϕ^{f∗},μ} (equivalently, Sep_{a,ϕ^{∗f} ,μ}) is as desired. That is, we claim that

κ ⊧ ∀x (x ∈ Sep_{a,ϕ^{∗f} ,μ} ↔ (x ∈ a ∧ ϕ(x))).

(In what follows, we suppress mention of the transition functions f_{κλ}, for purposes of readability, preferring instead to write the incorrect “λ ⊧ x ∈ a” instead of “λ ⊧ x ∈ f_{κλ}(a)”, to give only a mild example of what the reader would otherwise be in for.)

First suppose that κ ≤ λ < μ and x ∈ M_{λ}. (In this paragraph, we suppress mention of the transition functions f_{κλ}, for purposes of readability, preferring instead to write the incorrect “λ ⊧ x ∈ a” instead of “λ ⊧ x ∈ f_{κλ}(a)”, to give only a mild example of what the reader would otherwise be in for.) If x ∉ M^{μ} then x gets into neither a nor Sep_{a,ϕ^{∗f} ,μ}, and we’re done. Otherwise, by the choice of μ,

λ ⊧ “x ∈ a ∧ ϕ(x)” iff V_{μ}[G] ⊧ “λ ⊧ “x ∈ a ∧ ϕ(x)””.

The difference between M (in V[G]) and V_{μ}[G]’s version thereof is the partial order (ORD vs. μ) and the ordinal length of the inductive generation of terms (again, ORD vs. μ). The former is captured by ψ, the latter by f; notationally, M as interpreted in V_{μ}[G] is M_{pre−ψ}^{μ}. So

V_{μ}[G] ⊧ “λ ⊧ “x ∈ a ∧ ϕ(x)”” iff λ ⊧_{M_{pre−ψ}} “x ∈ a ∧ ϕ^{f}(x)”.

By the previous lemma, the latter is equivalent to λ ⊧ “x ∈ a ∧ ϕ^{f∗}(x)”. By the interpretation of Sep-terms, the latter is equivalent to λ ⊧ “x ∈ Sep_{a,ϕ^{f∗},μ}”.

Now consider the case λ ≥ μ, x ∈ M_{λ}. Since λ ≥ μ > dom(a), if λ ⊧ “x ∈ a” then there are ν < μ and y ∈ M_{ν} such that x = f_{νμ}(y) and ν ⊧ “y ∈ a”. Withough loss of generality ν can be chosen to be larger than the domains of a and ϕ’s parameters. For any such ν and y, by the same isomorphism argument as in the last section, ν ⊧ ϕ(y) iff λ ⊧ ϕ(x). Furthermore, since a ∈ V_{μ}[G] (by the choice of μ), y is not only in M_{ν} but also M_{ν}^{μ}. Combining all of this with the definition of f_{κλ}(Sep_{a,ϕ^{f∗},μ}) (which was highlighted just before the statement of the current theorem), we get the following equivalences:

λ ⊧ “x ∈ a ∧ ϕ(x)” ⟷

∃ν < μ, y ∈ M_{ν}^{μ} (x = f_{νλ}(y) ∧ ν ⊧ “y ∈ a ∧ ϕ(y)”) ⟷

(by the case above: κ ≤ λ < μ, with ν here playing the role of λ)

∃ν < μ, y ∈ M_{ν}^{μ} (x = f_{νλ}(y) ∧ ν ⊧ “y ∈ Sep_{a,ϕ^{f∗},μ}”) ⟷

∃ν < μ, y ∈ M_{ν} (x = f_{νλ}(y) ∧ ν ⊧ “y ∈ Sep_{a,ϕ^{f∗},μ}”) ⟷

λ ⊧ “x ∈ Sep_{a,ϕ^{f∗},μ}”.

Strong Collection: In the presence of full Separation (see last paragraph), Strong Collection follows from Collection. Suppose κ ⊧ ∀x ∈ a ∃y ϕ(x, y). Let λ, μ and f be as in the last paragraph. Then κ ⊧ “f is a bounding set for ϕ on a”.

Exponentiation: In order to highlight exactly why the following argument works for functions (yielding Exponentiation) but not for arbitrary relations (hence not yielding Subset Collection), it will be presented in terms of a relation R until exactly that moment when we need to use that R is not only a relation but also a function.

So let a and b be terms for sets in M_{κ}, and p a forcing condition, R a term, and λ ≥ κ an ordinal so that p |⊢ “λ ⊧ R is a relation from a to b”. Since the property of being a relation between two given sets is Δ_{0}, the assertion p |⊢ “λ ⊧ R is a relation from a to b” is Δ_{1} in V. We will use later the same result for the property of R being a function from a to b.

Let H be the Σ_{1}-Skolem hull of {a, b, κ, λ, R} ∪ TC(a) ∪ TC(b) ∪ κ, of the same size as that set (where “TC” stands for transitive closure). Let ρ be the transitive collapsing function. Then

ρ”H ⊧ “ρ(p) |⊢ “ρ(λ) ⊧ ρ(R) is a relation from ρ(a) to ρ(b)””.

ρ fixes p, a, and b because L_{ω}, TC(a), and TC(b) ⊆ H. Furthermore, ρ(λ) ≤ λ, so for some μ ≤ λ

ρ”H ⊧ “p |⊢ “μ ⊧ ρ(R) is a relation from a to b””,

and, by the same reasoning, for all q ≥ p,

H ⊧ “q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ R”” iff ρ”H ⊧ “q |⊢ “μ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)””.

However, the assertion “q |⊢ “μ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)”” is Δ_{1} over both V and ρ”H (as the collapse of a Σ_{1} substructure of V), hence is absolute (between ρ”H and V), as is “q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ R”” between H and V. Therefore

q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ R” iff q |⊢ “μ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)”.

Since μ ≤ λ

if q |⊢ “μ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)” then q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)”.

Combining the last two assertions,

if q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ R” then q |⊢ “λ ⊧ ⟨x_{a}, y_{b}⟩ ∈ ρ(R)”,

i.e. p |⊢ “λ ⊧ R ⊆ ρ(R)”.

Under the assumption merely that R is a relation, no more can be said. If, however, p |⊢ “λ ⊧ R is a (total) function (from a to b)”, then, by analogous arguments to those above,

H ⊧ “p |⊢ “λ ⊧ R is a function””,

ρ(H) ⊧ “p |⊢ “μ ⊧ ρ(R) is a function””,

p |⊢ “μ ⊧ ρ(R) is a function”, and

p |⊢ “λ ⊧ ρ(R) is a function”.

Since a (total) function cannot be properly extended to a function, p |⊢ “R = ρ(R)”.

By the cardinality constraint on H, there is an ordinal α (independent of λ and R) such that ρ”H ⊆ V_{α}. In particular, ρ(R) ∈ V_{α}. Let g be the function with domain α\κ such that g(ν) = { h ∈ V_{α} | h is a term naming an element of M_{ν} }. Then g is a bounding set for ^{a}b. By Separation (Restricted Separation suffices here), ^{a}b is a set.

¬ Subset Collection: Suppose that κ ⊧ “for all total relations R on N there is a total subrelation R’, R’ ∈ F”. There is an ordinal λ such that, for all terms G_{μ} in the transitive closure of F, μ < λ; without loss of generality, λ > κ. Since for every such μ λ ⊧ G_{μ} = N × N, f_{κλ}(F) can be evaluated in V. By assumption, λ ⊧ “there is a total subrelation of G_{λ} in f_{κλ}(F)”. This is, however, impossible, by the genericity of G, as follows. Let λ ⊧ “R’ ∈ f_{κλ}(F)”. In V, R’(λ) can be identified with a total relation on N (and so we will use the same notation R’(λ) for this relation in V). Let p be a forcing condition. Since p is finite and R’(λ) total, let ⟨m, n⟩ ∈ R’(λ) be such that ⟨m, n⟩ ∉ dom(p), and let q be p ∪⟨⟨m, n⟩, 0⟩. q |⊢ “R’(λ) is not a subrelation of G”, so q |⊢ “λ |̸= “R’ is a subrelation of G_{λ}””. Hence the set of conditions forcing λ |̸= “R’ is a subrelation of G_{λ}” is dense, and so in V[G] λ |̸= “R’ is a subrelation of G_{λ}”. This however contradicts the construction of λ, so the assumption on κ is false, and Subset Collection fails for relations on N.

4 Reflection

Although this article is about Power Set and its variants, a result about Collection and its variants is right there, and so should be pointed out. Classically, over the other axioms of ZF, Reflection, Collection, and Replacement are equivalent. The proofs that Reflection implies Collection, which in turn implies Replacement are soft and easy proofs, and so carry over verbatim to intuitionistic logic. The reverse implications are less obvious and make essential use of classical logic; the standard proofs do not carry over. In fact, it was shown in [4] that Replacement does not imply Collection over the remaining axioms of IZF. It is natural to ask whether the same can be said of Collection and Reflection. Although this is still unknown, the first construction of this paper provides a model of CZF + Separation + ¬ Reflection. The only axiom that’s missing from IZF is Power Set, and Subset Collection is at least a partial substitute.

Moreover, the failure of Reflection is very strong. All true Π_{1} facts are reflected in any transitive set, and any true Σ_{1} sentence is reflected in any transitive set that contains a witness. In contrast, consider ¬∀x ∀y (x = y ∨x ≠ y). This is true in the whole model, and false in every set.

References

[1] P. Aczel, The type theoretic interpretation of constructive set theory, in A. MacIntypre, L. Pacholski, and J. Paris (eds.), Logic Colloquium ’77 (North-Holland, Amsterdam, 1978), p. 55-66

[2] P. Aczel, The type theoretic interpretation of constructive set theory: choice principles, in A.S. Troelstra and D. van Dalen (eds.), The L.E.J. Brouwer Centenary Symposium (North-Holland, Amsterdam, 1982), p. 1-40

[3] P. Aczel, The type theoretic interpretation of constructive set theory: inductive definitions, in R.B. Marcus et al. (eds.), Logic, Mathodology and Philosophy of Science VII (North-Holland, Amsterdam, 1986), p. 17-49

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

[5] P. Martin-Löf, An intuitionistic theory of types: predicative part, in H.E. Rose and J. Sheperdson (eds.), Logic Colloquium ’73 (North-Holland, Amsterdam, 1975), p. 73-118

[6] P. Martin-Löf, Intuitionistic Type Theory (Bibliopolis, Naples, 1984)

[7] J. Myhill, Constructive set theory, Journal of Symbolic Logic, 1975, p. 347-382 [8] M. Rathjen, The strength of some Martin–Löf type theories, Archive for

Mathematical Logic, 1994, p. 347-385ff

[9] M. Rathjen, The higher infinite in proof theory, in J.A. Makowsky and E.V.ffRavve (eds.), Logic Colloquium ’95, Springer Lecture Notes in Logic, Vol. 11 (Springer, New York, Berlin, 1998), p. 275-304ff