Topological Forcing Semantics with Settling

Robert S. Lubarsky

Department of Mathematical Sciences, Florida Atlantic University 777 Glades Road Boca Raton, FL 33431, USA

                                       rlubarsk@fau.edu

August 24, 2008

Abstract

The semantics introduced in [3] is extended to all topological spaces.

1 Introduction

The standard topological semantics, as introduced in [1] (or see instead [2] by the same author), has been generalized in various ways, most notably via categorical semantics. (For a good introduction, see [4].) Here is introduced, not a generalized, but rather an alternative semantics instead.

An instance of this semantics was already applied in [3] to the reals as a topological space. The purpose there was to come up with a model of CZF_{Exp} set theory in which the Dedekind cuts do not form a set. CZF_{Exp} contains the Axiom of Exponentiation (the existence of function spaces), but not any stronger Power Set-like axiom, most notably Aczel’s Subset Collection, which suffices to prove the Dedekind cuts are a set. The essence of the construction there is that, as in a traditional topological model, the truth value of set membership (σ ∈ τ, where σ and τ are terms) is an open set of ℝ, but at any moment the terms under consideration can collapse to ground model terms. (A ground model term is the canonical image of a ground model set – think of the standard embedding of V into V[G] in classical forcing.) Such a collapse does not make the variable sets disappear, though. So no set could be the Dedekind cuts: any such candidate could at any time collapse to a ground model set, but then it wouldn’t contain the canonical generic because that’s a variable set, and this generic, over ℝ, is a Dedekind cut. ^{1}

1For those already familiar with a similar-sounding construction by Joyal, this is exactly what distinguishes the two. Joyal started with a topological space T, and took the union of T with a second copy of T, the latter carrying the discrete topology (i.e. every subset is open).

So by Joyal, you could specialize at a point, but then every set is also specialized there. Here, you can specialize every set you’re looking at at a point, but that won’t make the ambient variable sets disappear. Alternatively, the whole universe will specialize, but at the same time be reborn. For an exposition of Joyal’s argument in print, see either [2] or [5] p. 805-807.

This process of collapsing to a ground model set we call settling down. Our purpose is to show how this settling semantics works in an arbitrary topological space, not just ℝ. This extension is not completely straightforward. Certain uniformities of ℝ allowed for simplifications in the definition of forcing (⊩) and for proofs of stronger set-theoretic axioms, most notably Full Separation and Exponentiation. In the next section, we prove as much as we can making no assumptions on the topological space T being worked over; in the following section, natural and appropriately modest assumptions are made on T so that Separation and Exponentiation can be proven.

The greatest weakness in what can be proven in the general case is in the family of Power Set-like axioms. This is no surprise, as the semantics was developed for a purpose which necessitated the failure of Subset Collection (and hence of Power Set itself). That Exponentiation ended up holding is thanks to the particularities of ℝ, not to settling semantics. Rather, what does hold in general is a weakened version of all of these Power Set-like axioms. The reason that Power Set fails, like the non-existence of the set of Dedekind cuts above, is that any candidate for the power set of X might collapse to a ground model set, and so would then no longer contain any variable subset of X. However, that variable subset might itself collapse, and then would be in the classical power set of X. So while the subset in question, before the collapse, might not equal a member of the classical power set, it cannot be different from every such member. That is the form of Power Set which holds in the settling semantics:

Eventual Power Set: ∀X ∃C (∀Y ∈ C Y ⊆ X)∧(∀Y ⊆ X ¬∀Z ∈ C Y ≠ Z). Although we will not need them, there are comparable weakenings of Subset

Collection (or Fullness) and Exponentiation:

Eventual Fullness: ∀X, Y ∃C (∀Z ∈ C Z is a total relation from X to Y) ∧ (∀R if R is a total relation from X to Y then ¬∀Z ∈ C Z ⊈ R).

Eventual Exponentiation: ∀X, Y ∃C ∀F if F is a total function from X to Y then ¬∀Z ∈ C F ≠ Z.

Proposition 1.1 Eventual Power Set implies Eventual Fullness, which in turn implies Eventual Exponentiation.

2 The General Case

First we define the term structure of the topological model with settling, then truth in the model (the forcing semantics), and then we prove that the model satisfies some standard set-theoretic axioms.

Definition 2.1 For a topological space T, a term is a set of the form {⟨σ_{i}, J_{i}⟩ | i ∈ I} ∪ {⟨σ_{h}, r_{h}⟩ | h ∈ H}, where each σ is (inductively) a term, each J an open set, each r is a member of T, and H and I index sets.

The first part of each term is as usual. It suffices for the embedding x ↦ x̂ of the ground model into the topological model:

Definition 2.2 x̂ = {⟨ŷ, T ⟩ | y ∈ x}. Any term of the form x̂ is called a ground model term.

For ϕ a formula in the language of set theory with (set, not term) parameters x_{0}, x_{1}, ..., x_{n}, then ϕ̂ is the formula in the term language obtained from ϕ by replacing each x_{i} with x̂_{i}.

ˇ is the inverse of ˆ , for both sets/terms and formulas: ˆ τ̌ = τ, ˇ x̂ = x, ˆ ϕ̌ = ϕ, and ˇ ϕ̂ = ϕ.

The second part of the definition of a term plays a role only when we decide to have the term settle down and stop changing. This settling down in described as follows.

Definition 2.3 For a term σ and r ∈ T, σ^{r} is defined inductively on the terms as {⟨σ_{i}^{r}, T ⟩ | ⟨σ_{i}, J_{i}⟩ ∈ σ ∧ r ∈ J_{i}} ∪ {⟨σ_{h}^{r}, T ⟩ | ⟨σ_{h}, r⟩ ∈ σ}.

Note that σ^{r} is a ground model term. It bears observation that (σ^{r})^{s} = σ^{r}.

Definition 2.4 For ϕ = ϕ(σ_{0}, ..., σ_{i}) a formula with parameters σ_{0}, ..., σ_{i}, ϕ^{r} is ϕ(σ_{0}^{r}, ..., σ_{i}^{r}).

We define a forcing relation J ⊩ ϕ, with J an open subset of T and ϕ a formula.

Definition 2.5 J ⊩ ϕ is defined inductively on ϕ:

J ⊩ σ = τ iff for all ⟨σ_{i}, J_{i}⟩ ∈ σ J ∩ J_{i} ⊩ σ_{i} ∈ τ and vice versa, and for all r ∈ J σ^{r} = τ^{r}

J ⊩ σ ∈ τ iff for all r ∈ J there is a ⟨τ_{i}, J_{i}⟩ ∈ τ and J_{r} ⊆ J_{i} containing r such that J_{r} ⊩ σ = τ_{i}

J ⊩ ϕ ∧ ψ iff J ⊩ ϕ and J ⊩ ψ

J ⊩ ϕ ∨ ψ iff for all r ∈ J there is a J_{r} ⊆ J containing r such that J_{r} ⊩ ϕ or J_{r} ⊩ ψ

J ⊩ ϕ → ψ iff for all J′ ⊆ J if J′ ⊩ ϕ then J′ ⊩ ψ, and, for all r ∈ J, there is a J_{r} ⊆ J containing r such that, for all K ⊆ J_{r}, if K ⊩ ϕ^{r} then K ⊩ ψ^{r}

J ⊩ ∃x ϕ(x) iff for all r ∈ J there is a J_{r} ⊆ J containing r and a σ such that J_{r} ⊩ ϕ(σ)

J ⊩ ∀x ϕ(x) iff for all σ J ⊩ ϕ(σ), and for all r ∈ J there is a J_{r} ⊆ J containing r such that for all σ J_{r} ⊩ ϕ^{r}(σ).

(Notice that in the last clause, σ is not interpreted as σ^{r}.)

Lemma 2.6 ⊩ is sound for constructive logic.

Lemma 2.7 T forces the equality axioms, to wit:

1. ∀x x = x

2. ∀x, y x = y → y = x 3. ∀x, y, z x = y ∧ y = z → x = z

4. ∀x, y, z x = y ∧ x ∈ z → y ∈ z

5. ∀x, y, z x = y ∧ z ∈ x → z ∈ y.

proof:

1: It is trivial to show via a simultaneous induction that, for all J and σ, J ⊩ σ = σ, and, for all ⟨σ_{i}, J_{i}⟩ ∈ σ, J ∩ J_{i} ⊩ σ_{i} ∈ σ.

2: Trivial because the definition of J ⊩ σ =_{M} τ is itself symmetric.

3: For this and the subsequent parts, we need a lemma.

Lemma 2.8 If J′ ⊆ J ⊩ σ = τ then J′ ⊩ σ = τ, and similarly for ∈.

proof: By induction on σ and τ.

Returning to the main lemma, we show that if J ⊩ ρ = σ and J ⊩ σ = τ then J ⊩ ρ = τ, which suffices. This will be done by induction on terms for all opens J simultaneously.

For the second clause in J ⊩ ρ = τ, let r ∈ J. By the hypotheses, second clauses, ρ^{r} = σ^{r} and σ^{r} = τ^{r}, so ρ^{r} = τ^{r}.

The first clause of the definition of forcing equality follows by induction on terms. Starting with ⟨ρ_{i}, J_{i}⟩ ∈ ρ, we need to show that J ∩ J_{i} ⊩ ρ_{i} ∈ τ. We have J ∩ J_{i} ⊩ ρ_{i} ∈ σ. For a fixed, arbitrary r ∈ J ∩ J_{i} let ⟨σ_{j}, J_{j}⟩ ∈ σ and J′ ⊆ J ∩ J_{i} be such that r ∈ J′ ∩ J_{j} ⊩ ρ_{i} = σ_{j}. By hypothesis, J ∩ J_{j} ⊩ σ_{j} ∈ τ. So let ⟨τ_{k}, J_{k}⟩ ∈ τ and Ĵ ⊆ J ∩ J_{j} be such that r ∈ Ĵ ∩ J_{k} ⊩ σ_{j} = τ_{k}. Let J̃ be J′ ∩ Ĵ ∩ J_{j}. Note that J̃ ⊆ J ∩ J_{i}, and that r ∈ J̃ ∩ J_{k}. We want to show that J̃ ∩ J_{k} ⊩ ρ_{i} = τ_{k}. Observing that J̃ ∩ J_{k} ⊆ J′ ∩ J_{j}, Ĵ ∩ J_{k}, it follows by the previous lemma that J̃ ∩ J_{k} ⊩ ρ_{i} = σ_{j}, σ_{j} =_{M} τ_{k}, from which the desired conclusion follows by the induction. So r ∈ J̃ ∩ J_{k} ⊩ ρ_{i} ∈ τ. Since r ∈ J ∩ J_{i} was arbitrary, J ∩ J_{i} ⊩ ρ_{i} ∈ τ.

4: It suffices to show that if J ⊩ ρ = σ and J ⊩ ρ ∈ τ then J ⊩ σ ∈ τ. Let r ∈ J. By hypothesis, let ⟨τ_{i}, J_{i}⟩ ∈ τ, J_{r} ⊆ J_{i} be such that r ∈ J_{r} ⊩ ρ = τ_{i}; without loss of generality J_{r} ⊆ J. By the previous lemma, J_{r} ⊩ ρ = σ, and by the previous part of the current lemma, J_{r} ⊩ σ = τ_{i}. Hence J_{r} ⊩ σ ∈ τ. Since r ∈ J was arbitrary, we are done.

5: Similar, and left to the reader.

Lemma 2.9 1. For all ϕ ∅ ⊩ ϕ.

2. If J′ ⊆ J ⊩ ϕ then J′ ⊩ ϕ.

3. If J_{i} ⊩ ϕ for all i then ⋃_{i} J_{i} ⊩ ϕ.

4. J ⊩ ϕ iff for all r ∈ J there is a J_{r} ⊆ J containing r such that J_{r} ⊩ ϕ.

5. For all ϕ, J if J ⊩ ϕ then for all r ∈ J there is a neighborhood J_{r} of r such that J_{r} ⊩ ϕ^{r}.

6. For ϕ bounded (i.e. Δ_{0}) and having only ground model terms as parameters, T ⊩ ϕ iff ϕ̌ (i.e. V ⊧ ϕ̌).

proof:

1. Trivial induction. This part is not used later, and is mentioned here only to flesh out the picture.

2. Again, a trivial induction. The base cases, = and ∈, are proven by induction on terms, as mentioned just above.

3. By induction. For the case of →, you need to invoke the previous part of this lemma. All other cases are straightforward.

4. Trivial, using 3.

5. By induction on ϕ.

=: If r ∈ J ⊩ σ = τ then σ^{r} = τ^{r}. By the proof of the first part of the equality lemma, T ⊩ σ^{r} = τ^{r}.

∈: If r ∈ J ⊩ σ ∈ τ, let τ_{i}, J_{i}, and J_{r} be as given by the definition of forcing ∈. Inductively, some neighborhood of r (or, by the previous case, T itself) forces σ^{r} = τ_{i}^{r}. Since ⟨τ_{i}^{r}, T ⟩ ∈ τ^{r}, T ⊩ τ_{i}^{r} ∈ τ^{r}, and T ⊩ σ^{r} ∈ τ^{r}.

∨: If r ∈ J ⊩ ϕ ∨ ψ, suppose without loss of generality that r ∈ J_{r} ⊩ ϕ. Inductively let K_{r} be a neighborhood of r forcing ϕ^{r}. Then K_{r} ⊩ ϕ^{r} ∨ ψ^{r}.

∧: If r ∈ J ⊩ ϕ ∧ ψ, let J_{r} and K_{r} be neighborhoods of r such that J_{r} ⊩ ϕ and K_{r} ⊩ ψ. Then J_{r} ∩ K_{r} is as desired.

→: If r ∈ J ⊩ ϕ → ψ, then J_{r} as given in the definition of forcing → suffices. (To verify the second clause in the definition of J_{r} ⊩ ϕ^{r} → ψ^{r}, use the fact that (ϕ^{r})^{s} = ϕ and (ψ^{r})^{s} = ψ.)

∃: If r ∈ J ⊩ ∃x ϕ(x), let J_{r} ⊆ J and σ be such that r ∈ J_{r} ⊩ ϕ(σ). By induction, let K_{r} be such that r ∈ K_{r} ⊩ ϕ^{r}(σ^{r}). So K_{r} ⊩ ∃x ϕ^{r}(x).

∀: If r ∈ J ⊩ ∀x ϕ(x), then J_{r} as given by the definition of forcing ∀ suffices.

6. A simple induction.

At this point, we are ready to show what is in general forced under this semantics.

Theorem 2.10 T forces:

Infinity

Pairing

Union

Extensionality

Set Induction

Eventual Power Set Bounded (Δ_{0}) Separation

Collection

Some comments on this choice of axioms are in order. The first five are unremarkable. The role of Eventual Power Set was discussed in the Introduction. The restriction of Separation to the Δ_{0} case should be familiar, as that is also the case in CZF and KP. By way of compensation, the version of Collection in CZF is Strong Collection: not only does every total relation with domain a set have a bounding set (regular Collection), but that bounding set can be chosen so that it contains only elements related to something in the domain (the strong version). In the presence of full Separation, these are equivalent, as an appropriate subset of any bounding set can always be taken. Unfortunately, even the additional hypotheses provided by Collection are not enough in the current context to yield even this modest fragment of Separation, as will actually be shown at the beginning of the next section. In fact, even Replacement fails, as we will see.

proof:

• Infinity: ω̂ will do. (Recall that the canonical name x̂ of any set x from the ground model is defined inductively as {⟨ŷ, T ⟩ | y ∈ x}.)

• Pairing: Given σ and τ, {⟨σ, T ⟩, ⟨τ, T ⟩} will do.

• Union: Given σ, the union of the following four terms will do:

– {⟨τ, J ∩ J_{i}⟩ | for some σ_{i}, ⟨τ, J⟩ ∈ σ_{i} and ⟨σ_{i}, J_{i}⟩ ∈ σ}

– {⟨τ, r⟩ | for some σ_{i}, ⟨τ, r⟩ ∈ σ_{i} and ⟨σ_{i}, r⟩ ∈ σ}

– {⟨τ, r⟩ | for some σ_{i} and K, ⟨τ, K⟩ ∈ σ_{i}, r ∈ K, and ⟨σ_{i}, r⟩ ∈ σ} – {⟨τ, r⟩ | for some σ_{i} and K, ⟨τ, r⟩ ∈ σ_{i}, r ∈ K, and ⟨σ_{i}, K⟩ ∈ σ}.

• Extensionality: We need to show that T ⊩ ∀x ∀y [∀z (z ∈ x ↔ z ∈ y) → x = y]. It suffices to show that for any terms σ and τ, T ⊩ ∀z (z ∈ σ ↔ z ∈ τ) → σ = τ. (Although that is only the first clause in forcing ∀, it subsumes the second, because σ and τ could have been chosen as ground model terms in the first place.) To show that, for the second clause in forcing →, it suffices to show that T ⊩ ∀z (z ∈ σ^{r} ↔ z ∈ τ^{r}) → σ^{r} = τ^{r}. But, as before, this is already subsumed by choosing σ and τ to be ground model terms in the first place. Hence it suffices to check the first clause in forcing →: for all J, if J ⊩ ∀z (z ∈ σ ↔ z ∈ τ), then J ⊩ σ = τ.

To this end, let ⟨σ_{i}, J_{i}⟩ be in σ; we need to show that J ∩ J_{i} ⊩ σ_{i} ∈ τ. By the choice of J, J ⊩ σ_{i} ∈ σ ↔ σ_{i} ∈ τ. In particular, J ⊩ σ_{i} ∈ σ → σ_{i} ∈ τ. By 2.9, part 2), J ∩ J_{i} ⊩ σ_{i} ∈ σ → σ_{i} ∈ τ. Since J ∩ J_{i} ⊩ σ_{i} ∈ σ (proof of 2.7, part 1)), J ∩ J_{i} ⊩ σ_{i} ∈ τ. Symmetrically for ⟨τ_{i}, J_{i}⟩ ∈ τ.

Also, let r ∈ J. If σ^{r} ≠ τ^{r}, let ⟨ρ, T ⟩ be in their symmetric difference. By the choice of J, for some neighborhood J_{r} of r, J_{r} ⊩ ρ ∈ σ^{r} ↔ ρ ∈ τ^{r}. This contradicts the choice of ρ. So σ^{r} = τ^{r}.

• Set Induction (Schema): We need to show that T ⊩ ∀x ((∀y ∈ x ϕ(y)) → ϕ(x)) → ∀x ϕ(x). The statement in question is an implication. The definition of forcing → contains two clauses.

The first clause is that, for any open set J and formula ϕ, if J ⊩ ∀x(∀y ∈ x ϕ(y) → ϕ(x)) then J ⊩ ∀x ϕ(x). By way of proving that, suppose not. Let J and ϕ provide a counter-example. By hypothesis,

∀σ J ⊩ ∀y ∈ σ ϕ(y) → ϕ(σ)  (1)

and

∀r ∈ J ∃J′ ∋ r ∀σ′ J′ ⊩ ∀y ∈ σ′ ϕ^{r}(y) → ϕ^{r}(σ′).  (2)

Since J ⊮ ∀xϕ(x), either

∃σ J ⊮ ϕ(σ)  (3)

or

∃r ∈ J ∀J′ ∋ r ∃σ′ J′ ⊮ ϕ^{r}(σ′).  (4)

If (4) holds, let r as given by (4), and then let J′ be as given by (2) for that r. By (4), ∃σ′ J′ ⊮ ϕ^{r}(σ′); let σ be such a σ′ – so J′ ⊮ ϕ^{r}(σ) – of minimal V-rank. By (2), we have J′ ⊩ ∀y ∈ σ ϕ^{r}(y) → ϕ^{r}(σ). If we can show that J′ ⊩ ∀y ∈ σ ϕ^{r}(y), then (by the definition of forcing →) we will have a contradiction, showing that (4) must fail.

To that end, we must show, unpacking the abbreviation, that J′ ⊩ ∀y(y ∈ σ → ϕ^{r}(y)); that is,

∀τ J′ ⊩ τ ∈ σ → ϕ^{r}(τ)  (5)

and

∀s ∈ J′ ∃K ∋ s ∀τ K ⊩ τ ∈ σ^{s} → ϕ^{r}(τ),  (6)

the latter because (ϕ^{r})^{s} = ϕ^{r}.

By way of showing (5), suppose J′ ⊇ K ⊩ τ ∈ σ. Then K can be covered with open sets K_{i} such that K_{i} ⊩ τ = σ_{i} and K_{i} ⊆ J_{i} where ⟨σ_{i}, J_{i}⟩ ∈ σ. Since σ_{i} has strictly lower V-rank than σ, J′ ⊩ ϕ^{r}(σ_{i}). Hence K_{i} ⊩ ϕ^{r}(τ). Since the K_{i}s cover K (by lemma 2.9, part 3)) K forces the same. We still have to show that for all s ∈ J′ there is a K ∋ s such that for all K′ ⊆ K if K′ ⊩ τ^{s} ∈ σ^{s} then K′ ⊩ ϕ^{r}(τ^{s}). In fact, J′ suffices for K: if J′ ⊇ K′ ⊩ τ^{s} ∈ σ^{s} then K′ ⊩ ϕ^{r}(τ^{s}). Moreover, this is the same argument as the one just completed, with σ^{s} in place of σ. The only minor observation that bears making is that the V-rank of σ^{s} is less than or equal to that of σ, so again when τ is forced to be a member of σ^{s} its V-rank is strictly less than that of σ, so the choice of σ carries us through.

To show (6), we claim that J′ suffices for the choice of K: J′ ⊩ τ ∈ σ^{s} → ϕ^{r}(τ). Once more, this is just (5), with σ^{s} in place of σ.

This completes the proof that (4) must fail. Hence we have that the negation of (4) must hold, namely

∀r ∈ J ∃J′ ∋ r ∀σ′ J′ ⊩ ϕ^{r}(σ′),  (7)

as well as (3). Let σ be of minimal V-rank such that J ⊮ ϕ(σ). If we can show that J ⊩ ∀y ∈ σ ϕ(y), then by (1) we will have a contradiction, completing the proof of the first clause.

What we need to show are

∀τ J ⊩ τ ∈ σ → ϕ(τ)  (8)

and

∀r ∈ J ∃J′ ∋ r ∀τ J′ ⊩ τ ∈ σ^{r} → ϕ^{r}(τ).  (9)

By way of showing (8), suppose J ⊇ K ⊩ τ ∈ σ; we need to show that K ⊩ ϕ(τ). This is the same argument, based on the minimality of σ, as in the proof of (5). The other part of showing (8) is

∀r ∈ J ∃J′ ∋ r ∀K ⊆ J′ (K ⊩ τ^{r} ∈ σ^{r} ⇒ K ⊩ ϕ^{r}(τ^{r})).  (10)

Both (9) and (10) are special cases of (7).

This completes the proof of the first clause.

The second clause is that for all r ∈ T there is a J ∋ r such that for all K ⊆ J if K ⊩ ∀x ((∀y ∈ x ϕ^{r}(y)) → ϕ^{r}(x)) then K ⊩ ∀x ϕ^{r}(x). For any r, let J be T. Then what remains of the claim has exactly the same form as the first clause, with K and ϕ^{r} for J and ϕ respectively. Since the validity of this first clause was already shown for all choices of J and ϕ, we are done.

• Eventual Power Set: We need to show that T ⊩ ∀X ∃C ∀Y (Y ⊆ X → ¬∀Z(Z ∈ C → Y ≠ Z)). (Actually, we must also produce a C that contains only subsets of X. However, to extract such a sub-collection from any C as above is an instance of Bounded Separation, the proof of which below does not rely on the current proof. So we will make our lives a little easier and prove the version of EPS as stated.) Since the sentence forced has no parameters, the second clause in forcing ∀ is subsumed by the first, so all we must show is that, for any term σ, T ⊩ ∃C ∀Y (Y ⊆ σ → ¬∀Z(Z ∈ C → Y ≠ Z)).

Let τ = {⟨x̂, r⟩ | σ^{r} = ŝ ∧ x ⊆ s}. This is the desired C. It suffices to show that T ⊩ ∀Y (Y ⊆ σ → ¬∀Z(Z ∈ τ → Y ≠ Z)).

For the first clause in forcing ∀, we need to show that T ⊩ ρ ⊆ σ → ¬∀Z(Z ∈ τ → ρ ≠ Z). To do that, first suppose T ⊇ J ⊩ ρ ⊆ σ. (Note that that implies that for all s ∈ J T ⊩ ρ^{s} ⊆ σ^{s}, so that ⟨ρ^{s}, s⟩ ∈ τ, and T ⊩ ρ^{s} ∈ τ^{s}.) We must show that J ⊩ ¬∀Z(Z ∈ τ → ρ ≠ Z). It suffices to show that no non-empty subset K of J forces ∀Z(Z ∈ τ → ρ ≠ Z) or ∀Z(Z ∈ τ^{r} → ρ^{r} ≠ Z) (r ∈ J). For the former, we will show that K must violate the second clause in forcing ∀. Let s ∈ K. Letting Z be ρ^{s}, as just observed, all of T will force Z ∈ τ^{s} but nothing will force ρ^{s} ≠ Z. Similarly for the latter, by choosing Z to be ρ^{r}. To finish forcing the implication, it suffices to show that for all r T ⊩ ρ^{r} ⊆ σ^{r} → ¬∀Z(Z ∈ τ^{r} → ρ^{r} ≠ Z). Again, it suffices to let Z be ρ^{r}. For the second clause in forcing ∀, for r ∈ T and ρ a term, it suffices to show that T ⊩ ρ ⊆ σ^{r} → ¬∀Z(Z ∈ τ^{r} → ρ ≠ Z). This time letting Z by any ρ^{s} suffices.

• Bounded Separation: The important point here is that, for ϕ bounded (Δ_{0}) with only ground model terms, J ⊩ ϕ iff T ⊩ ϕ iff V ⊧ ϕ̌ (2.9, part 6). We need to show that T ⊩ ∀X ∃Y ∀Z (Z ∈ Y ↔ Z ∈ X ∧ ϕ(Z)). This means, first, that for any σ, T ⊩ ∃Y ∀Z (Z ∈ Y ↔ Z ∈ σ ∧ ϕ(Z)), and, second, for any r ∈ T there is a J ∋ r such that, for any σ, J ⊩ ∃Y ∀Z (Z ∈ Y ↔ Z ∈ σ ∧ϕ^{r}(Z)). In the second part, choosing J to be T, we have an instance of the first part, so it suffices to prove the first only. Let τ be {⟨σ_{i}, J∩J_{i}⟩ | ⟨σ_{i}, J_{i}⟩ ∈ σ and J ⊩ ϕ(σ_{i})}∪{⟨x̂, r⟩ | ⟨x̂, T ⟩ ∈ σ^{r} and T ⊩ ϕ^{r}(x̂)}. We claim that τ suffices: T ⊩ ∀Z (Z ∈ τ ↔ Z ∈ σ ∧ ϕ(Z)). First, let ρ be a term. We need to show that T ⊩ ρ ∈ τ ↔ ρ ∈ σ ∧ ϕ(ρ). Unraveling the bi-implication and the definition of forcing an implication, that becomes J ⊩ ρ ∈ τ iff J ⊩ ρ ∈ σ ∧ ϕ(ρ), and J ⊩ ρ^{r} ∈ τ^{r} iff J ⊩ ρ^{r} ∈ σ^{r} ∧ ϕ^{r}(ρ^{r}). The first iff should be clear from the first part of the definition of τ and the second iff from the second part of the definition, along with the observation that forcing ϕ^{r}(ρ^{r}) is independent of J. We also need, for each r ∈ T, a J ∋ r such that for all ρ J ⊩ ρ ∈ τ^{r} ↔ ρ ∈ σ^{r} ∧ ϕ^{r}(ρ). Choosing J to be T and unraveling as above (recycling the variable J) yields J ⊩ ρ ∈ τ^{r} iff J ⊩ ρ ∈ σ^{r} ∧ ϕ^{r}(ρ), and J ⊩ ρ^{s} ∈ τ^{r} iff J ⊩ ρ^{s} ∈ σ^{r} ∧ ϕ^{r}(ρ^{s}). These hold because the only things that can be forced to be in τ^{r} or σ^{r} are (locally) images of ground model terms, and the truth of ϕ^{r} evaluated at such a term is independent of J.

• Collection: Since only regular, not strong, Collection is true here, it would be easiest to his this with a sledgehammer: reflect V to some set M large enough to contain all the parameters and capture the truth of the assertion in question; the term consisting of the whole universe according to M will be more than enough. It is more informative, though, to follow through the natural construction of a bounding set, so we can highlight in the next section just what goes wrong with the proof of Strong Collection. We need T ⊩ ∀x ∈ σ ∃y ϕ(x, y) → ∃z ∀x ∈ σ ∃y ∈ z ϕ(x, y). It suffices to show that for any J if J ⊩ ∀x ∈ σ ∃y ϕ(x, y) then J ⊩ ∃z ∀x ∈ σ ∃y ∈ z ϕ(x, y), and the same relativized to r. The latter is a special case of the former, so it suffices to show just the former. By hypothesis, for each ⟨σ_{i}, J_{i}⟩ ∈ σ and r ∈ J_{i} ∩ J there are τ_{ir} and J_{ir} ⊆ J_{i} ∩ J, J_{ir} ∋ r such that J_{ir} ⊩ ϕ(σ_{i}, τ_{ir}). Also, for all r ∈ J there is a J_{r} ∋ r such that, for all ⟨x̂, T ⟩ ∈ σ^{r}, J_{r} ⊩ ∃y ϕ^{r}(x̂, y). For each s ∈ J_{r}, let τ_{rx̂s} and K ∋ s be such that K ⊩ ϕ^{r}(x̂, τ_{rx̂s}). By 2.9, part 5), K ⊩ ϕ^{r}(x̂, τ_{rx̂s}^{s}).

We claim that τ = {⟨τ_{ir}, J_{ir}⟩ | i ∈ I, r ∈ J_{i}∩J}∪{⟨τ_{rx̂s}^{s}, r⟩ | r ∈ J, ⟨x̂, T ⟩ ∈ σ^{r}, s ∈ J_{r}} suffices: J ⊩ ∀x ∈ σ ∃y ∈ τ ϕ(x, y).

Forcing a universal has two parts. The first is that for all ρ, J ⊩ ρ ∈ σ → ∃y ∈ τ ϕ(ρ, y). For the second, it suffices to show that for all r ∈ J and terms ρ J_{r} ⊩ ρ ∈ σ^{r} → ∃y ∈ τ^{r} ϕ^{r}(ρ, y).

For the former, first suppose J ⊇ K ⊩ ρ ∈ σ. It should be clear that the first part of τ covers this case. For the other part of forcing that implication, for each r ∈ J, it suffices to show that J_{r} is as desired: for all K ⊆ J_{r}, if K ⊩ ρ^{r} ∈ σ^{r} then K ⊩ ∃y ∈ τ^{r} ϕ^{r}(ρ^{r}, y). This is subsumed by the second implication from above, to which we now turn.

To show J_{r} ⊩ ρ ∈ σ^{r} → ∃y ∈ τ^{r} ϕ^{r}(ρ, y), we need to show first that if J_{r} ⊇ K ⊩ ρ ∈ σ^{r} then K ⊩ ∃y ∈ τ^{r} ϕ^{r}(ρ, y), and second that for all s ∈ J_{r} there is a K ∋ s such that if K ⊃ L ⊩ ρ^{s} ∈ σ^{r} then L ⊩ ∃y ∈ τ^{r} ϕ^{r}(ρ^{s}, y). By choosing K to be J_{r}, the second is subsumed by the first. For that, it should be clear that the second part of τ covers this case. In a bit more detail, it suffices to work locally. (That is, it suffices to find a neighborhood of s ∈ K forcing what we want, by 2.9.) Locally, ρ is forced equal to some x̂, where ⟨x̂, T ⟩ ∈ σ^{r}. As already shown, some neighborhood of s forces ϕ^{r}(x̂, τ_{rx̂s}^{s}), and ⟨τ_{rx̂s}^{s}, T ⟩ ∈ τ^{r} by the second part of τ.

3 Separation and Exponentiation

If Separation were to hold (in the presence of the other axioms from above), then Strong Collection would follow, which itself implies Replacement. Hence a powerful way to show that Separation is not forced is to give an example in which even Replacement fails. In the example below, the offending formula is a Boolean combination of Σ_{1} formulas; we do not know if simpler instances of Replacement, such as for Σ_{1} or Δ_{0} formulas, are falsifiable or instead are actually forced.

Let T_{n} (n > 0) be the standard space for collapsing ℵ_{n} to be countable: elements are injections from ℵ_{0} to ℵ_{n}, and an open set is given by a finite partial function of the same type. Let T be the disjoint union of the T_{n}s adjoined with an extra element ∞: ⨄_{n} T_{n} ∪ {∞}. A basis for the topology is given by all the open subsets of each T_{n}, plus the basic open neighborhoods of ∞, which are all of the form ⨄_{n≥N} T_{n} ∪ {∞} for some fixed N.

This T falsifies Replacement. To state the instance claimed to be falsified, we need two parameters. One is {⟨n̂, ∞⟩ | n ∈ ω}, which we will call ω^{−}, and the other the internalization of the function n ↦ ℵ_{n} (n ∈ ω), which we will refer to via the free use of the notation ℵ̂_{n}, even when n is just a variable.

Proposition 3.1 T ⊮ ∀x ∈ ω^{−} ∃!y [(y = 0 ∨ y = 1) ∧ (y = 0 ↔ ℵ̂_{x} is uncountable)∧(y = 1 ↔ ¬¬ℵ̂_{x} is countable)] → ∃f ∀x ∈ ω^{−}[(f(x) = 0∨f(x) = 1) ∧ (f(x) = 0 ↔ ℵ̂_{x} is uncountable) ∧ (f(x) = 1 ↔ ¬¬ℵ̂_{x} is countable)].

proof: First we show that T forces the antecedent ∀x[x ∈ ω^{−} → ∃!y [(y = 0 ∨ y = 1) ∧ (y = 0 ↔ ℵ̂_{x} is uncountable) ∧ (y = 1 ↔ ¬¬ℵ̂_{x} is countable)]].

For the first clause in forcing ∀, we need to show that for all σ T ⊩ σ ∈ ω^{−} → ∃!y [(y = 0 ∨ y = 1) ∧ (y = 0 ↔ ℵ̂_{σ} is uncountable) ∧ (y = 1 ↔ ¬¬ℵ̂_{σ} is countable)]. The first clause in forcing that implication is vacuous, as no open set will force σ ∈ ω^{−}. The second clause is vacuous for all choices of r except ∞, as then (ω^{−})^{r} is empty. Finally, for r = ∞, it suffices to show that T ⊩ ∃!y [(y = 0 ∨ y = 1) ∧ (y = 0 ↔ ℵ̂n̂ is uncountable) ∧ (y = 1 ↔ ¬¬ℵ̂n̂ is countable)]. The term which is 0 on ⨄_{0<i<n} T_{n} and 1 on the rest of T suffices.

The second clause in forcing ∀ is similar.

Since T forces the antecedent of the conditional, it suffices to show that T does not force the consequent: T ⊮ ∃f ∀x ∈ ω^{−}[(f(x) = 0 ∨ f(x) = 1) ∧ (f(x) = 0 ↔ ℵ̂_{x} is uncountable) ∧ (f(x) = 1 ↔ ¬¬ℵ̂_{x} is countable)]. If that were not the case, there would be a term (we will ambiguously refer to as f) and a neighborhood J of ∞ such that J ⊩ ∀x ∈ ω^{−}[(f(x) = 0 ∨ f(x) = 1) ∧ (f(x) = 0 ↔ ℵ̂_{x} is uncountable) ∧ (f(x) = 1 ↔ ¬¬ℵ̂_{x} is countable)]. By 2.9, part 5), there would be a K ∋ ∞ such that K ⊩ ∀x ∈ ω[(f^{∞}(x) = 0∨f^{∞}(x) = 1)∧(f^{∞}(x) = 0 ↔ ℵ̂_{x} is uncountable) ∧ (f^{∞}(x) = 1 ↔ ¬¬ℵ̂_{x} is countable)]. K, being open, contains a set of the form ⨄_{n≥N} T_{n}. Let M be N + 1. So K ⊩ (f^{∞}(M̂) = 0 ∨ f^{∞}(M̂) = 1) ∧ (f^{∞}(M̂) = 0 ↔ ℵ̂M̂ is uncountable) ∧ (f^{∞}(M̂) = 1 ↔ ¬¬ℵ̂M̂ is countable). But f^{∞}(M̂) is a ground model term, and so is (forced by K to be) equal to ˆ0 or ˆ1. Hence either K ⊩ ℵ̂M̂ is uncountable or K ⊩ ¬¬ℵ̂M̂ is countable. But neither is the case, since K ⊇ T_{N} ⊩ ℵ̂M̂ is uncountable and K ⊇ ⨄_{n>N} T_{n} ⊩ ℵ̂M̂ is countable.

In the example above, the problem around ∞ is that no neighborhood forces just what gets collapsed and what doesn’t. It is this lack of homogeneity that is the root cause of the failure of Separation.

Definition 3.2 T is locally homogeneous around r, s ∈ T if there are neighborhoods J_{r}, J_{s} of r and s respectively and a homeomorphism of J_{r} to J_{s} sending r to s.

An open set U is homogeneous if it is locally homogeneous around all r, s ∈ U. T is locally homogeneous if every r ∈ T has a homogeneous neighborhood.

Lemma 3.3 If U is homogeneous, ϕ contains only ground model terms, and U ⊇ V ⊩ ϕ (V non-empty), then U ⊩ ϕ.

proof: Let r ∈ V. For s ∈ U, let V_{r} and V_{s} be the neighborhoods f the homeomorphism given by the homogeneity of U. f(σ) can be defined inductively on terms σ. (Briefly, hereditarily restrict σ to V_{r} and apply f to the second parts of the pairs in the terms.) f(ψ) is then ψ with f applied to the parameters. It is easy to show inductively on formulas that V_{r} ⊩ ψ iff V_{s} ⊩ f(ψ).

If ϕ contains only ground model terms, then f(ϕ) = ϕ. So U is covered by open sets that force ϕ. Hence U ⊩ ϕ.

Theorem 3.4 If T is locally homogeneous then T ⊩ F ullSeparation.

proof: As in the proof of Bounded Separation from the previous section, we have to show that, for any σ, T ⊩ ∃Y ∀Z (Z ∈ Y ↔ Z ∈ σ ∧ ϕ(Z)), only this time with no restriction on ϕ. The choice of witness Y is slightly different. For each r let K_{r} ∋ r be homogeneous. Let τ be {⟨σ_{i}, J ∩ J_{i}⟩ | ⟨σ_{i}, J_{i}⟩ ∈ σ and J ⊩ ϕ(σ_{i})} ∪ {⟨x̂, r⟩ | ⟨x̂, T ⟩ ∈ σ^{r} and K_{r} ⊩ ϕ^{r}(x̂)}. The difference from before is that in the latter part of τ membership is determined by what’s forced by K_{r} instead of by T. We claim that τ suffices: T ⊩ ∀Z (Z ∈ τ ↔ Z ∈ σ ∧ ϕ(Z)).

For the first clause in forcing ∀, let ρ be a term. We need to show T ⊩ ρ ∈ τ ↔ ρ ∈ σ ∧ ϕ(ρ). By the first clause in forcing →, we have to show that for all J J ⊩ ρ ∈ τ iff J ⊩ ρ ∈ σ ∧ ϕ(ρ), which should be clear from the first part of τ. For the second clause in → it suffices to show that for all J ⊆ K_{r} J ⊩ ρ^{r} ∈ τ^{r} iff J ⊩ ρ^{r} ∈ σ^{r} ∧ ϕ^{r}(ρ^{r}). Regarding forcing membership, all of the terms here are ground model terms, so membership is absolute (does not depends on the choice of J). If ρ^{r} enters τ^{r} because of the first part of τ’s definition, then we have σ_{i}^{r} = ρ^{r}, r ∈ J ⊩ ϕ(σ_{i}), r ∈ J_{i}, and ⟨σ_{i}, J_{i}⟩ ∈ σ. By 2.9, part 5), some neighborhood J_{r} of r forces ϕ^{r}(σ_{i}^{r}). By the lemma just above (applied to K_{r} ∩ J_{r}), K_{r} forces the same. Hence we can restrict our attention to terms ρ^{r} which enter τ because of τ’s definition’s second part. Again by the preceding lemma, for J non-empty, J ⊩ ϕ^{r}(ρ^{r}) iff K_{r} ⊩ ϕ^{r}(ρ^{r}), which suffices. (For J empty, J forces everything.)

For the second clause in forcing ∀, it suffices to show that K_{r} ⊩ ρ ∈ τ^{r} ↔ ρ ∈ σ^{r} ∧ ϕ^{r}(ρ). If any J ⊆ K_{r} forces ρ ∈ τ^{r} or ρ ∈ σ^{r}, then locally ρ is forced to be some ground model term, and we’re in the same situation as in the previous paragraph.

It would be nice to turn the previous theorem into an iff. If that is false, it would be interesting to see exactly what condition is equivalent to Full Separation. Presumably it would have something to do with homogeneity, since the proof given seems so natural, but it’s possible that the correct condition, if weaker than local homogeneity, would involve different issues. It’s also possible that Separation has no natural correspondent on the topological side, which would be very unfortunate, but still important to know.

We now turn our attention to Exponentiation.

Theorem 3.5 If T is locally connected, then T ⊩ Exponentiation. proof: Given terms σ and χ, let τ be {⟨ρ, J⟩ | J ⊩ ρ is a function from σ to χ} ∪ {⟨x̂, r⟩ | x is a function from σ̌^{r} to χ̌^{r}}. (τ can be arranged to be set-sized by requiring that ρ be hereditarily empty outside of J.) It suffices to show that T ⊩ ∀z (z ∈ τ ↔ z is a function from σ to χ).

The first clause in forcing ∀ is that, for any term ρ, T ⊩ ρ ∈ τ ↔ ρ is a function from σ to χ. That J ⊩ ρ ∈ τ iff J ⊩ “ρ is a function from σ to χ” is immediate from the first part of τ. As for J ⊩ ρ^{r} ∈ τ^{r} iff J ⊩ “ρ^{r} is a function from σ^{r} to χ^{r}”, by 2.9, part 6), both of those statements are independent of J, and the iff holds because of the second part of τ.

The crux of the matter is the second clause in forcing ∀: J ⊩ ρ ∈ τ^{r} iff J ⊩ “ρ is a function from σ^{r} to χ^{r}”. Why can only ground model functions be forced (locally) to be functions? For s ∈ J, let K_{s} ⊆ J be a connected neighborhood of s. For each ⟨σ_{i}, T ⟩ ∈ σ^{r}, pick a ⟨χ_{i}, T ⟩ ∈ χ such that the value of (i.e. the largest subset of K_{s} forcing) “ρ(σ_{i}) = χ_{i}” is non-empty. That set, along with the value of “ρ(σ_{i}) ≠ χ_{i}”, is a disjoint open cover of K_{s}. Since K_{s} is connected, the latter set is empty. So all of the values of ρ are determined by K_{s}, so K_{s} forces ρ to equal a ground model term. Since J is covered by such sets, J also forces ρ to be a ground model term.

Again, it would be nice to turn this into an iff, or, failing that, to know what topological equivalent there is to Exponentiation.

An application of these theorems can be found in [3]. The second model presented there is the topological semantics of the current paper applied to ℝ (with the standard topology). ℝ is homogeneous (not just locally so) and locally connected, which is why that model satisfied Separation and Exponentiation. An example where Exponentiation fails is if T is Cantor space. Forcing with T produces a random 0-1 sequence, which is a function from ℕ to 2. So the canonical generic is in a function space, but cannot be captured by any ground model set.

References

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

[2] R.J. Grayson, Heyting-valued semantics, in G. Lolli, G. Longo, and Am Marcja (eds.), Logic Colloquium ’82, Studies in Logic and the Foundations of Mathematics Vol. 112 (North-Holland, Amsterdam New York Oxford, 1984), p. 181-208

[3] R. Lubarsky and M. Rathjen, On the constructive Dedekind reals, in Sergei N. Artemov and Anil Nerode (eds.), Proceedings of LFCS ’07, Lecture Notes in Computer Science Vol. 4514 (Springer, 2007), pp. 349-362; also to appear in Logic and Analysis (Springer), currently available online, ISSN 1863-3625

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

[5] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics – An Introduction, Vol. II, Studies in Logic and the Foundations of Mathematics Vol. 123 (North-Holland, Amsterdam New York Oxford, 1988)