Tychonov’s Theorem in Abstract Stone Duality

Paul Taylor

24 September 2006

Abstract New constructive definition of compactness in the form of the existence of a continuous ”universal quantifier”. Construction and compactness of Cantor space. Baire space is not definable (locally compact). Examination of the (non-) impact of a counterexample due to Kleene that has previously undermined other attempts to define and prove compactness of Cantor space constructively.

1 Introduction

These notes concern Cantor space (i.e. an object that enjoys the universal property of the exponential 2^{ℕ}) in ASD, rather than Tychonov’s theorem in any generality. They were written in May–August 2004 as part of a disagreement with Martín Escardó related to his paper Synthetic Topology. Some of my slightly facetious language in Section 6 below must be understood in the context of his paper and our disagreement.

The central intellectual question is whether Cantor space and the closed real interval are compact (in the “finite open cover” sense) in various alternative accounts of topology. The point is that they are not in certain traditional models in which these spaces are defined as sets of recursively definable points.

A brief survey of these models and their (in my opinion, pathological) properties appears in [I, Section 12]. As is usual in mathematical discourse, such a survey provides an introduction to this issues, but falsifies the history, as it was the conclusion to the debate. It also treats the closed real interval, whereas these notes are about Cantor space.

The disagreement with Escardó over the compactness of Cantor space is intellectually important because it clearly distinguishes ASD from his Synthetic Topology. The principal similarities between them are that

• the topology on X is treated as the exponential Σ^{X};

• compactness of X is characterised by the existence of a “universal quantifier” ∀_{X} : Σ^{X} → Σ; and

• the associated λ- and predicate calculi are subsequently used to develop topological arguments in a logical style.

The crucial differences are that • Escardó’s arguments provide a “shorthand” which must be interpreted in traditional models of topology that are fundamentally based on sets (or types, or objects of a topos); in particular his ∀ means “for every point” and exists for all spaces, compact spaces being those for which this set-theoretic operation is Scott-continuous; and his “subspaces” are subsets of points; whereas

• ASD is an autonomous calculus (a “type theory”, though not in the sense of Martin-Löf), which provides all of the necessary rules of inference itself; in particular, ∀_{X} is a term of the calculus that is only meaningful when X is compact; and “subspaces” are defined in a formal way in [B]. This disagreement with Escardó began after his long paper on Synthetic Topology had been

published. For my part, I had already been working on ASD full time for seven years, and my long paper [G], which characterises Computably based locally compact spaces and uses ℝ as a running example, was finished and about to be submitted to a journal.

At that time, however, I did not actually have a construction of Cantor space in ASD, let alone a proof of its compactness. I was nevertheless confident that I would be able to construct it, and that it would have this property. Indeed, the value of the whole ASD programme, and in particular its claim to provide the “right” topology on a space “automatically”, depended on this.

Escardó was extremely reluctant to believe that Cantor space in ASD could be compact, without invoking König’s Lemma and some additional axiom. The ASD calculus is recursively enumerable, and every term in it may be interpreted as a (parallel) program. He therefore expected it to behave in a similar way to Recursive Analysis of the Russian School, where Kleene Trees and Specker Sequences destroy the traditional compactness properties of Cantor space and the real closed interval.

Escardó himself achieves compactness of Cantor space and the real closed interval by relying on the underlying set-theoretical model for the spaces, whilst also requiring the continuous functions to be computable. This idea is essentially Klaus Weihrauch’s “Type Two Effectivity” [Wei00], although I was not familiar with the latter when these notes were written.

In fact, the construction of Cantor space that is presented here is much more like locale theory than traditional general topology, and König’s Lemma never appears in it. Indeed, even though I shamelessly appropriated the word “nucleus” from locale theory, but gave it a different meaning in ASD, these two meanings happen to coincide in this construction, which is therefore essentially also valid in locale theory.

The disagreement became public at the Domains Workshop that was held at the Technical University of Darmstadt at the end of August 2004.

It was Andrej Bauer who subsequently helped me to understand both these pathologies and how ASD overcomes them. These things are explained in [I, Section 12]. The central point seems to be that the subspaces in ASD are not subsets, but formal equalisers that have been adjoined to the category you first thought of by the construction in [B].

This construction had been designed to ensure that these subspace come equipped with the subspace topology, indeed with a canonical way of expanding their open subspaces. The term (called I in [B]) that provides this canonical expansion is inter-definable with the disputed universal quantifier.

I also had the central idea for the constructions in Section 7ff during the same period, although I filled in the details of the proof in September 2006.

It appears that Cantor space will play an important role in ASD in the future, providing representations of other topological spaces, because of its recursion theory, and for other reasons. I expect that that these notes will then be combined with other results and transformed into a more extensive paper.

The following are my original notes towards an introduction.

Some history of the definition of compactness and of Tychonov’s theorem by way of introduction.

The new definition(s) of compactness in ASD, removing at least the naïve use of directed unions.

∀ in ASD satisfies ∀-rules in categorical logic (right adjoint with Beck–Chevalley à la Lawvere) and equivalently proof theory (introduction and elimination with subsitution). It also satisfies the lattice dual of the Fronenius law that relates ∃ and ∧. But, as we shall see, it does not mean “for every”.

Escardó’s quantifier program.

Axioms of ASD: Monadicity, Phoa and Scott.

Give the explicit formula for 2^{ℕ} ↣ Σ^{ℕ} × Σ^{ℕ} and ∀_{2^{ℕ}} in ASD.

Compactness, Tychonov and “∀” in ASD have more to do with directed joins than with “for every” in set theory.

Will construct K^{N} as a compact subspace of K_{⊥}^{N}. Although on the face of it this seems a roundabout way of doing things, it turns out to be the natural setting in which to evaluate the program for ∀ makes full use of the structure of this embedding (Remark 4.12).

The same argument for Tychonov’s theorem will be valid in both ASD and locale theory, apart from some “implementation-specific details”. In order to translate it into a theorem for classical topological spaces, we need the Hofmann–Mislove theorem, and the axiom of choice.

Concentrate on Cantor space 2^{N} ↣ 2_{⊥}^{N} ↣ Σ^{N} × Σ^{N}. We’re interested in natural representations of K^{N}, so if we are given K ↣ Σ^{U} we want to find K^{N} ↣ Σ^{U×ℕ} so that λ-application commutes with the inclusions.

Duals of bases and Scott — probably in a separate paper.

2 Compactness and lifting

In this section we explain how we intend to represent a single space and the product of two spaces, and to encode their compactness. This will prepare us for the generalisation from 2 to N in the next section.

Compactness and lift for a single space

Say something about the lift and partial map classifier.

Remark 2.1 The lift of a compact space.

K ↪ K_{⊥} with adjoints from [D]

K  \overline{}1  Σ^{K}

X ≡ K_{⊥}^{\begin{aligned}i \\ &  \end{aligned}∩}  \overline{↓} Σ \begin{aligned}⊤ \\ &  \end{aligned}Σ^{K_{⊥}} ≡ Σ ↓ Σ^{K} [figure: ∃_{i} ≡ (⊥, id)]⊣ π_{1} [figure] ⊣ \begin{matrix}R_{i} ≡ (∀_{K}, id) \\  \end{matrix}

1 \begin{matrix}⊥_{⊔} &  \\ ⊣ [figure: !] \end{matrix}  \overline{}1^{⊥ }  Σ [figure: Σ^{!} ≡ (id, Σ^{!})]⊣ [figure: π_{0}] ⊣ \begin{matrix}(id, ⊤) \\  \end{matrix}

Σ^{i} ≡ π_{1} and ∀_{K_{⊥}} ≡ Σ^{⊥} ≡ π_{0} ∃_{i} ⊣ Σ^{i} satisfy the Frobenius and Beck–Chevalley laws.

Remark 2.2 Write J ≡ R_{i} · Σ^{i}, so with ψ ≡ (σ, ϕ) : Σ^{K_{⊥}}

J(σ, ϕ) = (∀k.ϕk, ϕ)
= (σ, ϕ) ∨ Σ^{!} · ∀_{K} · Σ^{i}(σ, ϕ)
Jψ  = ψ ∨ Σ^{!} · ∀_{K} · Σ^{i}ψ
= ψ ∨ λx. ∀k. ψ(ik)
= λx. ∀k. (ψx ∨ ψ(ik))  dual Frobenius

Notation 2.3 For x : K_{⊥} we write x↓ : Σ for the predicate that x ∈ K, although when several compact spaces are involved we sometimes write αx, βy, etc. By the usual convention, “x↓” or “Γ ⊢ x↓” means Γ ⊢ x↓ = ⊤ where appropriate.

Remark 2.4 The universal quantifier and necessity operator.

The modal operator □_{K} ≡ ∀_{K} · Σ^{i} is Σ^{!} · J ≡ λψ. Jψ⊥.

Hence ∀_{K} = □_{K} ·I = Σ^{!} · J · I, where I can be either R_{i} or (better) ∃_{i}, so ∀_{K}ϕ = J(Iϕ)⊥.

We have constructed J as a morphism of the category, making use the the definition of compactness of K in ASD. Indeed, it is clear that J ≡ R_{i} · Σ^{i} is a nucleus in the sense of both locale theory, since id ≤ J = J ·J and J preserves ∧, and ASD. In the former discipline, it would be written J ≡ (α ⇒ −), where α classifies the open sublocale K ⊂ K_{⊥}. But J is also Scott-continuous since K is compact.

From the equations for a localic nucleus above, we easily deduce that J(ϕ ∧ ψ) = J(Jϕ ∧ Jψ) and J(ϕ ∨ ψ) = J(Jϕ ∨ Jψ). Using the Scott principle, J then also satisfies the λ-equation for a nucleus in the sense of ASD [G, §7].

In both senses, the nucleus J identifies the open subspace K ⊂ K_{⊥}.

Even though these things are already clear, we shall now prove them again using the ASD λ-calculus. The reason for doing this is that we shall need to repeat the same calculations in more complex circumstances in the next section.

Lemma 2.5 Jψ(ik) = ψ(ik) and Jψ⊥ = ∀k′. ψ(ik′). Proof In each case one term dominates the other:

Jψ⊥ = ∀k′. ψ⊥ ∨ ψ(ik′) = ∀k′. ψ(ik′)
Jψ(ik) = ψ(ik) ∨ ∀k′. ψ(ik′) = ψ(ik)  □

Lemma 2.6 Let Γ, x : K_{⊥} ⊢ ux, vx : Y such that Γ ⊢ u⊥ = v⊥ : Y and Γ, k : K ⊢ u(ik) = v(ik) : Y. Then Γ, x : K_{⊥} ⊢ ux = vx : Y. Proof The point is that 1 + K ↠ K_{⊥} is Σ-epi. By sobriety of Y we are given

[figure: Γ × K_{⊥}; u; v; Y; Σ^{Σ^{Y}}]

in which it is enough to show that the composites are equal. Their double exponential transposes are

[figure: Γ × Σ^{Y}; ū; v̄; Σ^{K_{⊥}}; Σ × Σ^{K}]

but we are given that these composites are equal. □

Lemma 2.7 J is a nucleus in the sense of locale theory. Proof The three (in)equations,

x : K_{⊥}, ψ : Σ^{K_{⊥}} ⊢ ψx ≤ Jψx = J^{2}ψx and J(ψ_{1} ∧ ψ_{2})x = Jψ_{1}x ∧ Jψ_{2}x,

are easily seen to hold in the two cases x = ik and ⊥ (using Lemma 2.5), but this is enough, by Lemma 2.6. □

Lemma 2.8 J is also a nucleus (with id ≤ J) in the sense of ASD. Proof We show

F : Σ^{3}K_{⊥}, x : K_{⊥} ⊢ J(λy. F(λψ. Jψy))x = J(λy. F(λψ. ψy))x

using the same case analysis x = ik or ⊥ respectively as before:

LHS = J(λy. F(λψ. Jψy))(ik)
= (λy. F(λψ. Jψy))(ik)
= F(λψ. Jψ(ik))
= F(λψ. ψ(ik)) = RHS
LHS = ∀k.(λy. F(λψ. Jψy))(ik)
= ∀k.F(λψ. Jψ(ik))
= ∀k.F(λψ. ψ(ik)) = RHS  □

Lemma 2.9 Γ ⊢ x : K_{⊥} is admissible with respect to J iff Γ ⊢ x↓. Proof x : K_{⊥} is admissible for J iff λψ. Jψx = λψ. ψx iff λψ. ∀k′. ψ(ik′) ≤ λψ. ψx.

If x = ik, this holds because it is ∀-elimination. Conversely, consider ψ ≡ (↓), the predicate that classifies K ⊂ K_{⊥}; then admissibility implies (x↓) = ⊤, so x ∈ K. □

Corollary 2.10 K ≅ {X | J}. □

Two spaces

Remark 2.11 Now consider how two such embeddings i : K ↪ K_{⊥} and j : L ↪ L_{⊥} interact.

K × L

................................................. ........................

................................................. ........................ K × \{⊥\}  \overline{\{⊥\} × L}^{...................................................}^{........................}^{...................................................}^{........................}

(⊥, ⊥) •^{..............................................} .............................................. ...................^{...................}

\begin{aligned}K × L & ^{_{⊂} K × j} & K × L_{⊥} & Σ^{K×L} & [figure: ∃_{j}^{K}; ⊥; ⊥; R_{j}^{K}] & Σ^{K×L_{⊥}} \\ K_{⊥} × L & ^{\begin{aligned}i × L \\ & \end{aligned}∩} & ^{_{⊂} K_{⊥} × j} & K_{⊥} × L_{⊥} & ^{\begin{matrix}i × L_{⊥} \\ \end{matrix}∩} & Σ^{K_{⊥}×L} & [figure: ∃_{i}^{L}]⊣ [figure]⊣ \begin{matrix}R_{i}^{L} \\ \end{matrix} & [figure: ∃_{j}^{K_{⊥}}; ⊥; ⊥; R_{j}^{K_{⊥}}] & Σ^{K_{⊥}×L_{⊥}} & [figure: ∃_{i}^{L_{⊥}}]⊣ [figure]⊣ \begin{matrix}R_{i}^{L_{⊥}} \\ \end{matrix} \end{aligned}

The unlabelled middle arrows are Σ^{i×L} ≡ (Σ^{i})^{L} etc.

Remark 2.12 Since i is an open inclusion, it satisfies the Beck-Chevalley law with respect to the pullback above.

[figure: K_{⊥} × L; ⊂; K_{⊥} × j; K_{⊥} × L_{⊥}; π_{0}; K_{⊥}.]

The law says that

∃_{i}^{L} · Σ^{K×j} = Σ^{K_{⊥}×j} · ∃_{i}^{L_{⊥}}.

Now, in the situation above, all of these maps have right adjoints, so

R_{j}^{K} · Σ^{i×L} = Σ^{i×L_{⊥}} · R_{j}^{K_{⊥}},

i.e. Σ^{j} ⊣ R_{j} satisfy a Beck–Chevalley condition with respect to K × L_{⊥} ↪ K_{⊥} × L_{⊥} → L_{⊥}, even though j is not a closed inclusion.

From this it follows that the nuclei J_{1}^{L_{⊥}} and J_{2}^{K_{⊥}} commute, and Σ^{K×L} is the splitting of the composite idempotent. □

Now, the Beck–Chevalley law was proved in [C, Proposition 3.11] by a simple λ-calculation. We can prove commutation directly here instead.

Lemma 2.13 J_{1}^{L_{⊥}} and J_{2}^{K_{⊥}} commute. Proof Let θ : Σ^{K_{⊥}×L_{⊥}}, x : K_{⊥} and y : L_{⊥}.

By case analysis for y = ⊥, jℓ,

∀k. (θ(ik)y ∨ ∀ℓ′. θ(ik)(jℓ′)) = (∀k. θ(ik)y) ∨ (∀kℓ′. θ(ik)(jℓ′))

J_{2}^{K_{⊥}}θxy  = θxy ∨ ∀ℓ:L. θx(jℓ)
J_{1}^{L_{⊥}}(J_{2}^{K_{⊥}}θ)xy = J_{2}^{K_{⊥}}θxy ∨ ∀k:K. J_{2}^{K_{⊥}}θ(ik)y
= θxy ∨ (∀ℓ:L. θx(jℓ)) ∨ ∀k. (θ(ik)y ∨ ∀ℓ. θ(ik)(jℓ))
= θxy ∨ (∀ℓ. θx(jℓ)) ∨ (∀k. θ(ik)y) ∨ (∀kℓ. θ(ik)(jℓ))  above
= θxy ∨ (∀k. θ(ik)y) ∨ ∀ℓ. (θx(jℓ) ∨ ∀k. θ(ik)(jℓ))  similarly
= J_{1}^{L_{⊥}}θxy ∨ ∀ℓ. J_{1}^{L_{⊥}}θx(jℓ) = J_{2}^{K_{⊥}}(J_{1}^{L_{⊥}}θ)xy  □

Remark 2.14 Another way to see commutation using locale theory is to recall that J_{1} = (α ⇒ −) and J_{2} = (β ⇒ −), where α and β classify the open inclusions i and j. The composite nucleus is then α ⇒ (β ⇒ −) = (α ∧ β ⇒ −) = β ⇒ (α ⇒ −). □

Remark 2.15 For compactness of K × L we compose the right adjoints Σ^{K×L} → Σ^{K_{⊥}×L_{⊥}} → Σ, the second being given by application to (⊥, ⊥):

□_{K×L} θ = (J_{1}^{L_{⊥}} · J_{2}^{K_{⊥}}) θ (⊥, ⊥) and ∀_{K×L}ϕ = □_{K×L}(Iϕ).

When we expand this, the fourth term in the expression for Jθ, namely ∀kℓ. θ(ik)(jℓ), dominates the others. This is hardly surprising, but the point is that we can generalise from here to the infinite case.

3 Cantor space

In this section we shall construct Cantor space 2^{N} and show that it is compact, by generalising the embedding K × L ↣ K_{⊥} × L_{⊥} in the previous section to K^{N} ↣ (K_{⊥})^{N}. In fact, the method proves compactness of K^{N} on the assumption that K_{⊥}^{N} exists. You may think of N as ℕ, but we are using its topological properties, not arithmetic or recursion — in the classical model, N could be ℵ_{1} if you wish.

Peter Johnstone: see his original proof of Tychonov’s theorem for locales (in the paper, not the book) and also that of Tychonov⇒Choice using non-sober spaces.

Remark 3.1 In the following argument, N must be an overt space with decidable equality (discrete and Hausdorff), although Proposition 4.3 will eliminate the Hausdorffness assumption.

This is because we need to switch the arguments independently: the expression for Jθ in the case of a binary product had four disjuncts. These become 2^{n} for a product of n factors, switching between x : K_{⊥} and k : K in each of the n arguments of θ. The disjunction over 2^{n} cases will turn into existential quantification over ListN, so N itself must be overt.

Lemma 3.2 The exponential (K_{⊥})^{N} exists in the category of locales. Proof As N is a set with (decidable) equality and the discrete topology, it is (stably) locally compact. Hence all exponentials X^{N} exist in the category of locales. □

Local compactness of (K_{⊥})^{N} in locale theory and its existence in ASD are more difficult to show. So in the first instance we shall be content with the case K = 2. Other compact spaces K will be handled later.

Lemma 3.3 (2_{⊥})^{N} is the closed subspace of pairs of predicates on N that don’t hold simultaneously:

[figure: 2_{⊥}^{N}; 1; Σ^{N} × Σ^{N}; ⊓; ϕ, ψ ↦ ∃n. ϕn ∧ ψn; Σ; ⊥]

Hence the subspace 2_{⊥}^{N} ↣ Σ^{N} × Σ^{N} is defined by an inflationary Scott-continuous nucleus (in both senses), namely F ↦ F ∨ λϕψ. ∃n. ϕn ∧ ψn. There is a similar construction for any finite (i.e. overt discrete compact Hausdorff) space instead of 2. □

Remark 3.4 Cantor space, 2^{N}, will be constructed in the course of the following argument using another Scott-continuous nucleus (on 2_{⊥}^{N}). Then the composite embedding

2^{N} ↣ 2_{⊥}^{N} ↣ Σ^{N} × Σ^{N} is by f ↦ (λn. (fn = 0), λn. (fn = 1))

as we would expect.

Notation 3.5 Define Ω ≡ (K_{⊥})^{N} and

n : N, f : Ω, F : Σ^{Ω} ⊢ J_{n}F f ≡ F f ∨ ∀k:K. F (λm. if m = n then ik else fm) : Σ.

Remark 3.6 The idea of the following argument is that N ≅ (N \ {n}) + {n} so Ω = Ω_{n} × K_{⊥} where Ω_{n} ≡ K_{⊥}^{N\{n}} and then J_{n} = (R_{i} · Σ^{i})^{Ω_{n}} is the nucleus that defines the compact open subspace Ω_{n} × K ⊂ Ω_{n} × K_{⊥}.

Similarly, commutation follows from the treatment of two spaces by applying (−)^{Ω_{nm}} to the whole diagram, where Ω_{nm} ≡ K_{⊥}^{N\{n,m}}.

The λ-calculation can also be done directly, but for the case analysis (Lemma 2.6) we still need the Σ-epi Ω_{n} × K + Ω_{n} ↠ Ω_{n} × K_{⊥}.

Lemma 3.7 n : N ⊢ J_{n} : Σ^{Ω} → Σ^{Ω} is a family of nuclei in both senses. Proof For brevity, write

n : N, x : K_{⊥}, f : K_{⊥}^{N} ⊢ f_{x} ≡ λm. if m = n then x else fm

so f = f_{fn} and

J_{n}F f = F f_{fn} ∨ ∀k′. F f_{ik′}
J_{n}F f_{ik} = F f_{ik} ∨ ∀k′. F f_{ik′} = F f_{ik}
J_{n}F f_{⊥} = F f_{⊥} ∨ ∀k′. F f_{ik′} = ∀k′. F f_{ik′}.

Lemma 2.6 says that it is enough to consider these two cases.

For the localic result, F f ≤ J_{n}F f,

J_{n}^{2}F f_{ik}  = J_{n}F f_{ik} = F f_{ik}
J_{n}^{2}F f_{⊥}  = ∀k′. J_{n}F f_{ik′} = ∀k′. F f_{ik′}
J_{n}(F ∧ G)f_{ik} = (F ∧ G)f_{ik} = F f_{ik} ∧ Gf_{ik} = J_{n}F f_{ik} ∧ J_{n}Gf_{ik}
J_{n}(F ∧ G)f_{⊥} = ∀k′. (F ∧ G)f_{ik′}
= ∀k′. F f_{ik′} ∧ ∀k′. Gf_{ik′} = J_{n}F f_{⊥} ∧ J_{n}Gf_{⊥}.

For J_{n} to be a nucleus in the sense of ASD we must show that

n : N, f : Ω, F : Σ^{3}Ω ⊢ J_{n}Hf = J_{n}Gf,

where G ≡ λg. F(λF. F g) and H ≡ λg. F(λF. J_{n}F g)

satisfy Gf_{ik} = F(λF. F f_{ik}) = F(λF. J_{n}F f_{ik}) = Hf_{ik}.

So if fn = ik then

LHS = J_{n}Hf = J_{n}Hf_{ik} = Hf_{ik} = Gf_{ik} = J_{n}Gf_{ik} = RHS

whilst if fn = ⊥ then

LHS = J_{n}Hf_{⊥} = ∀k′. J_{n}Hf_{ik′} = ∀k′. Hf_{ik′}
= ∀k′. Gf_{ik′} = J_{n}Gf_{⊥} = RHS.  □

Lemma 3.8 As in Lemma 2.9, for Γ ⊢ f : Ω, n : N

Γ ⊢ fn↓

= Γ, F : Σ^{Ω} ⊢ J_{n}F f ≤ F f where the predicate above the line is of type Σ, and for the inequality below it (which is really equality since id ≤ J_{n}) we say that “f is J_{n}-admissible”. Proof If fn↓ then F f = ϕ(fn) = J_{n}F f.

Conversely, put F ≡ λf. fn↓, so ϕ = ↓ and J_{n}F f = (ik)↓ = ⊤, whence fn↓ = F f = J_{n}F f = ⊤. □

Remark 3.9 For each n : N, this condition defines a compact open subspace of K_{⊥}^{N}. We intend to form the intersection of these subspaces over n : N. This intersection is again compact but no longer open. The “quantification” over n implicit in this statement comes from the fact that the proof above is uniform in n : N, so

Γ, n : N ⊢ fn↓

= Γ, F : Σ^{Ω}, n : N ⊢ J_{n}F f ≤ F f,

We shall bind the free variable n in the bottom line by forming the join of the nuclei J_{n}. For this, we first consider the join of two commuting nuclei, then of any (Kuratowski-) finite set of them.

This will leave us with the directed union of a family of inflationary Scott-continuous nuclei. Classically, this is the situation of the Hofmann–Mislove theorem, and corresponds to the codirected intersection of of the corresponding compact subspaces. (PTJ for the localic version).

Lemma 3.10 n, m : N ⊢ J_{n} · J_{m} = J_{m} · J_{n}. Proof Since equality on N is decidable, we may consider the cases n = m and n ≠ m separately, the former being trivial. Put

θxy = F (λr. if r = n then x else if r = m then y else fr)

so F f = θ(fn)(fm) etc. Then the expansions of both J_{n}(J_{m}θ)xy and J_{m}(J_{n}θ)xy are

θxy ∨ ∀k_{1}. θ(ik_{1})y ∨ ∀k_{2}. θx(ik_{2}) ∨ ∀k_{1}. ∀k_{2}. θ(ik_{1})(ik_{2}),

as in Lemma 2.13, with the same case analysis to justify commutation of ∀k and ∨. □

Lemma 3.11 The composite of two commuting nuclei is again a nucleus, which encodes the intersection of the corresponding subspaces. Proof This is a general result to which [B, Remark 5.10] alluded without stating it clearly. We nevertheless call the two nuclei J_{n} and J_{m} for the sake of compatibility of notation. These satisfy

F : Σ^{3}Ω ⊢ J_{n}(λf. F(λF. J_{n}F f)) = J_{n}(λf. F(λF. F f))
G : Σ^{3}Ω ⊢ J_{m}(λf. G(λG. J_{m}Gf)) = J_{m}(λf. G(λG. Gf))

from which we deduce, for G : Σ^{3}Ω,

(J_{n} · J_{m})(λf. G(λG. (J_{n} · J_{m})Gf))
= (J_{m} · J_{n})(λf. G(λG. (J_{n} · J_{m})Gf))  J_{n}, J_{m} commute
= J_{m}(J_{n}(λf. (G · Σ^{J_{m}})(λG. J_{n}Gf)))  def Σ^{J_{m}}
= J_{m}(J_{n}(λf. (G · Σ^{J_{m}})(λG. Gf)))  J_{n} nucleus
= (J_{n} · J_{m})(λf. (G · Σ^{J_{m}})(λG. Gf))  J_{n}, J_{m} commute
= J_{n}(J_{m}(λf. G(λG. J_{m}Gf)))  def Σ^{J_{m}}
= J_{n}(J_{m}(λf. G(λG. Gf)))  J_{m} nucleus wrt G

so J_{n} · J_{m} is a nucleus.

To show that this encodes the intersection, let Γ ⊢ f : Ω. Then

Γ, F : Σ^{Ω} ⊢ J_{n}F f = F f = J_{m}F f = Γ, F : Σ^{Ω} ⊢ (J_{n} · J_{m})F f = F f

because, downwards,

(J_{n} · J_{m})F f = J_{n}(J_{m}F)f = J_{m}F f = F f

since f is J_{n}-admissible wrt J_{m}F and J_{m}-admissible wrt F. Conversely,

(J_{m}F)f = (J_{n} · J_{m})(J_{m}F)f = (J_{n} · J_{m} · J_{m})F f = (J_{n} · J_{m})F f = F f

since f is (J_{n} ·J_{m})-admissible wrt both J_{m}F and F, and J_{m} is idempotent. Similarly, J_{n}F f = F f.

□

Notation 3.12 Define ℓ : ListN ⊢ J_{ℓ} : Σ^{Ω} → Σ^{Ω} by list recursion [E] from J_{0} ≡ id and

J_{n::ℓ}F f ≡ (J_{n} · J_{ℓ})F f = J_{ℓ}F f ∨ ∀k. J_{ℓ}F (λm. if m = n then k else fm).

This is the composite of {J_{n} | n ∈ ℓ}, and encodes the intersection of the corresponding subspaces.

Lemma 3.13 J_{ℓ} is a family of nuclei (in both senses), and, for Γ ⊢ F : K_{⊥}^{N},

n : N, F : Σ^{Ω} ⊢ J_{n}F f ≤ F f = ℓ : ListN, F : Σ^{Ω} ⊢ J_{ℓ}F f ≤ F f

Proof ℓ : ListN ⊢ J_{ℓ} is a nucleus, by equational list induction, as it is a composite of commuting nuclei.

To prove the second part upwards, n ∈ ℓ ⊢ J_{n} ≤ J_{ℓ}.

Downwards, by induction on ℓ. J_{0}F f = F f and

J_{n::ℓ}F f ≡ J_{n}(J_{ℓ}F)f ≤ J_{n}F f = F f.  □

Remark 3.14 Since the J_{n} are commuting idempotents (and composition is associative), if ℓ_{1} ∼ ℓ_{2} in the congruence generated by the semilattice laws (idempotence and commutation) then J_{ℓ_{1}} = J_{ℓ_{2}}.

Hence the subscript may be considered to range over KN (the “finite powerset” of N) [E], and we have defined the intersection of any (Kuratowski-) finite collection of the compact open subspaces. □

Lemma 3.15 ⊢ J ≡ ∃ℓ:KN . J_{ℓ} is a nucleus on Ω (in both senses) and, for Γ ⊢ f : K_{⊥}^{N},

Γ, ℓ : KN, F : Σ^{Ω} ⊢ J_{ℓ}F f ≤ F f = Γ, F : Σ^{Ω} ⊢ JF f ≤ F f Proof The join is directed, so by Scott continuity [G, §7] J is a (Scott-continuous, inflationary) nucleus in the sense of either locale theory or ASD. The second part is the definition of the join J = ∃ℓ. J_{ℓ}. □

Lemma 3.16 TFAE for Γ ⊢ f : K_{⊥}^{N} or Γ, n : N ⊢ fn : K_{⊥}:

(a) Γ ⊢ λn. (fn↓) = ⊤ : Σ^{N};

(b) Γ, n : N ⊢ (fn↓) = ⊤ : Σ;

(c) Γ, n : N, F : Σ^{Ω} ⊢ J_{n}F f = F f, i.e. f is admissible wrt each J_{n},

(d) Γ, ℓ : KN, F : Σ^{Ω} ⊢ J_{ℓ}F f = F f, i.e. f is admissible wrt each J_{ℓ},

(e) Γ, F : Σ^{Ω} ⊢ JF f = F f, i.e. f is admissible wrt J ≡ ∃ℓ. J_{ℓ},

(f) Γ ⊢ f : {Ω | J}. Proof The steps use λ-abstraction, 3.8, 3.13, 3.15 and [B, §8]. □

Proposition 3.17 {Ω | J} forms a pullback as shown and is the required exponential K^{N}.

[figure: {Ω | J}; 1; Ω ≡ K_{⊥}^{N}; (↓)^{N}; Σ^{N}; ⊤]

Proof For Γ ⊢ f : K_{⊥}^{N}, (a) says that f and ! form a commutative trapezium, whilst (f) says that it factors through {Ω | J}, so this is a pullback. Then s : Γ × N → K corresponds to f : Γ × N → K_{⊥} with Γ, n : N ⊢ fn↓, which is (b), and then (f) provides f : Γ → {Ω | K} as required for the exponential transposition. □

Theorem 3.18 If K is compact, N is overt discrete Hausdorff and the exponential K_{⊥}^{N} exists then the exponential K^{N} exists and is compact. Proof By definition [B], the inclusion i : {Ω | J} ↣ Ω comes with R : Σ^{{Ω|J}} ↣ Σ^{Ω} such that id ≤ J = R · Σ^{i} and Σ^{i} · R = id, so Σ^{i} ⊣ R.

Also, evaluation at λn. ⊥ : K_{⊥}^{N} provides the right adjoint to the inverse image Σ^{!} for ! : K_{⊥}^{N} → 1.

The composite of these provides the quantifier,

Σ^{!} ⊣ λϕ. (Rϕ)(λn. ⊥) ≡ ∀_{K^{N}} ,

as required to show that K^{N} is compact, and so proves Tychonov’s theorem in this case. □

This is the first time in the ASD programme when we have made “public” use of the Σ-splitting of the representation of an object as a subspace. Recall from the normalisation theorem in [B] that this is best avoided: whilst the translation erases i and admit, it turns the Σ-splitting into the corresponding nucleus, in this case J.

4 Properties of Cantor space

This section collects various observations about the preceding construction.

It is an example of the limit–colimit coincidence in several ways. In the following diagrams, ℓ ⊂ ℓ′ range over ListN.

Remark 4.1 First, recall that {Ω | J_{n}} and {Ω | J_{ℓ}} are compact open subspaces of Ω, so the corresponding inverse image maps have adjoints on both sides. However, {Ω | J} is compact but no longer open, so its inverse image has an adjoint on the right but not the left. As we have seen, {Ω | J} is the intersection (limit) of the {Ω | J_{n}} or {Ω | J_{ℓ}}. Hence Σ^{{Ω|J}} is the colimit of the corresponding algebras and homomorphisms, and therefore the filtered colimit of the {Ω | J_{ℓ}} and functions. It is also the limit of the right adjoints, but these adjoint pairs are not embeddings and projections of classical domain theory. The limit–colimit coincidence for general adjoint pairs is discussed in the classical case in [Tay86, Tay87]. (Say a bit about how the generalised coincidence works.)

[figure: K^{N} = {Ω | J}; {Ω | J_{ℓ′}}; {Ω | J_{ℓ}}; {Ω | J_{0}} = Ω]

[figure: Σ^{{Ω|J}}; ⊥̸; ⊥; Σ^{{Ω|J_{ℓ′} }}; ⊥; ⊥; Σ^{{Ω|J_{ℓ}}}; ⊥; ⊥; Σ^{Ω}]

Remark 4.2 When we regard K_{⊥}^{N} as an infinitary product, or rather as a cofiltered limit of finite products and proper maps, we find another limit–colimit coincidence, which this time does consist of embeddings and projections.

[figure: K^{N}; K^{ℓ′}; K^{ℓ}; 1; K_{⊥}^{N}; ⊤; K_{⊥}^{ℓ′}; ⊤; K_{⊥}^{ℓ}; ⊤; Σ]

The left adjoint extends f : K_{⊥}^{ℓ}, which is Γ×ℓ _{⊃} U → K, by composition with Γ×ℓ′ _{⊃} Γ×ℓ. Applying Σ^{(−)} to this diagram yields

[figure: Σ^{K^{N}}; ⊤; Σ^{K^{ℓ′}}; ⊤; Σ^{K^{ℓ}}; ⊤; Σ]

(and similarly with K_{⊥} in place of K), which is again a colimit of embeddings and a limit of projections. □

Proposition 4.3 If K is compact Hausdorff, M is overt discrete and definable, and the exponential K_{⊥}^{ℕ} exists, then K^{M} exists and is compact Hausdorff. Proof Every definable overt discrete object M is a quotient of an overt discrete Hausdorff object N (such as ℕ) by an open equivalence relation ∼. So there is a coequaliser (∼) ⇉ M ↠ N, which we expect to provide an equaliser K^{N} ↣ K^{M} ⇉ K^{(∼)}.

Since M and (∼) are overt discrete Hausdorff, K^{M} and K^{(∼)} exist and are compact. So it is enough to show that the equaliser defines a closed subspace, but this is co-classified by λf. ∃m_{1}m_{2}. (m_{1} ∼ m_{2}) ∧ (fm_{1} ≠ fm_{2}).

For Hausdorffness, (f ≠ g) = ∃n. (fn ≠ gn). □

Lemma 4.4 There are maps p : KN×KN → 2^{N} and P : Σ^{KN×KN} → Σ^{2^{N}} such that P θ(p(ℓ_{0}, ℓ_{1})) = θ(ℓ_{0}, ℓ_{1}). Proof

p(ℓ_{0}, ℓ_{1})  ≡ λn. n ∈ ℓ_{0} ∧ n ∉ ℓ_{1}
P θ  ≡ λs. ∃ℓ_{0}ℓ_{1}. (∀n ∈ ℓ_{0}. sn = 0) ∧ (∀n ∈ ℓ_{1}. sn = 1) ∧ θ(ℓ_{0}, ℓ_{1})
P θ(p(ℓ_{0}, ℓ_{1})) = ∃ℓ′_{0}ℓ′_{1}. (∀n ∈ ℓ′_{0}. ¬(n ∈ ℓ_{1} ∧ n ∉ ℓ_{0})) ∧ (∀n ∈ ℓ′_{1}. n ∈ ℓ_{1} ∧ n ∉ ℓ_{0}) ∧ θ(ℓ′_{0}, ℓ′_{1})
= ∃ℓ′_{0}ℓ′_{1}. (ℓ′_{0} ∩ ℓ_{1} ⊂ ℓ_{0}) ∧ (ℓ′_{1} ⊂ ℓ_{1} \ ℓ_{0}) ∧ θ(ℓ′_{0}, ℓ′_{1})
≥ θ(ℓ_{0}, ℓ_{1})

putting ℓ′_{0} ≡ ℓ_{0} and ℓ′_{1} ≡ ℓ_{1} \ ℓ_{0}. We need monotonicity of θ for ≤, or a better description of the Vietoris space on 2^{N}. □

Corollary 4.5 2^{N} is overt. (We could also do this using Baire’s theorem, as K^{N} is the intersection of overt dense subspaces.) □

Proposition 4.6 2^{ℕ} is not discrete. Proof If it were,

(a) it would be overt discrete compact Hausdorff, and therefore finite (listable);

(b) there would be a universal quantifier for decidable predicates on ℕ;

(c) ∃n. ϕn would be decidable whenever ϕ is, so all definable predicates would be decidable. Somehow the last two conflict with Scott continuity. □

Corollary 4.7 {0} ⊂ 2^{ℕ} is not open. Proof “Exclusive or” or addition modulo 2 is a binary operation (in fact an Abelian group structure) on 2^{N} such that, for s, t : 2^{N}, s = t ⊣⊢ (s + t) = 0. So {0} would be open iff 2^{ℕ} were discrete. □

Remark 4.8 Next we consider the universal quantifier in a more computational way. For this purpose, it is more convenient to work with K_{⊥}^{N}, since is more closely related to computation than is K^{N}. So, instead of the universal quantifier ∀_{K^{N}} : Σ^{K^{N}} → Σ itself, we consider the necessity modal operator □ ≡ ∀_{K^{N}} · Σ^{i} : Σ^{K_{⊥}^{N}} → Σ^{K^{N}} → Σ. By construction, □ F = JF ⊥.

Remark 4.9 The join over ℓ : KN may be rewritten as

∃ℓ. J_{ℓ} = J_{0} ∨ ∃nℓ. J_{n::ℓ},

thereby providing a fixed point equation like those in [E]:

JF f = ∃ℓ. J_{ℓ}F f
= J_{0}F f ∨ ∃nℓ. J_{n::ℓ}F f
= J_{0}F f ∨ ∃nℓ. (J_{ℓ}F f ∨ ∀k. J_{ℓ}F (λm. if m = n then ik else fm))
= J_{0}F f ∨ ∃nℓ. J_{ℓ}F f ∨ ∃nℓ. ∀k. J_{ℓ}F (λm. if m = n then ik else fm)
=^{∗} ∃ℓ. J_{ℓ}F f ∨ ∃n. ∀k. ∃ℓ. J_{ℓ}F (λm. if m = n then ik else fm)
= JF f ∨ ∃n. ∀k. JF (λm. if m = n then ik else fm)
= JF f ∨ ∃n. J(∀k. F (λm. if m = n then ik else fm))

using Scott-continuity of ∀k (“directed Choice”) in the step marked (=^{∗}), and the fact that J preserves ∀k in the last step.

The “∃n” in this formula may look a little odd. What it means is that the unwinding of this fixed point equation is allowed to select the dimensions n ∈ ℓ ⊂ N in whatever order it pleases.

Remark 4.10 Specialising to the case N = ℕ, we can consider the dimensions in numerical order. We also reformulate the fixed point property in terms of shifting the stream by one place either way. In particular, for f : K_{⊥}^{ℕ} and x : K_{⊥} we write

x :: f ≡ λn. if n = 0 then x else f(n − 1)
head f ≡ f0
tail f ≡ λn. f(n + 1).

This isomorphism arises from ℕ ≅ 1 + ℕ and acts on the subspaces and nuclei:

[figure: ℕ; K^{ℕ}; K_{⊥}^{ℕ}; Σ^{K_{⊥}^{ℕ}}; 1 + ℕ; ≅; K × K^{ℕ}; ≅; K_{⊥} × K_{⊥}^{ℕ}; ≅; Σ^{K_{⊥}×K_{⊥}^{ℕ}}; ≅]

The nucleus J defining K^{ℕ} ↣ K_{⊥}^{ℕ} is then isomorphic to a nucleus J′ on K_{⊥} × K_{⊥}^{ℕ} defined for G : Σ^{K_{⊥}×K_{⊥}^{ℕ}}, x : K_{⊥} and f : K_{⊥}^{ℕ} by

J′Gxf = (J^{K_{⊥}} · J_{1}^{K_{⊥}^{ℕ}})Gxf
= J^{K_{⊥}}(λg. J_{1}(λy. Gyg))xf
= J^{K_{⊥}}(λgy. Gyg ∨ ∀k. G(ik)g))xf
= J(λg. Gxg ∨ ∀k. G(ik)g))f,

where we write J_{1} for the nucleus in Remark 2.2 that defines K ⊂ K_{⊥}. Applying the isomorphism,

F : Σ^{K_{⊥}^{ℕ}}, f : K_{⊥}^{ℕ} ⊢ JF f = J(λg. F (f0 :: g) ∨ ∀k. F (ik :: g))(tail f)

and so

□ F = JF ⊥ = J(λg. ∀k. F (ik :: g))⊥
= □ (λg. ∀k. F (ik :: g))
= ∀k. □ (λg. F (ik :: g)).

Remark 4.11 In the special case of Cantor space (K = 2), this is

□ F = □ (λg. F (0 :: g) ∧ F (1 :: g)) = □ (λg. F (0 :: g)) ∧ □ (λg. F (1 :: g)),

or, considering s : 2^{ℕ} and P : Σ^{2^{ℕ}} instead of g : K_{⊥}^{ℕ} and F : Σ^{2_{⊥}^{ℕ}},

∀_{2^{ℕ}}P = ∀_{2^{ℕ}}(λs. P (0 :: s) ∧ P (1 :: s)) = ∀_{2^{ℕ}}(λs. P (0 :: s)) ∧ ∀_{2^{ℕ}}(λs. P (1 :: s)),

which is the fixed point equation in [Esc04, p37, bottom].

Unfortunately, it is not clear from this equation as it stands how it is to be interpreted as a recursive program, in particular when it is supposed to terminate. Escardó goes on to describe a solution to this problem that relies on the call-by-name evaluation order in the lazy functional programming language Haskell.

More briefly, we can see what the intended behaviour must be by comparing this equation with the previous version: it has to be unwound n times, such that for each of the 2^{n} prefixes ℓ of length n, P (ℓ :: s) returns true without examining the tail s. □

Remark 4.12 Notice that, even though to obtain □ F we just apply JF to ⊥ on the outside of the program, in the course of unwinding the recursion JF is applied to partial functions of arbitrary finite support. This is the computational reason why we should define J and not just ∀ itself.

Remark 4.13 How are we going to construct (2^{N})_{⊥}^{N}?

Maybe (2^{N})_{⊥}^{N} ↣ Σ^{N} × 2_{⊥}^{N×N} by a similar construction to that defining K^{N} ↣ K_{⊥}^{N}.

Then if K is a subquotient of 2^{N} by a closed partial equivalence relation, K_{⊥}^{N} is also a subquotient of (2^{N})_{⊥}^{N}. (NB this only works because it involves lifting ℓ → K to ℓ → 2^{N} with ℓ finite.)

Dependent products, and partial products of compact objects along open maps.

K^{N} and N^{K} using bases.

5 Baire space is not definable

We shall now show that there are neither all exponentials nor all finite limits in the free model of ASD, i.e. the category of types and terms that are definable in the calculus. In particular, we shall show that no definable object has the universal property of the exponential ℕ^{ℕ} (known as Baire space) or that of a certain pullback.

Remark 5.1 Functional programmers have nothing to worry about, since ℕ^{ℕ} is not the denotation of the programming datatype nat → nat. This is because amongst the programs of this type are many that fail to terminate, and therefore whose denotations are partial functions, whereas ℕ^{ℕ} is the space of total functions. (More fundamentally, ℕ is the honest discrete natural numbers object of pure mathematics, not a domain with ⊥.) So the denotation of nat → nat is either (ℕ_{⊥})^{ℕ} or (ℕ_{⊥})^{(ℕ_{⊥})}, according as we insist that the program read its argument or not.

On the other hand, there is a cartesian closed category of which ℕ_{⊥}, (ℕ_{⊥})^{ℕ} and (ℕ_{⊥})^{(ℕ_{⊥})} are objects, and which is definable as a full subcategory of any model of ASD. Its objects are known as Scott domains [F]. A larger cartesian closed category, analogous to SFP or bifinite domains, could also be defined and used in the usual way for nondeterminism.

Remark 5.2 Beware also that the following discussion applies to the free model, i.e. we shall show that ℕ^{ℕ} is not definable. The argument does not show that it is inconsistent.

Indeed, there is a model of ASD that, as in Synthetic Domain Theory, is a reflective subcategory of a topos, where the reflector preserves finite products. Such a model is cartesian closed, and also complete and cocomplete (in so far as the topos is).

(This topos consists of sheaves on the opposite of the (essentially small) category of algebras for the Σ^{Σ^{(−)}} monad in the effective topos.)

The import of the result of this section in such a model is that, whilst the object ℕ^{ℕ} exists, it is not locally compact. In fact, we shall work from the traditional definition of local compactness, namely the existence of a basis of compact neighbourhoods. An object has this property iff it is a Σ-split subspace of Σ^{N}, with N overt discrete, and this is the relationship with definability in ASD [G].

Remark 5.3 We begin by recalling the classical argument that we intend to translate into ASD. The central idea is that compact subspaces of ℕ^{ℕ} are small, whilst inhabited open ones are large, and so the situation 0 ∈ U ⊂ K ⊂ ℕ^{ℕ} that is characteristic of locally compact spaces is impossible.

More precisely, if K ⊂ ℕ^{ℕ} is compact then so is each of its images K ↠ K_{n} ⊂ ℕ under the continuous maps ev_{n} : ℕ^{ℕ} → ℕ. Then K_{n} is bounded, say by g(n), for some function g : ℕ → ℕ, which means that if f ∈ K then ∀n. fn < gn.

A nonempty open subspace of ℕ^{ℕ} in the Tychonov or compact–open topology, on the other hand, is restricted in only finitely many dimensions, being the whole of ℕ in the others. Hence it cannot be contained in K. However, this depends on the prior existence of ℕ^{ℕ} and the characterisation of its open sets, so we shall have to modify the argument for ASD.

For the least upper bound g(n) we also rely on classical logic (excluded middle). Instead we shall find some upper bound, for which a choice principle is needed.

Remark 5.4 State the existence and choice principles, and why we expect them to hold in the free model.

Proposition 5.5 Let N be overt discrete Hausdorff. Then the following are equivalent:

(a) a closed subspace (coclassified by ⊢ ψ : Σ^{N}) of a finite subspace ⊢ ℓ_{0} : ListN;

(b) a compact subspace i : K ⊂ N; and

(c) a necessity operator ⊢ A : Σ^{Σ^{N}} that preserves ⊤ and ∧. Proof [a⇒b] is standard; [b⇒c] A = ∀_{K} · Σ^{i} and [a⇒c] A = λϕ. ∀n ∈ ℓ_{0}. ϕn ∨ ψn.

[c⇒a] By the basis expansion, A = λϕ. ∃ℓ. A(λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕn.

Then ⊢ ⊤ = A⊤ = ∃ℓ. A(λn. n ∈ ℓ).

So by the existence property, there’s some ⊢ ℓ_{0} : ListN with ⊢ A(λn. n ∈ ℓ_{0}) = ⊤.

Also let ψ ≡ λn. A(λm. n ≠ m).

I claim that A is recovered from ℓ_{0} and ψ by the formula above.

Using the ListN-indexed ∨-basis for N, it suffices to check this for ϕ = λn. n ∈ ℓ for ℓ : ListN, i.e.

∀n ∈ ℓ_{0}. (ϕn ∨ ψn) = ∀n ∈ ℓ_{0}. n ∈ ℓ ∨ A(λm. n ≠ m)
= ∀n ∈ (ℓ_{0} \ ℓ). A(λm. n ≠ m)
= A(λn. n ∉ (ℓ_{0} \ ℓ))  filter
= A(λn. n ∉ (ℓ_{0} \ ℓ)) ∧ A(λn. n ∈ ℓ_{0})  this is ⊤
= A(λn. n ∉ (ℓ_{0} \ ℓ) ∧ n ∈ ℓ_{0})  filter
= A(λn. n ∈ ℓ ∧ n ∈ ℓ_{0})
= A(λn. n ∈ ℓ) ∧ A(λn. n ∈ ℓ_{0})  filter
= A(λn. n ∈ ℓ) = Aϕ  this is ⊤. □

Lemma 5.6 Let n : ℕ ⊢ A_{n} : Σ^{Σ^{ℕ}} preserve ⊤ and ∧. Then there is some morphism g : ℕ → ℕ (i.e. n : ℕ ⊢ gn : ℕ) such that n : ℕ ⊢ ⊤ = A_{n}(λm. m < gn). Proof By the same argument, using the choice principle in place of the existence property. □

Lemma 5.7 Suppose that the exponential ℕ^{ℕ} exists, and let K be a compact subspace of it. Then there is some morphism g : ℕ → ℕ such that if Γ ⊢ h : K then n : ℕ ⊢ hn < gn. Proof Let ⊢ A : Σ^{Σ^{ℕ}} be the modal operator corresponding to K and put

n : ℕ ⊢ A_{n} ≡ λϕ. A(λf. ϕ(fn)),

which also preserve ⊤ and ∧. By Lemma 5.6, there is some g : ℕ → ℕ such that

n : ℕ ⊢ ⊤ = A_{n}(λm. m < gn) = A(λf. fn < gn).

Now let Γ ⊢ h ∈ K, which means that Γ, ϕ : Σ^{ℕ^{ℕ}} ⊢ ϕh ≥ Aϕ. So

Γ, n : ℕ ⊢ ⊤ = A(λf. fn < gn) ≤ (λϕ. ϕh)(λf. fn < gn) = (hn < gn).  □

Theorem 5.8 Baire space, the exponential ℕ^{ℕ}, is not locally compact. Proof If it were locally compact, there would be 0 ∈ U ⊂ K ⊂ ℕ^{ℕ} with U open and K compact. Let g : ℕ → ℕ bound K as in Lemma 5.7.

The following argument avoids relying on the prior characterisation of U in Remark 5.3. Define i : 2^{ℕ} → ℕ^{ℕ} by

isn ≡ \{ \begin{matrix}0 & if sn = 0 \\ gn & if sn = 1 \end{matrix}

Then the square

[figure: {0}; K; 2^{ℕ}; i; ℕ^{ℕ}]

commutes since 0 ∈ K and i0 = 0. It is a pullback since if Γ ⊢ is = h ∈ K then Γ, n : ℕ ⊢ isn < gn, so s = 0 and h = 0.

Hence the pullback (inverse image) of 0 ∈ U ⊂ K ⊂ ℕ^{ℕ} along i is 0 ∈ Σ^{i}U ⊂ {0} ⊂ 2^{ℕ}. But this means that {0} = Σ^{i}U ⊂ 2^{ℕ} is open, contradicting Corollary 4.7. □

Corollary 5.9 The pullback on the right is not definable.

[figure: ℕ; 1; ?; 1; ℕ_{⊥}; ∩; ∃; Σ; ⊤; (ℕ_{⊥})^{ℕ}; Σ^{ℕ}; ⊤]

Proof The idea is the same as in Proposition 3.17: if the pullback exists then it’s the exponential ℕ^{ℕ}, and vice versa.

The pullback on the left is the one that classifies ℕ as an open subspace of its lift, and in fact {} : ℕ → Σ^{ℕ} is the locally closed subspace classified by (D, ∃_{ℕ}) = (⊥, ⊤).

The functor (−)^{ℕ}, if it existed, would be right adjoint to (−) × ℕ, and so would preserve pullbacks. However, it is just as easy to check the universal properties on an individual basis. □

Remark 5.10 Finally, notice also that, if the map ℕ^{ℕ} → (ℕ_{⊥})^{ℕ} exists, it is a regular mono, but is not Σ-split. □

6 Kleene trees

This section is not part of the proof of Tychonov’s theorem, which we have already completed. It presents my early response to the doubts that Martín Escardó expressed concerning the compactness of Cantor space in ASD. It tries, as well as I was able, to bring the foregoing construction into direct conflict with his objections based on Kleene trees and the failure of König’s Lemma. For a better explanation of the latter, see [I, Section 12], Andrej Bauer’s work and elsewhere in the literature.

We must be careful with the so-called “universal quantifier” in our definition of compactness, as it does rather less than a naïve interpretation might suggest.

Remark 6.1 We start off by talking about programs, not values in ASD.

The programming language should be parallel. Success for results of type unit means termination, so there’s no issue of determinism, as termination of one branch of a parallel program is OK. However, a parallel program whose result type is bool must be accompanied by a proof that we don’t get 1 from one branch and 0 from the other, cf. Lemma 3.3.

We exclude programming languages that can report attempted accesses to the input. So there is no program P of type (unit → unit) → unit for which P (λx. x) terminates but P (λx. ⊤) doesn’t. Such programs have no denotational semantics in Scott-style domain theory, topology or ASD. (They do in stable domain theory or games semantics, but it is not the current objective of ASD to formalise those.)

Definition 6.2 A stream is a program of type nat → bool. It is called total if it terminates (with some deterministic boolean value) for any (terminating numerical) input, and partial otherwise.

Definition 6.3 A drain is a program that takes a stream as input, i.e. which has type (nat → bool) → unit. We call it

(a) superficial if it terminates straight away, without examining (any of the values from) its input stream;

(b) shallow if, for some fixed n that is valid for all streams, it examines (at least one but) at most the first n values from its input stream and then terminates in every one of the 2^{n} cases;

(c) deep if it terminates on any total stream that it may be given, but after examining an unbounded number of values;

(d) blocked if there is some total stream on which it fails to terminate.

Remark 6.4 We can test a drain by applying it to a single stream. More generally, we may apply some program of type

                           ((nat → bool) → unit) → unit

to the drain. This program may then apply the drain to some streams. Notice in particular that Escardó’s quantifier program Q is of this type.

Are the four types of drain distinguishable by such tests?

Plainly a blocked drain is (negatively) identifiable by applying it to some stream on which it fails to terminate, whereas any drain of the other three kinds always terminates when applied to a total stream.

Remark 6.5 The question of whether shallow drains can be distinguished from superficial ones depends on whether we can detect whether a program actually reads the input that it is given. This can be tested one way round by providing ⊥ as input (i.e. it never arrives); if the predicate still manages to terminate, that is because it never tried to access its input. By assumption on the programming language (Remark 6.1), a test the other way round is not possible. We see therefore that the superficial–shallow test can be made using partial streams but not total ones.

Remark 6.6 This leaves deep drains. The obvious answer is that they don’t exist. As the drain terminates on any given stream, it must have read only finitely many values from it. Regarding the stream as a path through the infinite binary tree, the moment of termination of the drain defines a pruning of the tree. Thus it has no infinite path. By König’s Lemma, the pruned tree is finite, and in particular of finite uniform depth, so the drain is shallow after all.

Even with this argument we must be careful. If one branch of a parallel drain terminates on a given total stream, the pruning of the tree is made at a point determined by the collection of input values that have so far been read by any of the branches. However, some different scheduling of the parallel branches may result in a different pruning.

Remark 6.7 In fact, König’s Lemma is no longer valid if the infinite paths are required to be computable, i.e. the output of some program. Indeed, there is a computably defined infinite binary tree in which every computable path is finite. We shall not attempt to describe the program, but take it on authority that there is indeed a deep drain (program) D.

By construction Ds terminates for any total stream s. This property distinguishes the deep drains from blocked ones.

However, when we apply the quantifier program Q of Remark 4.11 to D, the result QD does not terminate, because at no finite depth n do the 2^{n} cases suffice. This distinguishes deep drains from shallow ones, completing the proof of the

Proposition 6.8 Q classifies (i.e. terminates on exactly) superficial and shallow drains. However, QD does not answer the question “Ds↓ for every total stream s”. □

Remark 6.9 Now we turn to the denotational semantics of such programs in ASD. The full theory of Scott domains in ASD is set out in [F], but we only need the base types

[[unit]] ≡ 1_{⊥} = Σ, [[bool]] ≡ 2_{⊥} and [[nat]] ≡ ℕ_{⊥}

and a few exponentials. We should have [[nat → bool]] ≡ (2_{⊥})^{ℕ_{⊥}}, but the possibility that a stream program may terminate with some boolean value without ever reading its numerical input is just a distraction, so we put

[[nat → bool]] ≡ 2_{⊥}^{ℕ}, [[(nat → bool) → unit]] ≡ Σ^{2_{⊥}^{ℕ}}

and

[[((nat → bool) → unit) → unit]] ≡ Σ^{Σ^{2^{ℕ}_{⊥}}} .

When we restrict attention to total streams, we have the subspaces and quotients

2^{ℕ} ^{i} 2_{⊥}^{ℕ}, Σ^{2^{ℕ}}[figure: Σ^{i}; ⊥; R] Σ^{2_{⊥}^{ℕ}} and Σ^{Σ^{2^{ℕ}}} ^{Σ^{Σ^{i}}} Σ^{Σ^{2^{ℕ}_{⊥}}} ,

where the last two are actually retracts.

Remark 6.10 The composite of the denotational semantics in ASD [F] with the interpretation of ASD in classical topology agrees with the classical Scott–Plotkin denotational semantics of the language.

Either version of denotational semantics satisfies the following properties:

(a) for programs f : a → b and u : a, [[fu]] = [[f]][[u]] : [[b]];

(b) a program p : unit terminates iff [[p]] = ⊤ : Σ, where ⇒ by subject-reduction and induction on the execution path and ⇐ by Plotkin’s “logical relations” technique;

(c) [[Q]] = □. However, it is sufficient for the following argument to rely on these properties for classical Scott– Plotkin denotational semantics.

Remark 6.11

(a) The superficial drain has denotation λf. ⊤ in either Σ^{2_{⊥}^{ℕ}} or Σ^{2^{ℕ}}.

(b) A shallow drain S with depth n has denotation [[S]] ≥ λf. (∀m < n. fm↓) : Σ^{2_{⊥}^{ℕ}}, which becomes Σ^{i}[[S]] = λs. ⊤ : Σ^{2^{ℕ}} when restricted to total streams.

(c) Conversely, any program with this denotation is a shallow drain.

(d) The quantifier program Q terminates on any shallow drain S, so [[QS]] = ⊤ : Σ.

(e) It fails on any deep or blocked drain D or B, so [[QD]] = [[QB]] = ⊥ : Σ. □

Corollary 6.12 [[Q]] classifies {F | ∃n. · · ·} ⊂ Σ^{2_{⊥}^{ℕ}} and Σ^{i}[[Q]] classifies {⊤} ⊂ Σ^{2^{ℕ}}, so Σ^{i}[[Q]] = ∀_{2^{ℕ}} and [[Q]] = □. □

Corollary 6.13 [[D]] is not equal to ⊤ : Σ^{2^{ℕ}} in either ASD or classical Scott–Plotkin denotational semantics. □

Theorem 6.14 δ ≡ Σ^{i}[[D]] satisfies

{⊢ s : 2^{ℕ} \atop ⊢ δs = ⊤ : Σ}

but

⊬ δ = ⊤ : Σ^{2^{ℕ}} and s : 2^{ℕ} ⊬ δs = ⊤ : Σ.

In the first case, s is a definable closed term in ASD that is provably of type 2^{ℕ}; every such term is representable by a program in P CF^{++}. The line is not actually a direct deduction step, but means that a proof that s is well defined can be transformed (essentially by executing the program) into a proof of termination. In the second case, s is a variable. □

Remark 6.15 Apparently, this failure is traceable to that of König’s lemma. Maybe we could use cosmic rays or an antiprotonic computer to generate “arbitrary” streams (cf. [Esc04]), in particular the non-computable one required by the classical König’s lemma, for which D fails.

Indeed, we could extend PCF and its classical Scott–Plotkin semantics with a new functionsymbol f of type nat → bool, and β-rules corresponding to the stream provided by König’s lemma. Then Df would not terminate, so [[Df]] = [[D]][[f]] = ⊥ and [[D]] ≠ ⊤. □

Now, I don’t believe that cosmic rays are generated by a Turing machine. On the other hand, I do believe that some sort of super-Turing computation may someday be possible by clever use of Quantum Mechanics. When that day comes, I would expect to see Denotational Semantics and Abstract Stone Duality modified to accommodate it, but without changing the essence of these theories. (I understand that Recursion Theory will not need to be modified, since Quantum Computing does not extend the class of definable functions — it just claims to evaluate some of them much faster.) Indeed Gödel and Turing were well aware of these possibilities, or at least of their mathematical consequences. However, I see no reason why such 21st century methods should feel obliged to validate a 1928 theorem of classical Set Theory. Even if they do, they won’t make the problem above go away, because Gödel is the villain of the peace and not König.

Theorem 6.16 There is a program E of type nat → unit that terminates when applied to any numeral, but whose denotation ϵ ≡ [[E]] : Σ^{ℕ} in either ASD or classical Scott–Plotkin semantics is not λn. ⊤. That is,

{⊢ n : ℕ \atop ⊢ ϵn = ⊤ : Σ}

but

⊬ ϵ = ⊤ : Σ^{ℕ} and n : ℕ ⊬ ϵn = ⊤ : Σ.

Proof By Lemma 4.4 there are maps p : Kℕ × Kℕ → 2^{ℕ} and P : Σ^{Kℕ×Kℕ} → Σ^{2^{ℕ}} such that P · Σ^{p} = id. Essentially by using the binary expansion of a number, there is also an isomorphism u : ℕ ≅ Kℕ × Kℕ. Hence we have a retraction

⊤ ≠ δ ∈ Σ^{2^{ℕ}}[figure: Σ^{p·u}; \underline{P · Σ^{u^{−1}}}] Σ^{ℕ} ∋ ϵ

Then E ≡ λn. D(p(un)) terminates for every numeral, but ϵ ≠ ⊤. □

7 Overt closed subspaces

Theorem 7.1 Every overt closed subspace of 2^{ℕ} is either empty or a retract. Proof Let (ω, □, ♢) be a closed, compact, overt subspace of 2^{ℕ} in the notation of [J, Proposition 8.4]. By [J, Lemma 9.2], it is decidable whether this is empty, so we assume that it isn’t; this may be expressed by any of the equivalent statements

□ ⊥ ⇔ ⊥,  ♢ ⊤ ⇔ ⊤,  □ ≤ ♢,  □ ω ⇔ ⊥.

Given t : 2^{ℕ}, we shall construct a sequence s : 2^{ℕ}, which will be the value of the retract at t. The idea is that s_{n} := t_{n} if it can be, but s_{n} ≠ t_{n} if it must be, where the “possible worlds” are defined by all infinite sequences s that satisfy the requirements and extend the finite one that has been defined so far.

We switch notation for the modal operators, writing

ω_{0} ≡ ω,  A_{0} ≡ □ ≤ P_{0} ≡ ♢,  K_{0} ≡ K.

These will be the bases cases of recursive sequences

ω ≤ ω_{n} ≤ ω_{n+1}  ≤ ω_{∞} ≡ ∃n. ω_{n},
∀_{2^{ℕ}} ≤ □ ≡ A_{0} ≤ A_{n} ≤ A_{n+1} ≤ A_{∞} ≡ (∃n. A_{n})
≤ P_{m+1} ≤ P_{m} ≤ P_{0} ≡ ♢ ≤ ∃_{2^{ℕ}},

which define the nonempty, closed, compact, overt subspaces K_{n} with

K_{∞} ≡ ⋂_{n} K_{n} ⊂ K_{n+1} = {u : K_{n} | u_{n} = s_{n}} ⊂ K_{n} ⊂ 2^{ℕ},

where s_{n} is defined from t_{n} and K_{n}. Finally, we shall discover that K_{∞} = {s}.

By the mixed modal laws, the propositions P_{n}(λu. u_{n} = 0) and A_{n}(λu. u_{n} = 1) are complementary, as are P_{n}(λu. u_{n} = 1) and A_{n}(λu. u_{n} = 0), whilst since K_{n} is nonempty, A_{n}(λu. u_{n} = 0) ⇒ P_{n}(λu. u_{n} = 0) and A_{n}(λu. u_{n} = 1) ⇒ P_{n}(λu. u_{n} = 1).

Hence we have the following exhaustive analysis into four disjoint cases,

t_{n} A_{n}(λu. u_{n} = 0) P_{n}(λu. u_{n} = 0) A_{n}(λu. u_{n} = 1) P_{n}(λu. u_{n} = 1) s_{n}
0  ⊤^{=,♢}  ⊥^{□}  0
0  ⊥^{□} ⇒  ⊥  ⊤^{≠}  ⇒ ⊤^{♢}  1
1  ⊤^{≠}  ⇒ ⊤^{♢}  ⊥^{□} ⇒  ⊥  0
1  ⊥^{□}  ⊤^{=,♢}  1

where ⇒ indicates use of nonemptiness, the missing values being indeterminate but unimportant. The superscripts =, ≠, ♢ and □ indicate the relevant columns for each case in the next part of the argument.

Next, we assign values to s_{n} uniquely such that

(s_{n} = t_{n}) ⇔ P_{n}(λu. u_{n} = t_{n})  marked =
(s_{n} ≠ t_{n}) ⇔ A_{n}(λu. u_{n} ≠ t_{n})  marked ≠.

Using logical notation, this is

s_{n} ≡ 0 if P_{n}(λu. u_{n} = 0) ∧ (t_{n} = 0) ∨ A_{n}(λu. u_{n} = 0) ∧ (t_{n} = 1)
s_{n} ≡ 1 if P_{n}(λu. u_{n} = 1) ∧ (t_{n} = 1) ∨ A_{n}(λu. u_{n} = 1) ∧ (t_{n} = 0).

Now, the predicates ϕ ≡ λu. (u_{n} = s_{n}) and ψ ≡ λu. (u_{n} ≠ s_{n}) are complementary, so they define a clopen subspace of K_{n}. By [J, Lemma 10.4], this is compact and overt, with

ω_{n+1} ≡ λu. ω_{n}u ∨ (u_{n} ≠ s_{n})
A_{n+1} ≡ λθ. A_{n}(λu. θu ∨ u_{n} ≠ s_{n})
P_{n+1} ≡ λθ. P_{n}(λu. θu ∧ u_{n} = s_{n}).

It is nonempty because, cf. [J, Lemma 9.2],

P_{n+1}⊤ ≡ P_{n}(λu. u_{n} = s_{n}) ⇔ ⊤  marked ♢
A_{n+1}⊥ ≡ A_{n}(λu. u_{n} ≠ s_{n}) ⇔ ⊥  marked □,

so also A_{n+1} ≤ P_{n+1}. Hence, as claimed,

∀_{2^{ℕ}} ≤ A_{n} ≤ A_{n+1} ≤ (∃n. A_{n}) ≡ A_{∞} ≤ P_{m+1} ≤ P_{m} ≤ ∃_{2^{ℕ}}.

The formulae for the derived modal operators may be simplified a little,

A_{n}θ ⇔ □(λu. θu ∨ ∃m < n. u_{m} ≠ s_{m})
P_{n}θ ⇔ ♢(λu. θu ∧ ∀m < n. u_{m} = s_{m})
ω_{n}u ⇔ ωu ∨ ∃m < n. (u_{m} ≠ s_{m}),

although the sequence (s_{n}) was itself defined in terms of A_{n} and P_{n}.

Now we consider the joins ω_{∞} and A_{∞} of the increasing sequences ω_{n} and A_{n}. Using the componentwise characterisation of ≠ on 2^{ℕ},

ω_{∞}u ⟺ ωu ∨ ∃m. (u_{m} ≠ s_{m}) ⟺ ωu ∨ (u ≠ s).

This co-classifies the intersection of closed subspaces,

K_{∞} = K_{0} ∩ {s},

as we would expect from the construction.

Since each ω_{n} and A_{n} encode the same closed compact subspace as in [J, Theorem 6.8], and the relationship between such encodings is Scott continuous, ω_{∞} and A_{∞} are related in the same way, i.e.

A_{∞}θ ⟺ ∀u:2^{ℕ}. ω_{∞}u ∨ θu ⟺ ∀u. ωu ∨ (u ≠ s) ∨ θu ⟺ ωs ∨ θu.

Hence

A_{∞}(θ ∨ ϕ) ⟺ ωs ∨ θs ∨ ϕs ⟺ A_{∞}θ ∨ A_{∞}ϕ,

whilst

A_{∞}⊥ ⟺ ∃n. A_{n}⊥ ⟺ ⊥,

but A_{∞} already preserves ⊤ and ∧ since it is a necessity operator. By [G, ] it is therefore prime, i.e. of the form λθ. θr, but we must have r ≡ s. Hence

ω_{∞}u ⟺ (u ≠ s),  A_{∞}θ ⟺ θs,  K_{∞} = {s},

which is also overt, with P_{∞}θ ≡ θs.

Since the whole argument admits parameters (notwithstanding the case analyses), t may be a variable, and the construction t ↦ s defines a function 2^{ℕ} → K_{0} ⊂ 2^{ℕ}.

Now observe that

(s ≠ t) ⟺ ∃n. (∀m < n. s_{m} = t_{m}) ∧ (s_{n} ≠ t_{n}).

Then, with this n,

(s_{n} ≠ t_{n}) ⇔ A_{n}(λu. u_{n} ≠ t_{n})
⇔ □(λu. u_{n} ≠ t_{n} ∨ ∃m < n. u_{m} ≠ s_{m})
⇔ □(λu. u_{n} ≠ t_{n} ∨ ∃m < n. u_{m} ≠ t_{m})
⇔ □(λu. ∃m ≤ n. u_{m} ≠ t_{m}),
so (s ≠ t)  ⇒ ∃n. □(λu. ∃m ≤ n. u_{m} ≠ t_{m}),
⇔ □(λu. ∃n. ∃m ≤ n. u_{m} ≠ t_{m}),
⇔ □(λu. u ≠ t) ⟺ ωt,

since the join ∃n is directed.

Hence K_{0} is exactly the fixed subspace of the function t ↦ s, which is idempotent. □

Remark 7.2 Classically, a space X is called separable if it has a countable dense subsequence. Replacing “countable” by “recursively enumerable”, i.e. the image of an open subspace of ℕ classified by δ, we may define

♢ ϕ ≡ ∃n. ϕa_{n} ∨ δn,

and say that a space X in ASD is separable if ♢ is its existential quantifier. Any separable space is therefore overt.

Proposition 7.3 2^{ℕ} is separable. □

Proposition 7.4 The direct image of any separable space is separable. □

Corollary 7.5 Any overt compact subspace of 2^{ℕ} is separable. □

Remark 7.6 I conjecture that any overt subspace of 2^{ℕ} is separable, but this seems to be very difficult to prove. In locale theory, any subspace has a closure, and if the subspace is overt, its closure has the same possibility operator, to which the main Theorem is applicable. The same holds in ASD with the underlying set axiom.

Without the underlying set axiom, there may be overt subspaces that have no closure. For example, the codes of terminating programs form an overt subspace of ℕ that has no closure.

8 Canopies

In the axiomatisation of ASD, the “lower levels” (the monadic and Phoa principles) are exactly lattice-dual, and already provide a great deal of the structure of topology [A, B, C, D]. The duality has to break down somewhere, and indeed the remaining axioms (overtness and recursion over ℕ, and the Scott principle) are not lattice-dual.

Could there be a better lattice duality for even these two axioms?

• ℕ is the initial algebra for the functor 1 + (−); it is overt, discrete and Hausdorff;

• 2^{ℕ} is the final coalgebra (prove this!) for the functor 2 × (−); it is overt, compact and Hausdorff.

The following investigation is an attempt to find the corresponding dual Scott principle. In [G], the equivalence is proved amongst

• traditional formulations of local compactness for spaces, using open and compact subspaces;

• local compactness for locales, using continuous lattices;

• the basis expansion

ϕx ⟺ ∃n. A_{n}ϕ ∧ β^{n}x,

where the effective basis (β^{n}, A_{n}) is indexed by an overt discrete object N, where wlog N ≡ ℕ; and

• Σ-split subspaces of ℕ.

Since the phrase “dual basis” has already been used for the family (A_{n}), we need a new word for the concept in which the overt discrete space N is replaced in the last case by a compact Hausdorff space K.

We show in this section that X is a Σ-split subspace of Σ^{K} iff obeys a dual version of the basis expansion.

In the following two sections we show that every definable (locally compact) object X has a canopy, and also relate this notion to the Lawson topology on the continuous lattice of open subspaces of X.

Definition 8.1 An effective canopy for a space X is a pair of families

k : K ⊢ ω^{k} : Σ^{X} k : K ⊢ P_{k} : Σ^{Σ^{X}} ,

where K is a compact Hausdorff space, such that every ϕ : Σ^{X} has a canopy decomposition,

ϕ : Σ^{X}, x : X ⊢ ϕx ⟺ ∀k. P_{k}ϕ ∨ ω^{k}x.

Definition 8.2 An effective canopy (ω^{k}, P_{k}) is called

(a) a codirected or ∧-canopy if there is some element (that we call 1 ∈ K) such that

ω^{1} = λx. ⊤ and P_{1} = λϕ. ⊥

(though P_{1} = ⊥ ⇒ ω^{1} = ⊤ by Lemma 8.3) and a binary operation ⋆ : K × K → K such that

ω^{k⋆h} = ω^{k} ∧ ω^{h}  and  P_{k⋆h} = P_{k} ∨ P_{h};

(b) an ∨-canopy if ω^{0} = λx. ⊥ for some element (that we call 0 ∈ K), and there is a binary operation + such that

ω^{k+h} = ω^{k} ∨ ω^{h} P_{k} ≥ P_{k+h} and P_{h} ≥ P_{k+h},

(c) a lattice canopy if it is both ∨ and ∧;

(d) an ideal canopy if each P_{k} preserves ∨ and ⊥, and so defines an overt subspace N_{k};

(e) a prime canopy if each P_{k} of the form P_{k}ϕ ⇔ ϕp_{k} for some p_{k} : X, the corresponding overt subspace being N_{k} = {p_{k}}.

Lemma 8.3 If Γ ⊢ ϕ : Σ^{X} satisfies Γ ⊢ P_{k}ϕ ⇔ ⊥ then Γ ⊢ ω^{k} ≥ ϕ. Proof Since P_{k}ϕ ⇔ ⊥, the canopy decomposition for ϕ includes ω^{k} as a conjunct. □

Remark 8.4 Each pair (ω^{k}, P_{k}) therefore satisfies one direction of the rule for an overt closed subspace in [J, Definition 8.1], and also the relative instantiation rule [J, Proposition 8.2(c)],

ϕx ⇒ ω^{k}x ∨ P_{k}ϕ.

However, the other direction need not hold: the overt subspace defined by P_{k} need not be contained in the closed subspace co-classified by ω^{k}:

Lemma 8.5 If ⊢ P_{k}ω^{k} ⇔ ⊥ then ω^{k} co-classifies an overt closed subspace.

[figure: 1; 1; Σ^{N} = ω^{k} ↓ Σ^{X}; ω^{k}; Σ^{X}; P_{k}; Σ; ⊥]

Proof The equation P_{k}ω^{k} ⇔ ⊥ says that the square commutes. Any test map ϕ : Γ → ω^{k} ↓ Σ^{X} that (together with ! : Γ → 1) also makes a square commute must satisfy Γ ⊢ P_{k}ϕ ⇔ ⊥ and Γ ⊢ ϕ ≥ ω^{k}, but then ϕ = ω^{k} by the previous result. Hence the square is a pullback, whilst ω^{k} = ⊥_{Σ^{N}}, so the lower composite is ∃_{N}, making N overt. □

Corollary 8.6 If P_{0}⊥ ≡ P_{0}ω^{0} ⇔ ⊥ then the whole space is overt. □

Definition 8.7 i : X Y is a Σ-split subspace if (it is the equaliser of some pair [B] and) there is a map I : Σ^{X} → Σ^{Y} such that Σ^{i} · I = id_{Σ^{X}}.

[figure: X; i; × \underline{Î}; Y; Σ^{X}; \underline{Σ^{i}}; I; Σ^{Y}]

Lemma 8.8 Any object X that has an effective canopy (ω^{k}, P_{k}) indexed by K is a Σ-split subspace of Σ^{K}. Proof Using the canopy (ω^{k}, P_{k}), define

i : X → Σ^{K}  by x ↦ λk.ω^{k}x
I : Σ^{X} → Σ^{Σ^{K}} by ϕ ↦ λψ.∀k. P_{k}ϕ ∨ ψk.

Then Σ^{i}(Iϕ) = λx. (Iϕ)(ix) = λx. ∀k. P_{k}ϕ ∨ ω^{k}x = ϕ. □

Lemma 8.9 Let (ω^{k}, P_{k}) be an effective canopy for Y and i : X Y a Σ-split subspace. Then (Σ^{i}ω^{k}, Σ^{I}P_{k}) is an effective canopy for X. If an ∧- or ∨-canopy was given, the result is one too. If P_{k} is an ideal and I preserves ⊥ and ∨ (in particular if I ⊣ Σ^{i}) then Σ^{I}P_{k} is also an ideal. Proof For ϕ : Σ^{X}, Iϕ : Σ^{Y} has canopy decomposition

Iϕ ⇔ ∀k. P_{k}(Iϕ) ∨ ω^{k} ≡ ∀k. (Σ^{I}P_{k})ϕ ∨ ω^{k}.

Since Σ^{i} is a homomorphism, it preserves scalars, ∨ and ∀, so

ϕ = Σ^{i}(Iϕ) = Σ^{i}(∀k. P_{k}(Iϕ) ∨ ω^{k}) = ∀k. P_{k}(Iϕ) ∨ Σ^{i}ω^{k}.  □

Corollary 8.10 A space X has an effective canopy indexed by a compact Hausdorff space K iff X is a Σ-split subspace of Σ^{K}. □

9 Examples of canopies

Remark 9.1 Stone Spaces, Lemma VII 1.5: any Hausdorff topological semilattice (A, ∧) is order-Hausdorff. This is because the equaliser

[figure: (≤); A × A; ∧; π_{0}; A]

is targeted at a Hausdorff space, so is a closed subspace. Indeed,

(a ≤ b) ≡ (a ∧ b ≠ a) ⟺ (a ∨ b ≠ b).  □

Proposition 9.2 Assuming excluded middle, every locally compact locale or sober space has an ideal lattice canopy.

Proof Let K and Σ^{X} be respectively the (distributive continuous) lattice of opens of the locale equipped with the Lawson and Scott topologies, so K is the patch topology on Σ^{X}.

Then K is a compact Hausdorff topological lattice whose order relation ≤ is closed, and we have continuous functions β : K → Σ^{X} and (≰) : Σ^{X} × K → Σ. Use these to define

ω^{k} ≡ λx. (x ∈ βk) and P_{k} ≡ λϕ. (ϕ ≰ ω^{k}).

Plainly ω is a lattice homomorphism and A is contravariant, whilst

P_{1}ϕ ⇔ (ϕ ≰ ω^{1}) ⇔ ⊥ P_{k}⊥ ⇔ (⊥ ≰ ω^{k}) ⇔ ⊥
P_{k⋆h}ϕ ⇔ (ϕ ≰ ω^{k⋆h}) ⇔ (ϕ ≰ ω^{k} ∧ ω^{h}) ⇔ (ϕ ≰ ω^{k}) ∨ (ϕ ≰ ω^{h}) ⇔ P_{k}ϕ ∨ P_{h}ϕ
P_{k}(ϕ ∨ ψ) ⇔ (ϕ ∨ ψ ≰ ω^{k}) ⇔ (ϕ ≰ ω^{k}) ∨ (ψ ≰ ω^{k}) ⇔ P_{k}ϕ ∨ P_{k}ψ.

Finally, for the canopy expansion,

∀k. P_{k}ϕ ∨ ω^{k}x ⇔ ∀k. (ϕ ≰ ω^{k}) ∨ (x ∈ ω^{k}) ⇔ ∀k. (ϕ ≤ ω^{k} ⇒ x ∈ ω^{k}) ⇔ (x ∈ ϕ),

using ω^{k} = ϕ in the last step. □

Corollary 8.6 shows that this proof necessarily depends on classical locale theory. Nevertheless, we can translate the idea almost verbatim into examples that are valid in ASD. Even though β ≡ \overline{\{−\}} : K → Σ^{K} in Lemma 9.3 is not epi, still P_{k}ϕ ⇐ (ϕ ≰ ω^{k}).

Lemma 9.3 Any compact Hausdorff space K has a K-indexed prime canopy given by

ω^{k} ≡ \overline{\{k\}} ≡ λx. (x ≠_{K} k) and P_{k} ≡ η_{K}(k) ≡ λϕ. ϕk,

so the kth closed overt subspace is {k}. Proof ∀k. ηkϕ ∨ \overline{\{k\}}h ⇔ ∀k. ϕk ∨ (h ≠ k) ⇔ ϕh. □

Proposition 9.4 Let H be a compact Hausdorff space with effective canopy (ω^{k}, P_{k}) indexed by a compact Hausdorff space K. Then H is the subquotient of K by a closed partial equivalence relation. Proof Write k ⊩ x for k : K, x : H ⊢ P_{k}\overline{\{x\}} ∨ ω^{k}x (using Hausdorffness of H) and K′ = {k | ¬∀x. k ⊩ x} ⊂ K, which is closed, using compactness.

Then, using the canopy expansion of \overline{\{x\}},

x : H ⊢ ⊥ ⇔ (x ≠_{H} x) ⇔ \overline{\{x\}}(x) ⇔ ∀k. P_{k}\overline{\{x\}} ∨ ω^{k}x ⇔ ∀k. k ⊩ x,

so every point x : H has some code k : K′. The latter belongs only to x since

k ⊩ x ∨ k ⊩ y ⇔ P_{k}\overline{\{x\}} ∨ ω^{k}x ∨ P_{k}\overline{\{y\}} ∨ ω^{k}y
⇐ P_{k}\overline{\{x\}} ∨ ω^{k}y
⇐ (∀k. P_{k}\overline{\{x\}} ∨ ω^{k})y
⇔ \overline{\{x\}}y ⇔ (x ≠_{H} y).

Hence K′ → Σ^{H} by k ↦ λx. k ⊩ x factors through \overline{\{\}} : H Σ^{H}, and H is K′/∼ where h ∼ k iff ¬∀x. h ⊩ x ∨ k ⊩ x [C]. □

Corollary 9.5 In the free model, if X has a canopy indexed by any compact Hausdorff space H then it has one indexed by 2^{ℕ}. Proof Let k : 2^{ℕ}, h : H ⊢ k ⊩ h be the relation defined in the Proposition and (ω^{h}, P_{h}) the canopy on X. Define

γ^{k} = λx. ∀h. k ⊩ h ∨ ω^{h}x and D_{k} = λϕ. ∀h. k ⊩ h ∨ P_{h}ϕ

so γ^{k} = ω^{h} and D_{k} = P_{h} if k ⊩ h, but γ^{k} = ⊤ and D_{k} = ⊤ if k ∉ K′. Then, using the properties of ⊩,

∀k. D_{k}ϕ ∨ γ^{k}x ⇔ ∀khh′. k ⊩ h ∨ P_{h}ϕ ∨ k ⊩ h′ ∨ ω^{h′}x
⇔ ∀h. P_{h}ϕ ∨ ω^{h}x ⇔ ϕx

so (γ^{k}, D_{k}) is an effective canopy. □

Example 9.6 Σ^{K} has a Fin(K)-indexed prime ∨-canopy given by

B^{ℓ} ≡ λϕ. ∃h ∈ ℓ. ϕh and P_{ℓ} ≡ λF. F (λh. h ∈ ℓ),

because F ϕ ⇔ ∀ℓ. F (λh. h ∈ ℓ) ∨ ∃h ∈ ℓ. ϕh. □

Lemma 9.7 Let N be overt discrete Hausdorff, so any overt closed subspace of N is complemented and is determined by a function N → 2. Then K = 2^{N}, ω^{k} = λn. (kn = 1) and A^{k} = λϕ. ∃n. ϕn∧ (kn = 0) provide an ideal lattice canopy for N. Proof For the canopy expansion,

(∗) ≡ ∀k. P_{k}ϕ ∨ ω^{k}n ⇔ ∀k. (∃m. ϕm ∨ km = 0) ∨ (kn = 1).

Then ϕn ⇒ (∗) since ϕn ⇔ ϕn ∧ (kn = 0 ∨ kn = 1) ⇒ (∃m. ϕm ∧ km = 0) ∨ (kn = 1). Conversely, consider k ≡ (λm. if m = n then 0 else 1), so

(∗) ⇒ (∃m. ϕm ∧ km = 0) ∨ (kn = 1) ⇒ (∃m. ϕm ∧ m = n) ∨ (0 = 1) ⇔ ϕn.

This is an ideal lattice canopy for the same reasons as before. □

Remark 9.8 Canopy for an overt discrete space analoguous to base of compact Hausdorff space determined by a family of disjoint pairs (U^{k} ∩̸ V_{k}) of open subspaces.

This would be given by a family of pairs of open subspaces that cover: U_{k} ∪ V_{k} = X.

Remark 9.9 What interesting canopies are there on ℝ?

10 Existence of canopies

It remains to show that every definable (locally compact) object has a canopy. However, since we know from [G] that every such object is a Σ-split subspace of Σ^{ℕ}, and that such subspaces inherit canopies, it is enough to construct a canopy on Σ^{ℕ}.

We assume the Scott principle, which provides various bases for Σ^{N}.

Proposition 10.1 Let N be overt discrete Hausforff. Then Σ^{N} has an ideal lattice canopy indexed by K ≡ Mono(KN, 2), whose lattice structure is inherited pointwise from that on 2.

Proof For k : K ⊂ 2^{KN}, ϕ : Σ^{N} and F : Σ^{Σ^{N}} define

B^{k}ϕ ≡ ∃ℓ. (∀n ∈ ℓ. ϕn) ∧ (kℓ = 1)
P_{k}F ⇔ ∃ℓ. F (λn. n ∈ ℓ) ∧ (kℓ = 0)

Again P_{k}F ⇔ (F ≰ B^{k}): since B^{k}(λn. n ∈ ℓ) ⇔ (kℓ = 1) is decidable, P_{k}F ⇔ ∃ℓ. F (λn. n ∈ ℓ) ∧ ¬B^{k}(λn. n ∈ ℓ).

To prove F ϕ ⇒ ∀k. P_{k}F ∨ B^{k}ϕ, recall the ∧-basis expansion

F ϕ ⇔ ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕn,

so we must show, for k : K and ℓ : KN,

F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕn ⇒ P_{k}F ∨ B^{k}ϕ,

but the first disjunct holds if kℓ = 0 and the second if kℓ = 1.

Conversely, we use the lattice basis indexed by L : K(KN).

F ϕ  ⇔ ∃L. D_{L}F ∧ C^{L}ϕ
C^{L}ψ  ⇔ ∃ℓ ∈ L. ∀n ∈ ℓ. ψm
D_{L}G  ⇔ ∀ℓ ∈ L. G(λn. n ∈ ℓ)
∀k. P_{k}F ∨ B^{k}ϕ ⇔ ∀k. P_{k}(∃L. D_{L}F ∧ C^{L}) ∨ B^{k}ϕ
⇔ ∃L. D_{L}F ∧ ∀k. (P_{k}C^{L} ∨ B^{k}ϕ) ⇔ (∗)

since ∃L is directed. Now, for each L : K(KN) and ℓ : KN consider

k_{L}ℓ ≡ \{ \begin{matrix}1 & if ∃ℓ′ ∈ L. ℓ′ ⊂ ℓ \\ 0 & if ∀ℓ′ ∈ L. ℓ′ ⊄ ℓ \end{matrix}

so k_{L} : K and

C_{L}(λn. n ∈ ℓ) ⇔ (∃ℓ′ ∈ L. ∀n ∈ ℓ′. n ∈ ℓ)
⇔ (∃ℓ′ ∈ L. ℓ′ ⊂ L) ⇔ (k_{L}ℓ = 1)
P_{k_{L}}C^{L}  ⇔ ∃ℓ. C_{L}(λn. n ∈ ℓ) ∧ (k_{L}ℓ = 0) ⇔ ⊥
Ω^{k_{L}}ϕ  ⇔ ∃ℓ. (∀n ∈ ℓ. ϕn) ∧ (∃ℓ′ ∈ L. ℓ′ ⊂ ℓ)
⇔ ∃ℓ′ ∈ L. ∀n ∈ ℓ. ϕn ⇔ C^{L}ϕ
(∗)  ⇒ ∃L. D_{L}F ∧ (P_{k_{L}}C^{L} ∨ B^{k}ϕ)
⇔ ∃L. D_{L}F ∧ B^{k}ϕ ⇔ F ϕ

Finally we show that (B^{k}, P_{k}) is an ideal lattice canopy.

B^{1}ϕ  ⇔ ∃ℓ. (∀m ∈ ℓ. ϕm) ∧ (1 = 1) ⇐ (∀m ∈ 0. ϕm) ⇔ ⊤
B^{0}ϕ  ⇔ ∃ℓ. (∀m ∈ ℓ. ϕm) ∧ (0 = 1) ⇔ ⊥
P_{1}F  ⇔ ∃ℓ. F (λm. m ∈ ℓ) ∧ (1 = 0) ⇔ ⊥
P_{k}⊥  ⇔ ∃ℓ. ⊥(λm. m ∈ ℓ) ∧ (kℓ = 0) ⇔ ⊥
B^{k⋆h}ϕ  ⇔ ∃ℓ. (∀m ∈ ℓ. ϕm) ∧ (kℓ = hℓ = 1)
⇒ (∃ℓ′. (∀m ∈ ℓ′. ϕm) ∧ (kℓ′ = 1)) ∧ (∃ℓ′′. (∀m ∈ ℓ′′. ϕm) ∧ (hℓ′′ = 1))
⇔ B^{k}ϕ ∧ B^{h}ϕ  with ⇐ by ℓ ≡ ℓ′ + ℓ′′
B^{k+h}ϕ  ⇔ ∃ℓ. (∀m ∈ ℓ. ϕm) ∨ ((kℓ = 1) ∨ (hℓ = 1))
⇔ (∃ℓ′. (∀m ∈ ℓ′. ϕm) ∧ (kℓ′ = 1)) ∨ (∃ℓ′′. (∀m ∈ ℓ′′. ϕm) ∧ (hℓ′′ = 1))
⇔ B^{k}ϕ ∨ B^{h}ϕ
P_{k}(F ∨ G) ⇔ ∃ℓ. (F ∨ G)(λm. m ∈ ℓ) ∧ (kℓ = 0)
⇔ (∃ℓ′. F (λm. m ∈ ℓ′) ∧ (kℓ′ = 0)) ∨ (∃ℓ′′. G(λm. m ∈ ℓ′′) ∧ (kℓ′′ = 0))
⇔ P_{k}F ∨ P_{k}G
P_{k⋆h}F  ⇔ ∃ℓ. F (λn. n ∈ ℓ) ∧ (kℓ = 0 ∨ hℓ = 0)
⇔ P_{k}F ∨ P_{h}F  □

Remark 10.2 (P_{(−)}, B^{(−)}) : Mono(KN, 2) ↣ Σ^{3}N ×Σ^{2}N is the composite of the representations Mono(KN, 2) ↣ Σ^{KN} × Σ^{KN} and KN ↣ Σ^{Σ^{N}} × Σ^{N} without the parts that are redundant owing to co- or contravariance.

Theorem 10.3 Every definable (locally compact) object has a canopy indexed by 2^{ℕ}. □

Corollary 10.4 Every definable compact Hausdorff space is a subquotient of 2^{ℕ} by a closed partial equivalence relation. □

References

[Esc04] Martín Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004.

[Tay86] Paul Taylor. Recursive Domains, Indexed category Theory and Polymorphism. PhD thesis, Cambridge University, 1986.

[Tay87] Paul Taylor. Homomorphisms, bilimits and saturated domains — some very basic domain theory. 1987.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Wei00] Klaus Weihrauch. Computable Analysis. Springer, Berlin, 2000.

The papers on abstract Stone duality may be obtained from

                            www.cs.man.ac.uk/∼pt/ASD

[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300–366, 2002.

[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[D] Paul Taylor, Non-Artin gluing in recursion theory and lifting in abstract Stone duality. 2000.

[E] Paul Taylor, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Electronic Notes in Theoretical Computer Science 416, Elsevier, 2005.

[F] Paul Taylor, Scott domains in abstract Stone duality. March 2002. [G–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone

duality. Electronic Notes in Theoretical Computer Science 69, Elsevier, 2003.

[G] Paul Taylor, Computably based locally compact spaces. Logical Methods in Computer Science, 2005, to appear.

[H-] Paul Taylor, An elementary theory of the category of locally compact locales.

APPSEM Workshop, Nottingham, March 2003.

[H] Paul Taylor, An elementary theory of various categories of spaces and locales. November 2004.

[I] Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. Computability and Complexity in Analysis, Kyoto, August 2005.

[J] Paul Taylor, A λ-calculus for real analysis. Computability and Complexity in Analysis, Kyoto, August 2005.

[K] Paul Taylor, Interval analysis without intervals. February 2006.