Inside every model of Abstract Stone Duality lies an Arithmetic Universe

Paul Taylor

8 May 2005

Abstract The first paper published on Abstract Stone Duality showed that the overt discrete objects (those admitting ∃ and = internally) form a pretopos, i.e. a category with finite limits, stable disjoint coproducts and stable effective quotients of equivalence relations. Using an ℕ-indexed least fixed point axiom, here we show that this full subcategory is an arithmetic universe, having a free semilattice (“collection of Kuratowski-finite subsets”) and a free monoid (“collection of lists”) on any overt discrete object. Each finite subset is represented by its pair (□, ♢) of modal operators, although a tight correspondence with these depends on a stronger Scottcontinuity axiom. Topologically, such subsets are both compact and open and also involve proper open maps. In applications of ASD this can eliminate lists in favour of a continuationpassing interpretation.

Contents  6. Admissible implies modal  17
1. Introduction  1  7. K as a functor  18
2. Proofs and natural numbers  4  8. Lists, heads and tails  21
3. Finite subsets as modalities  8  9. Recursion over lists  24
4. Fixed point properties  12  10. The free semilattice  28
5. Stages in the construction  14  11. Overt compact subspaces  30

1 Introduction

In Abstract Stone Duality the topology on a space X is treated as an exponential Σ^{X} with a λ-calculus rather than as a lattice with arbitrary joins. This has given accounts of the category of locally compact spaces, both over an elementary topos [H], and for a logic in which the maps ℕ → ℕ are precisely the provably total general recursive functions [G].

Remark 1.1 It is an important feature of ASD that its spaces do not have “underlying sets” of points — or even of open subspaces, as in locale theory. ASD is a direct axiomatisation of the category S of “spaces”, amongst which the “discrete” ones serve in the role of “sets”. However, as we take the word discrete to mean that there is an internal notion of equality, (=_{X}) : X × X → Σ (i.e. the diagonal X ⊂ X × X is open), we actually say overt discrete, meaning that there is also an “existential quantifier”, ∃_{X} : Σ^{X} → Σ.

Remark 1.2 Having postulated a notion of the category of “sets” in this roundabout fashion, i.e. as the full subcategory E of overt discrete types in a certain λ-calculus, we are faced with the challenge of showing that it has enough of the usual features of set theory or categorical logic to warrant the name, as none of these went in as ingredients. In fact, E is a topos if we assume the existence of “underlying sets”, i.e. a right adjoint to the inclusion E ↪ S [H], so it is important not to make such an assumption if we want to develop a computational axiomatisation of topology.

Giraud’s theorem, which characterised Grothendieck toposes in terms of the limits and (infinitary) colimits that they admit, suggested the first categorical approximation to the “finitary” aspects of the category of sets: a pretopos is a category with finite limits, stable disjoint coproducts and stable effective quotients of equivalence relations. Then André Joyal introduced arithmetic universes to prove Gödel’s incompleteness theorem in a categorical style: they have just enough structure to form the free internal thing of the same kind. Specifically, an arithmetic universe is a pretopos with free internal monoids (ListX), from which the free internal arithmetic universe can be obtained by means of generators and relations.

Actually, these structures are just what is taught in a first year “discrete math” course intended for computer scientists, i.e. one in which only the collection of listable subsets is considered, instead of a full set-theoretic powerset. We shall argue in future work (on the construction of S from E) that the other substitutes for the powerset, i.e. the collections of recursively enumerable and of decidable subsets of X, are the non-discrete spaces Σ^{X} and 2^{X}. If Σ^{X} had an underlying set, this would be the usual powerset of X.

Remark 1.3 Unfortunately, despite their 30-year history, knowledge of arithmetic universes circulates literally by word of mouth. The only only refereed (or even obtainable) papers on them are those by Maria Emilia Maietti, who provided a Martin-Löf-style type theory for them [6]. She claims that her notion of arithmetic universe [7] is stronger than that used here. Indeed, some disagreement over detail is known by those who have worked with arithmetic universes — but they hardly help matters by failing to write any papers. However, the best way to settle doubts over correct definitions in mathematics is to prove their equivalence with other structures that come from other intuitions. The construction in this paper of an arithmetic universe from a model of ASD and the proposed converse will, I believe, not only serve this purpose, but also provide a more expressive calculus than Maietti’s, allowing domain-theoretic methods to be used to define structures within arithmetic universes more fluently.

Remark 1.4 In ASD the full subcategory of overt discrete objects is already known to be a pretopos [C], so the present work is concerned with the free monoid and the free semilattice (KX).

Note, however, that, as an existential question, this is redundant in the two cases on which we usually focus: in the classical models (the source of our intuitions) E is a topos, whilst in the free one (the target of our computations) every object of E is a subquotient of ℕ by an open partial equivalence relation; in both cases lists can be encoded in well known ways.

This paper is also arguably unnecessary from a topological point of view, in that the existence of the free monoid could reasonably be taken as another axiom, so our conclusion is merely that this axiom is redundant.

Nevertheless, ASD sets itself apart from other approaches to topology by having a freestanding (technically) elementary axiomatisation that does not rely on a pre-existing category of sets or spaces. The intention is to use this as a route to computation, so our representation of KX is of interest even when we already know abstractly that it exists.

Remark 1.5 The two semilattice structures that we use most often are ∧ and ∨ in powers of Σ, and it turns out that these are jointly faithful, indeed that KX is a subspace of Ω ≡ Σ^{Σ^{X}} × Σ^{Σ^{X}}, where each finite subset ℓ is represented by the two modal operators,

[ℓ] ≡ λϕ. ∀x ∈ ℓ. ϕx and ⟨ℓ⟩ ≡ λϕ. ∃x ∈ ℓ. ϕx.

It is well known that modal logic is related to the three powerdomains, in one of which the inclusion order agrees with the intrinsic one, in another they are contravariant, whilst in the third inclusion inclusion involves both the intrinsic order and its opposite [4, 9, 10]. However, we only consider the convex powerdomain of an (overt) discrete space. The reason for this lack of ambition is that this paper forms part of the “bootstrapping” of the theory of ASD: much more can be done using the whole thing, in particular [G]; the analogous structure in an Hausdorff space such as ℝ is considered in [I]. Also, we represent elements of the powerdomain by modal operators, whereas the works cited use them to generate its topology, relying on the prior existence of the free semilattice.

Remark 1.6 Our translation of finite subsets into higher order λ-terms may be of computational value, like other examples of the continuation passing style. The theory of locally compact spaces is developed in [G] using bases of open and compact subspaces, and that paper concludes with a sketch of how continuous functions (for example ℝ → ℝ) might be manipulated computationally using relations. Unfortunately, at least as the theory is expressed there, such bases have to be indexed by (finitary) lattices, and heavy use is made of the free distributive lattice generated by an overt discrete object. This may be constructed via the free semilattice, whose elements might in turn be represented as lists, but possibly at quite a heavy computational cost.

On the other hand, as functional programmers know very well, there are plenty of situations in which (nested) lists provide excellent data structures. For this, it would be absurd to take a diversion via logic, especially by means of the construction that we use in Sections 8–9. What this paper provides, therefore, is a choice between lists (as traditionally implemented) and a mathematically isomorphic structure that encodes finite subsets using modal logic, λ-calculus and continuation-passing. Empirical study will be needed to make this choice in particular applications.

Remark 1.7 Returning to type theory, the disagreement with Maietti regarding the definition of an arithmetic universe appears to concern parametric list types, which are not covered in this paper. Certainly these are needed, but there are ways of obtaining them without first developing dependent spaces in general.

A family of overt discrete objects indexed by another such object is given, as in a topos, by any map δ : X → N, where X[n] ≡ δ^{−1}(n). (We call δ the “display” map [8, Chapter VIII].) Then ListX[n] is given by the display N + P → N, where

P  \overline{}N

[figure: ListX; Listδ; ListN; KN; \begin{matrix}\{ \\ | & − & | \\ \} \end{matrix}]

provides the non-empty lists and the extra term N the empty ones.

Remark 1.8 Another connection between our construction and domain theory is that it uses the methods of that subject. Specifically, the ASD calculus provides for the introduction of subtypes of a given ambient type Ω, defined by an endomorphism E of Σ^{Ω}. In this paper we obtain that endomorphism as the least fixed point of an operator $ of yet higher type.

To do this, a fixed point axiom must be added to what [C] used to show that E is a pretopos. To construct KX and ListX it is enough to assume

Axiom 1.9 The “linear countable” fixed point axiom is

Γ, n : ℕ ⊢ ϕn : Σ^{U} Γ, n : ℕ ⊢ ϕn ≤ ϕ(n + 1) : Σ^{U}
Γ, F : Σ^{U} → Σ^{V} ⊢ F (∃n. ϕn) = ∃n. F (ϕn) : Σ^{V}

However, in order to obtain all of the topological results that we expect [G], and in particular to show that every pair (□, ♢) of operators satisfying the modal laws actually corresponds to a listable subset(Section 11), the following stronger^{1} assumption is needed. Despite the conceptual simplification that it would bring throughout this paper, we are unable even to state it before proving our main result, as it involves either ListX or KX.

1The fixed point axiom says that F preserves countable directed joins, but in the classical models uncountable directed joins are also needed. Recall, for example, that in universal algebra the free functor for a theory of infinite arity κ preserves κ-filtered colimits of diagrams of any size λ. The two versions of our axiom correspond very roughly to the roles of these two cardinal parameters in the classical case.

Axiom 1.10 The Scott-continuity axiom is

Γ, ℓ : KX ⊢ ϕ^{ℓ} : Σ^{U} Γ, ℓ_{1}, ℓ_{2} : KX ⊢ ϕ^{ℓ_{1}} ∨ ϕ^{ℓ_{2}} ≤ ϕ^{ℓ_{1}+ℓ_{2}}
Γ, ℓ : KX ⊢ α_{ℓ} : Σ Γ ⊢ α_{nil} = ⊤ Γ, ℓ_{1}, ℓ_{2} : KX ⊢ α_{ℓ_{1}+ℓ_{2}} = α_{ℓ_{1}} ∧ α_{ℓ_{2}}
Γ, F : Σ^{U} → Σ^{V} ⊢ F (∃ℓ. α_{ℓ} ∧ ϕ^{ℓ}) = ∃ℓ. α_{ℓ} ∧ F ϕ^{ℓ}.

A family (α_{ℓ}, ϕ^{ℓ}) satisfying the five premises is called a directed diagram. In the free model every overt discrete object such as KX is a subquotient of ℕ; in this case general Scott-continuity may be derived from the fixed point axiom above. In other models, such as the classical ones, a Scott-continuity axiom is needed for each overt discrete object X.

Remark 1.11 This brings us back to the study of general models of ASD (for which the existential question about KX and ListX is not trivial). Besides the free and classical ones, we may obtain other models by strengthening the axioms with more ways of forming types, terms or equations. For example, the “underlying set” is a new type [H]. An oracle for termination would say that the (already definable) space T̄ of codes for non-terminating programs is overt, providing a new term ∃T̄ : ΣT̄ → Σ.

The very meaning of the assertions that we made in the opening paragraph depends on what we can prove about equality of terms. A morphism of the category is a class of terms that are provably equivalent according to a certain logic, whilst a partial morphism f : ℕ ⇀ ℕ is total by definition iff there is a proof that Σ^{f} satisfies a certain equation [D]. Since the definitions of prime and nucleus [A, B] depend on equations, if the logic proves more of them then it also defines more terms and (sub)types.

What counts as a legitimate proof (in particular of the equality of two terms) is an issue that we have to consider more carefully in this paper than has been done hitherto in the ASD literature, because this is the first serious use that we have made of recursion and induction over ℕ. That is the subject of the next section.

Section 3 gives the intuition and notation for the construction of KX and its modal logic, which are developed in Sections 4–6. Section 7 considers the properties of K as a functor. The universal property of KX as the free semilattice is, however, only proved in Section 10, being derived from that for ListX, which we construct in Sections 8–9. Section 11 reconsiders the sense in which KX is a finite powerset.

2 Proofs and natural numbers in ASD

Before we begin the construction of the free monoid and semilattice, we have to consider the form of proofs in the λ-calculus for ASD more carefully than has been done in previous papers. Nevertheless, our purpose is a domain-theoretic construction, not a proof-theoretic analysis of ASD, so we shall not give the complete set of rules. See in particular [B, §8] for a summary of the λ-calculus for {X | E} that handles the monadic property.

The main issue to be considered is induction over ℕ, the point being that the definition of the natural numbers object is not adequate as it is usually given. It is well known that an object Γ of parameters has to be added explicitly to the definition when we work in a category that is not cartesian closed. Similarly, equational hypotheses have to be considered explicitly when the category does not have all equalisers.

Axiom 2.1 The λ-calculus for ASD consists of types, terms and equations. Its judgements assert that

• types such as 0, 1, ℕ, Σ, X × Y, Σ^{X} and {X | E} are well formed,

• terms are well formed and of particular types, or

• equations hold between terms. Such judgements about terms and equations are made in certain contexts, i.e. on the assumption that their free variables have certain types.

However, even though the definition of the subtype {X | E} involves the term E, we insist (as the theory is currently formulated) that it be formed in the empty (global) context, i.e. without free variables. Even the pure syntax of dependent type theories is very complicated, and becomes more so in a semantic situation, where we have to choose a class of display maps [8, Chapter VIII]. Of course, we must also perform the semantic calculations, which form the main task of this paper. Families of overt and compact objects are encoded as open and proper maps respectively [C, §7].

Judgements are therefore of the four forms

⊢ X type,  Γ ⊢ a : X,  Γ ⊢ a = b : X and Γ ⊢ α ≤ β : X.

The last of these arises from the lattice structure on types of the form Σ^{U}, where (α ≤ β) means α = (α ∧ β) or β = (α ∨ β). The order can be extended to other objects, but we shall not need that.

In this paper we find that equations (and inequalities) are also needed as assumptions. In other words, the context Γ may include equations and inequalities between terms, as well as a list of typed variables. Any provable judgement attests to the validity of a certain fragment of reasoning from its hypotheses to its conclusions, so, as we want to form bigger arguments by concatenating such fragments (i.e. by means of a cut rule), all forms of assertion that are allowed as conclusions should also be allowed as hypotheses. In particular this is needed for induction over ℕ, which internalises the process of concatenation. (Adding such hypotheses to Martin-Löf type theory leads to undecidability [2, §3.2], but the ASD calculus is Turing-complete by design anyway.)

Axiom 2.2 Terms of type Σ may be seen as predicates in coherent logic:

(a) ⊤ and ⊥;

(b) α ∧ β and α ∨ β, where α, β : Σ;

(c) ϕa, where ϕ : Σ^{X} and a : X;

(d) (a =_{X} b), where a, b : X, and X is discrete (such as ℕ but not ℝ or 2^{ℕ});

(e) (a ≠_{X} b), where X is a Hausdorff type (such as ℕ, ℝ or 2^{ℕ});

(f) ∃_{X}ϕ ≡ ∃x. ϕx, where ϕ : Σ^{X} and X is an overt type (ℕ, ℝ, 2^{ℕ});

(g) ∀_{X}ϕ ≡ ∀x. ϕx, where ϕ : Σ^{X} and X is a compact type (such as [0, 1] ⊂ ℝ or 2^{ℕ} but not ℕ). We shall find that a type X has all four properties (d–g) iff it is finite, whilst it is Kuratowski-finite iff it has properties (d,f,g), that notion being the main subject of this paper. Terms of type ϕ : Σ^{X} are formed with a λ-calculus. As usual, the introduction of λx, ∃x or ∀x discharges the variable from the context, which must therefore contain no equational assumption in which x is free.

Remark 2.3 Notice that this logic does not include implication. Indeed, every term is monotone considered as a function of its free variables of type Σ^{U}. But a strictly limited form of implication is allowed in that assumptions and conclusions of judgements may be of the form α ≤ β : Σ^{U}, so judgements may be of the form

…, α ≤ β : Σ^{U}, … ⊢ γ ≤ δ : Σ^{V} ,

which means (∀u. αu ⇒ βu) ⇒ (∀v. γv ⇒ δv) in traditional notation.

When we need to make an assertion α that is a term of type Σ, we shall often follow mathematical idiom by saying simply “α” alone; by this we mean the judgement Γ ⊢ α = ⊤ : Σ, where the context Γ has been established implicitly in the argument.

Of course, any equation or inequality that is an assumption may be used directly as the conclusion of an “identity” or “axiom” judgement, or may be discharged by a “cut” rule. They are also discharged by logical rules that we now give.

Axiom 2.4 Even though we cannot define a term α ⇒ β of type Σ, the usual rule for it does introduce an inequality, in both an intuitionistic way and an apparently classical one:

{Γ, α = ⊤ : Σ ⊢ β = ⊤ : Σ \atop Γ ⊢ α ≤ β : Σ}  {Γ, α = ⊥ : Σ ⊢ β = ⊥ : Σ \atop Γ ⊢ α ≥ β : Σ}

The intuitionistic rule is equivalent to the Euclidean principle,

F : Σ^{Σ}, α : Σ ⊢ α ∧ F α = α ∧ F ⊤,

and the other rule to its lattice dual. Writing α and ¬β for α = ⊤ and β = ⊥, together they yield rules similar to those for negation in Gerhard Gentzen’s classical sequent calculus.

They and monotonicity are together equivalent to the Phoa principle,

F : Σ^{Σ}, α : Σ ⊢ F α = F ⊥ ∨ α ∧ F ⊤.

Note that these things are valid in intuitionistic locale theory [C, Section 5]. The Euclidean principle is equivalent (in the context of the monadicity assumption) to saying that ⊤ : Σ classifies a certain class of monos in S, which we call open, whilst its dual says that ⊥ : Σ classifies closed inclusions.

An example of the first principle that’s obvious in the abstract but may look strange when it’s used in practice is the rule (where X and Y are discrete)

{Γ, a = b : X ⊢ c = d : Y \atop Γ ⊢ (a =_{X} b) ≤ (c =_{Y} d) : Σ}  □

Turning to recursion and induction, we have to reconsider the definition of ℕ in a category without equalisers, such as that of locally compact spaces. See also [1] and [5, §II.4].

Axiom 2.5 The recursion scheme introduces terms of any type X, dependent on n : ℕ:

{Γ ⊢ z : X Γ, n : ℕ, x : X ⊢ s(n, x) : X \atop Γ, n : ℕ ⊢ rec(n, z, s) : X}

Its meaning is given by the β-rules

Γ  ⊢ rec(0, z, s) = z : X
Γ, n : ℕ ⊢ rec(n + 1, z, s) = s(n, rec(n, z, s)).

This is called recursion at type X, the point being that as the class of types at which the recursion scheme is asserted grows, so considerably does the power of the logic.

The corresponding diagrammatic property is

[figure: Γ; 0; Γ × ℕ; id × succ; Γ × ℕ]

[figure: z]

[figure: X; rec; . . . . . . . . . . . . . . . . .; s; Γ × ℕ × X.; (id, rec); . . . . . . . . . . . . . . . . .]

If the category is cartesian closed then this diagram may be rewritten with ℕ × X^{Γ} in place of X, the object Γ itself being removed from the top line. Symbolically, this means that the parameters can be embedded in both the data and the new term by means of λ-abstraction. If, as in ASD, the category (has finite products but) is not cartesian closed then the object Γ of parameters is needed.

Axiom 2.6 The equational induction scheme for Γ, n : ℕ ⊢ a_{n}, b_{n} : X:

{Γ ⊢ a_{0} = b_{0} : X Γ, n : ℕ, a_{n} = b_{n} : X ⊢ a_{n+1} = b_{n+1} : X \atop Γ, n : ℕ ⊢ a_{n} = b_{n} : X}

Notice that this says nothing about where a_{n} and b_{n} themselves came from. If they had been defined by the same base and step data on X, an η-rule or uniqueness hypothesis in the recursion scheme above would have made them equal. However, the scheme is more general than that: the term a_{n} need not arise directly from recursion, but may perhaps be of the form f(rec(n, z, s)) where f is some function, whilst b_{n} is some unrelated f′(rec(n, z′, s′)).

Remark 2.7 Just as the generalisation with parameters was redundant in a cartesian closed category, so the equational induction scheme can be derived from the usual universal property of ℕ when the category has equalisers:

E ≡ {(γ, n) | a_{n}(γ) = b_{n}(γ) : X} Γ × ℕ [figure: a_{n}; b_{n}] X.

The base case says that (id, 0) : Γ → Γ × ℕ factors through E, whilst the induction step says that id × succ restricts to a map E → E. Then Axiom 2.5 provides

rec_{E} : Γ × ℕ → E.

This is inverse to the inclusion, one equation being given by uniqueness of

rec_{ℕ} : Γ × ℕ → Γ × ℕ

and the other by the fact that E ↣ Γ × ℕ is mono. □

The equational induction scheme (and its equivalent version for inequalities α_{n} ≤ β_{n}) will be used in Propositions 4.4, 4.12, 5.9 and 7.10, and we shall deduce its analogue for lists and finite subsets in Propositions 9.7 and 10.11. It ought to have been stated as [A, Remark 2.5], since it was actually used in [A, Lemmas 8.9 and 9.6] and [B, Lemma 8.14].

Since the proof given for [A, 9.6] was sketchy and contained other errors, we give the correct version here by way of an example of equational induction. It turns recursion at type ℕ into recursion at type Σ^{ℕ}, as part of the process of bringing descriptions (the m.) to the outside of a term.

Lemma 2.8 Γ ⊢ rn ≡ rec(n, z, λn′u. s(n′, u)) = the m. ρ(n, m), where

ζ  ≡ (λm. m = z),
σ(n, ϕ) ≡ (λm. ∃m′. ϕm′ ∧ m = s(n, m′))
ρ(n, m) ≡ rec(n, ζ, σ)m.

Proof The base case (in context Γ) is

λm. ρ(0, m) ≡ λm. rec(0, ζ, σ)m = λm. ζm  β-rule
≡ λm. (m = z)  def ζ
= λm. (m = r0)  β-rule

The induction step, with the hypothesis λm′. ρ(n, m′) = λm′. (m = rn′), is

λm. ρ(n + 1, m) ≡ λm. rec(n + 1, ζ, σ)m
= λm. σ(n, rec(n, ζ, σ))m  β-rule
= λm. ∃m′. rec(n, ζ, σ)m′ ∧ (m = s(n, m′))  def σ
≡ λm. ∃m′. ρ(n, m′) ∧ (m = s(n, m′))
= λm. ∃m′. (m′ = rn) ∧ (m = s(n, m′))  hypothesis
= λm. (m = s(n, rn))  equality rules
= λm. (m = r(n + 1))  β-rule

So Γ, n : ℕ ⊢ λm. ρ(n, m) = λm. (m = rn) : Σ by Axiom 2.6. □

Remark 2.9 Recall from [B, Section 8] that the rules for the introduction of focus and admit terms have equational premises. This now means that there are such terms that are only defined in certain contexts that contain particular equational assumptions.

Recall, however, from op. cit. that, for any term Γ ⊢ α : Σ, there is another term Γ ⊢ ᾱ : Σ not involving focus or admit, with the property that Γ ⊢ α = ᾱ : Σ. (In fact, ᾱ is obtained, essentially, by erasing admit.) Now, as ᾱ does not contain focus or admit, no equational hypotheses are ever used in its formation, and so it is defined in the context Γ̄ without them. □

Corollary 2.10 Σ is injective in the category of contexts (possibly involving equations) and substitutions. □

Remark 2.11 How might such equational hypotheses be interpreted in a category S that does not necessarily have all equalisers? The obvious way is that, for f_{1}, f_{2} : X → A and g_{1}, g_{2} : X → B in S, the statement

x : X, f_{1}x = f_{2} : A ⊢ g_{1}x = g_{2}x : B

means that

for every a : Γ → X in S, if (f_{1} · h) = (f_{2} · h) then (g_{1} · h) = (g_{2} · h).

The restricted λ-calculus was formally extended with (abstract) sobriety [A] and monadicity [B]. This interpretation of equational hypotheses could be used to make another similar formal extension.

However, the result of such an extension would be an account of spatial locales (equivalently, sober spaces — in the traditional sense rather than that of [A]), not general ones. This is because the generality of the test object Γ is spurious: locally compact locales have enough points (classically, at least), and so this formula only uses the global points of Γ to test the equations. Equalisers (and, in fact, products) of locales and sober spaces are not the same [3, §II 2.13].

Remark 2.12 The category whose objects are contexts with equations has finite products, but it no longer has the exponentials Σ^{(−)} that originally motivated ASD — these are only defined on the subcategory of contexts without equations. The problem is inescapable since, as we have just noted, such hypotheses have already been used, albeit inadvertently. This means that the theory really captures, not the category of locally compact spaces on its own, but that category embedded in either the category of locales or or spatial locales.

Nevertheless, the way forward is not to rewrite what has been done in this hybrid fashion, but to study the (substantially) larger structure that includes both equalisers and exponentials. Preliminary investigations of this structure, relating not only to the whole of the category of locales but also to cartesian closed extensions, may be found in [H]. However, this structure not only contains spaces of a much more general kind, but also captures a much stronger logic of (implications amongst) equations. This means that, in order to nail down the precise equivalence with arithmetic universes (Remark 1.3), the proposed converse construction will probably be of a category analogous to spatial locales.

But for the purposes of the present paper, the equational hypotheses are simply a device for managing proofs.

3 Finite subsets as modal operators

Throughout, let X be an overt discrete space. Its typical values will be called x, y, etc. and its predicates ϕ, ψ, etc. We shall construct an object KX and then show that it is the free semilattice on X. Although KX is intended to be the space of Kuratowski-finite subsets of X, we shall use list notation for it, writing ℓ : KX for a typical value. So nil , { ; |x| ; } : KX denote the empty and singleton subsets, + is union and x :: ℓ = { ; |x| ; }+ℓ. Note that we also use {x} for λy. (x =_{X} y) : Σ^{X}. We shall actually need to switch back and forth between KX and ListX, and between the “mathematical” notion of monoid based on the + operation and the “computer science” notion based on ::.

Remark 3.1 KX will be constructed as a Σ-split subspace of Ω ≡ Σ^{Σ^{X}} × Σ^{Σ^{X}}.

The typical values of Ω will be called L = (N, P), where the letters stand for necessity and possibility, as the central idea is to represent a subset ℓ : KX by means of its modal operators [ℓ], ⟨ℓ⟩ : Σ^{Σ^{X}}, which also vary negatively and positively with respect to the inclusion of lists. Along with P : Σ^{Σ^{X}} we shall also make frequent use of π ≡ λx. P {x} : Σ^{X}.

Remark 3.2 If we already had KX and ListX at our disposal, we would define

[ℓ] ≡ λϕ. ∀x ∈ ℓ. ϕx and ⟨ℓ⟩ ≡ λϕ. ∃x ∈ ℓ. ϕx,

and the membership predicate (x ∈ ℓ) ≡ π_{ℓ}x = P {x}, where P ≡ ⟨ℓ⟩. Then

[ nil ] = λϕ. ⊤  ⟨ nil ⟩ = λϕ. ⊥  π_{nil} = λy. ⊥
[x :: ℓ] = ϕx ∧ [ℓ]ϕ  ⟨x :: ℓ⟩ = ϕx ∨ ⟨ℓ⟩ϕ  π_{x::ℓ} = λy. (x = y) ∨ π_{ℓ}y
[ℓ_{1} + ℓ_{2}] = [ℓ_{1}] ∧ [ℓ_{2}]  ⟨ℓ_{1} + ℓ_{2}⟩ = ⟨ℓ_{1}⟩ ∨ ⟨ℓ_{2}⟩  π_{ℓ_{1}+ℓ_{2}} = π_{ℓ_{1}} ∨ π_{ℓ_{2}},

so that [{ ; |x| ; }] = ⟨{ ; |x| ; }⟩ = ηx = λϕ. ϕx and π{ ; |x| ; } = {x}. Also

(ℓ_{1} ⊂ ℓ_{2}) ≡ ∀x ∈ ℓ_{1}. ∃y ∈ ℓ_{2}. (x =_{X} y) ≡ [ℓ_{1}](λx. ⟨ℓ_{2}⟩{x}) ≡ [ℓ_{1}]π_{2}

and (ℓ_{1} = ℓ_{2}) ≡ (ℓ_{1} ⊂ ℓ_{2}) ∧ (ℓ_{2} ⊂ ℓ_{1}), which are values of type Σ. Finally, the “Curried” operations □ ϕ ≡ λℓ. [ℓ]ϕ and ♢ ϕ ≡ λℓ. ⟨ℓ⟩ϕ generate the topology on the powerdomains (Remark 1.5), but are not very useful here.

Notation 3.3 As we want to construct KX as a subspace of Ω, we need to extend this notation to L ≡ (N, P) : Ω ≡ Σ^{Σ^{X}} × Σ^{Σ^{X}}. For the modal notation itself, we simply use [ ] and ⟨ ⟩ for the product projections, so □ ϕL ≡ [L]ϕ ≡ Nϕ and ♢ ϕL ≡ ⟨L⟩ϕ ≡ P ϕ. Then we define

nil  ≡ (⊤, ⊥) : Ω
x :: (N, P)  ≡ (x :: N, x :: P) ≡ (λϕ. Nϕ ∧ ϕx, λϕ. P ϕ ∨ ϕx)
(N_{1}, P_{1}) + (N_{2}, P_{2}) ≡ (N_{1} ∧ N_{2}, P_{1} ∨ P_{2})
≡ (λϕ. N_{1}ϕ ∧ N_{2}ϕ, λϕ. P_{1}ϕ ∨ P_{2}ϕ)
x ∈ L  ≡ ⟨L⟩{x} ≡ P {x} ≡ πx
L_{1} ⊂ L_{2}  ≡ [L_{1}](λx. ⟨L_{2}⟩{x}) ≡ N_{1}(λx. P_{2}{x}) ≡ N_{1}π_{2}
L_{1} ∼ L_{2}  ≡ (L_{1} ⊂ L_{2}) ∧ (L_{2} ⊂ L_{1})
L ∼ nil  = [L]⊥ ≡ N⊥
L ≁ nil  = ⟨L⟩⊤ ≡ P ⊤.

Clearly + is an associative, commutative, idempotent binary operation on Ω, and nil is a unit for it, with nil ⊂ L; we shall derive their other algebraic properties of + and ⊂ shortly. Notice, however, that for P they behave like ∨ and ≤, but for N they are like ∧ and ≥. This means that they are not intrinsic structure on Ω (as ≤, ∨ and ∧ are in Σ), but imposed on it by specifying certain maps.

The ∧/∨-ambiguity in the :: notation will always be resolved by the context, but we shall not risk confusion by further overloading of the important sign for equality.

Plainly not every pair (N, P) will arise as ([ℓ], ⟨ℓ⟩) from a finite subset.

Definition 3.4 We say that the pair Γ ⊢ (N, P) : Ω is modal if N and P satisfy

\begin{aligned}N⊤ & = & ⊤ & P ⊥ & = & ⊥ \\ N(ϕ ∧ ψ) & = & Nϕ ∧ Nψ & P (ϕ ∨ ψ) & = & P ϕ ∨ P ψ \\ N(ϕ ∨ ψ) & ≤ & Nϕ ∨ P ψ & P (ϕ ∧ ψ) & ≥ & P ϕ ∧ Nψ \\ N(λx. P \{x\}) & = & ⊤ & P ϕ & = & ∃x. ϕx ∧ P \{x\}. \end{aligned}

The last law, which recovers P from π ≡ λx. P {x}, implies that P preserves ⊥, ∨ and ∃. Recalling the classical connection between finiteness and Scott continuity, it is perhaps not surprising that Axiom 1.10 provides converses. If P is Scott continuous and preserves ⊥ and ∨ then it also preserves ∃ and satisfies the last law. From Scott-continuity of N, Theorem 11.7 shows that the modal laws exactly characterise Kuratowski-finite subsets.

In view of the number of things to be checked, we shall omit most of the proofs that pairs (N, P) are modal, recommending them as exercises. Note that the sixth and fifth laws usually require the Euclidean principle and its dual respectively.

When the ambient space is Hausdorff instead of discrete (e.g. ℝ), the seventh law is replaced by P (λx. N\overline{\{x\}}), where \overline{\{x\}} ≡ (λy. x ≠ y) [I].

Lemma 3.5 Modal operators satisfy the Frobenius law and its dual:

ϕ : Σ^{X}, σ : Σ ⊢ P (σ ∧ ϕ) = σ ∧ P ϕ and N(σ ∨ ϕ) = σ ∨ Nϕ.

Proof By the Phoa principle (Axiom 2.4), since P ⊥ = ⊥ and N⊤ = ⊤. □

Lemma 3.6 If (N, P) is modal then P {x} ∧ Nϕ ≤ ϕx.

Proof P {x} ∧ Nϕ ≤ P ({x} ∧ ϕ)

≡ P (λy. (x = y) ∧ ϕy)
= ∃y. P {y} ∧ (x = y) ∧ ϕy
= P {x} ∧ ϕx ≤ ϕx  □

Using these laws we can already recover the algebraic structure of KX.

Proposition 3.7 Definable finite subsets give rise to modal pairs because

(a) nil ≡ (⊤, ⊥) is modal;

(b) x : X ⊢ { ; |x| ; } ≡ (λϕ. ϕx, λϕ. ϕx) is modal;

(c) if Γ ⊢ (N_{1}, P_{1}), (N_{2}, P_{2}) : Ω are modal then so is (N_{1}, P_{1}) + (N_{2}, P_{2}). □

A similar study of the intersection operation raises topological questions.

Proposition 3.8 There is a greatest modal (N, P) iff X is compact, in which case N = ∀_{X}, P = ∃_{X} and π = ⊤.

Proof Suppose that there is a bound for all singletons:

λx. ({ ; |x| ; } ⊂ (N, P)) = λx. [{ ; |x| ; }](λy. P {y}) = λx. P {x} = π.

Hence if (N, P) is the greatest modal pair then π = ⊤. In this case,

P = λϕ. ∃x. πx ∧ ϕx = λϕ. ∃x. ϕx = ∃_{X}.

Also, x : X, ϕ : Σ^{X} ⊢ Nϕ = Nϕ ∧ P {x} = ϕx,

so Σ^{!_{X}} σ ≡ λx. σ ≤ ϕ iff σ ≤ N(λx. σ) ≤ Nϕ ≤ ϕx, which means that Σ^{!_{X}} ⊣ N, i.e. N = ∀_{X} and X is compact.

Now N(λx. ∃_{X}{x}) = N(λx. ∃y. x = y) = N⊤ = ⊤ so if X is compact then (N, P) ⊂ (∀_{X}, ∃_{X}). This pair is modal because, in particular,

∃x. (ϕx ∧ ψx) ≥ ∃x. ϕx ∧ (∀y. ψy) ≥ (∃x. ϕx) ∧ (∀y. ψy)
∀x. (ϕx ∨ ψx) ≤ ∀x. ϕx ∨ (∃y. ψy) ≤ (∀x. ϕx) ∨ (∃y. ψy)

by the Frobenius law and its dual. □

Proposition 3.9 If (=_{X}) is decidable (in which case we say that X is Hausdorff as well as discrete) and (N_{1}, P_{1}) and (N_{2}, P_{2}) are modal then so is (N, P), where

Nϕ = N_{1}(λx. ϕx ∨ N_{2}(λy. x ≠ y))
P ϕ = P_{1}(λx. ϕx ∧ P_{2}(λy. x = y))
= ∃x. P_{1}{x} ∧ P_{2}{x} ∧ ϕx,

and this is the meet with respect to ⊂. Decidability is necessary because, if { ; |x| ; } and { ; |y| ; } have a meet (N, P) that is modal, then N⊥ = (x ≠ y), so (x =_{X} y) is decidable. Intersection of decidable lists can also be defined by a “filtering” program — after we have proved that recursion is valid. □

The modal laws are also enough to ensure that ∼ provides the internal equality for KX.

Proposition 3.10 Let Γ ⊢ L_{1}, L_{2} : Ω be modal. Then these are equivalent:

(L_{1} ⊂ L_{2}) = ⊤  ⟨L_{1}⟩ ≤ ⟨L_{2}⟩  π_{1} ≤ π_{2}  [L_{2}] ≤ [L_{1}].

Proof By the 8th modal law, P_{1} ≤ P_{2} iff π_{1} ≤ π_{2}. Recall that

(L_{1} ⊂ L_{2}) ≡ [L_{1}](λx. ⟨L_{2}⟩{x}) ≡ N_{1}(λx. P_{2}{x}) ≡ N_{1}π_{2}.

By the 7th modal law this is implied by π_{1} ≤ π_{2} since ⊤ = N_{1}π_{1} ≤ N_{1}π_{2} ≡ (L_{1} ⊂ L_{2}), or by N_{2} ≤ N_{1} since ⊤ = N_{2}π_{2} ≤ N_{1}π_{2} ≡ (L_{1} ⊂ L_{2}).

Conversely, from L_{1} ⊂ L_{2}, we deduce successively that

Γ, ϕ : Σ^{X}, N_{2}ϕ = ⊤  ⊢ π_{2} ≤ ϕ  Lemma 3.6
Γ, N_{1}π_{2} = ⊤  ⊢ π_{1} ≤ π_{2}  similarly
Γ, N_{1}π_{2} = ⊤  ⊢ P_{1} ≤ P_{2}  8th modal law
Γ, N_{1}π_{2} = ⊤, ϕ : Σ^{X}, N_{2}ϕ = ⊤ ⊢ π_{1} ≤ π_{2} ≤ ϕ
Γ, N_{1}π_{2} = ⊤, ϕ : Σ^{X}, N_{2}ϕ = ⊤ ⊢ N_{1}π_{1} ≤ N_{1}ϕ  monotonicity
Γ, N_{1}π_{2} = ⊤, ϕ : Σ^{X}, N_{2}ϕ = ⊤ ⊢ ⊤ ≤ N_{1}ϕ  7th modal law
Γ, N_{1}π_{2} = ⊤, ϕ : Σ^{X}  ⊢ N_{2}ϕ ≤ N_{1}ϕ  Axiom 2.4
Γ, N_{1}π_{2} = ⊤  ⊢ N_{2} ≤ N_{1}  □

Corollary 3.11 Amongst modal pairs, ∼ provides the internal equality relation, whilst ⊂ is the imposed partial order for which the imposed semilattice structure + is the join.

Proof The relation ⊂ is reflexive and transitive because the equivalent conditions on [L] or ⟨L⟩ are. We have Γ ⊢ (L_{1} ∼ L_{2}) ≡ (L_{1} ⊂ L_{2}) ∧ (L_{2} ⊂ L_{1}) = ⊤ iff Γ ⊢ [L_{1}] ≥ [L_{2}], [L_{1}] ≤ [L_{2}], ⟨L_{1}⟩ ≥ ⟨L_{2}⟩ and ⟨L_{1}⟩ ≤ ⟨L_{2}⟩, which happens iff Γ ⊢ L_{1} = L_{2} : Ω. As for the relationship with +,

(L_{1} ⊂ L_{2}) = ⊤ ⊣⊢ ⟨L_{1}⟩ ≤ ⟨L_{2}⟩, [L_{1}] ≥ [L_{2}]
⊣⊢ ⟨L_{2}⟩ = ⟨L_{1}⟩ ∨ ⟨L_{2}⟩, [L_{2}] = [L_{1}] ∧ [L_{2}]
⊣⊢ L_{2} = L_{1} + L_{2}  □

Proposition 3.12 If (N, P) are modal then ((N, P) ∼ nil ) is decidable:

((N, P) ∼ nil ) = N⊥ and ((N, P) ≁ nil ) = P ⊤ = ∃x. x ∈ L.

Proof From the modal laws, N⊥ ∨ P ⊤ ≥ N(⊥ ∨ ⊤) = N⊤ = ⊤ and N⊥ ∧ P ⊤ ≤ P (⊥ ∧ ⊤) = P ⊥ = ⊥. On the other hand, ((N, P) ∼ nil ) = N⊥ by definition, whilst P ⊤ = P (∃x. {x}x) = ∃x. P {x} = ∃x. x ∈ L. □

Corollary 3.13 K0 = 1 and K1 = 2.

Proof Ω_{0} = Σ^{Σ^{0}} × Σ^{Σ^{0}} ≅ Σ × Σ and Ω_{1} = Σ^{Σ^{1}} × Σ^{Σ^{1}} ≅ Σ^{Σ} × Σ^{Σ}. By the Phoa principle and the constraints N⊤ = ⊤, P ⊥ = ⊥, N⊥ ∧ P ⊤ = ⊥ and N⊥ ∨ P ⊤ = ⊤, we have ((N, P) ∼ (⊤, ⊥)) ∨ ((N, P) ∼ (id, id)). □

Although we have seen that the modal laws characterise the algebraic structure of KX, we still have to show that it is

(a) a Σ-split subspace of Ω, as modal laws just define an equaliser;

(b) the free semilattice on X, with induction and recursion, and

(c) overt, making the quantifier ∃ℓ : KX in Axiom 1.10 legitimate. We shall do this by developing another characterisation of KX.

4 Fixed point properties

Since it is the purpose of the paper to define the space of Kuratowski-finite subsets, we have to eliminate them from the notation in the previous section. We illustrate this first with the extension of the existential quantifier on ∃ : Σ^{KX} → Σ to an operator E : Σ^{Ω} → Σ.

Remark 4.1 Transforming ∃ℓ. θℓ into θ nil ∨ ∃x. ∃ℓ. θ(x :: ℓ), we have

∃_{KX}θ ≡ ∃ℓ. θℓ = θ nil ∨ ∃x. ∃ℓ. θ(x :: ℓ)
= θ nil ∨ ∃x. ∃_{KX}(λℓ. θ(x :: ℓ))
≡ θ nil ∨ ∃x. ∃_{KX}(𝕊xθ).

We can therefore define E as the least fixed point of E = λΘ. Θ nil ∨ ∃x. E(𝕊xΘ), where we write Θ for a typical value of type Σ^{Ω} or predicate on Ω. Notice that unwinding this fixed point equation reveals the list representation of subsets that we had managed to conceal behind the semilattice structure in the previous section.

Notation 4.2 The shift operator 𝕊 : X × Σ^{Ω} → Σ^{Ω} is defined by

𝕊xΘ(N, P) ≡ Θ(x :: N, x :: P) ≡ Θ(λϕ. Nϕ ∧ ϕx, λϕ. P ϕ ∨ ϕx),

and the exception operator S : X × Σ^{Σ^{X}} → Σ^{Σ^{X}} by

SxNϕ ≡ N(λy. x = y ∨ ϕy).

Remark 4.3 Similarly, to prove that the embedding i : KX ↣ Ω is Σ-split, we must also show how to extend any predicate θ from KX to Ω, by means of a morphism I : Σ^{KX} → Σ^{Ω}. The composite E ≡ I · Σ^{i} is called a nucleus (Definition 5.1), starting from which, [B] shows how to define KX formally as a subspace of Ω. Like E, E will be defined by a fixed point equation, the idea being that

IθL ≡ ∃ℓ. (L ∼ ℓ) ∧ θℓ, so EΘL ≡ ∃ℓ. (L ∼ ℓ) ∧ Θ([ℓ], ⟨ℓ⟩).

We can expand this as before, since ((N, P) ∼ ℓ) = Nπ_{ℓ} ∧ [ℓ]π_{P}:

EΘ(N, P) = ∃ℓ. Nπ_{ℓ} ∧ [ℓ]π_{P} ∧ Θ([ℓ], ⟨ℓ⟩)
= Nπ_{nil} ∧ [ nil ]π_{P} ∧ Θ nil
∨ ∃x. ∃ℓ. Nπ_{x::ℓ} ∧ [x :: ℓ]π_{P} ∧ Θ([x :: ℓ], ⟨x :: ℓ⟩)
= (N⊥ ∧ ⊤ ∧ Θ nil )
∨ ∃x. ∃ℓ. SxNπ_{ℓ} ∧ P {x} ∧ [ℓ]π_{P} ∧ 𝕊xΘ([ℓ], ⟨ℓ⟩)
= (N⊥ ∧ Θ nil ) ∨ ∃x. P {x} ∧ E(𝕊xΘ)(SxN, P).  □

The reasoning that has led up to this fixed point equation depends on the prior existence of lists, so we have to start again from this formula as our “guess” for the definition of the nucleus E. First let us recall the fixed point property itself, which follows from Axiom 1.9, but also uses equational induction (Axiom 2.6).

Proposition 4.4 Let A = Σ^{U} and Γ ⊢ F : A^{A}. Then Γ ⊢ α ≡ ∃n. F^{n}⊥ : A satisfies Γ ⊢ F α = α. Moreover, if Γ ⊢ β : A is a pre-fixed point, that is, Γ ⊢ F β ≤ β, then Γ ⊢ α ≤ β. □

Definition 4.5 Let E_{∞} and E_{∞} be the least fixed points of their respective equations above. In the next section we shall prove that E_{∞} is a nucleus on Ω, also satisfying

⊢ E_{∞} ≤ id and x : X, Θ : Σ^{Ω} ⊢ E_{∞}(𝕊xΘ) ≤ 𝕊x($E_{∞}Θ),

so we define KX ≡ {Ω | E_{∞}}. We call Γ ⊢ L : Ω admissible if E_{∞} admits it:

Γ, Θ : Σ^{Ω} ⊢ E_{∞}ΘL = ΘL.

In Section 6 we shall show that all admissible L are modal, so we have the benefit of the algebraic structure that we described in the previous section.

Lemma 4.6 If Θ ≤ λL. σ then E_{∞}Θ ≤ σ.

Proof First, E_{0}Θ = Θ nil ≤ σ. Now, if E ≤ λΘ. σ then E(𝕊xΘ) ≤ σ, so

ΦE ≡ λΘ. Θ nil ∨ ∃x. E(𝕊xΘ) ≤ λΘ. σ.

This amounts to saying that Φ(λΘ. σ) ≤ (λΘ. σ), i.e. that λΘ. σ is a pre-fixed point of Φ; then by Proposition 4.4, the least fixed point E_{∞} satisfies E_{∞} ≤ λΘ. σ. □

Lemma 4.7 E_{∞}ΘL ≤ E_{∞}Θ.

Proof First, E_{0}ΘL = Θ nil ∧ [L]⊥ ≤ Θ nil = E_{0}Θ ≤ E_{∞}Θ, so E_{0} ≤ λΘL. E_{∞}Θ. Now suppose that E ≤ λΘL. E_{∞}Θ. Then

$EΘL = Θ nil ∧ [L]⊥ ∨ ∃x. E(𝕊xΘ)(SxN, P) ∧ P {x}
≤ E_{∞}Θ ∨ ∃x. E_{∞}(𝕊xΘ) = ΦE_{∞}Θ = E_{∞}Θ.

Again we have shown that λΘL. E_{∞}Θ is a pre-fixed point of $, so it is greater than the least fixed point, E_{∞}. □

Lemma 4.8 E_{∞} = E_{∞} · E_{∞}.

Proof First, E_{0}Θ = Θ nil = E_{0}Θ nil = E_{0}(E_{0}Θ) ≤ E_{∞}(E_{∞}Θ).

Now suppose that E ≤ E_{∞} · E_{∞}. Then

ΦEΘ = Θ nil ∨ ∃x. E(𝕊xΘ)
≤ E_{∞}(E_{∞}Θ) ∨ ∃x. E_{∞}(E_{∞}(𝕊xΘ))  hypothesis
≤ E_{∞}(E_{∞}Θ) ∨ ∃x. E_{∞}(𝕊x($E_{∞}Θ))  Definition 4.5
= ΦE_{∞}($E_{∞}Θ) = E_{∞}(E_{∞}Θ),

i.e. E_{∞} · E_{∞} is a pre-fixed point of Φ, so E_{∞} ≤ E_{∞} · E_{∞}, but they are equal since E_{∞} ≤ id. □

Proposition 4.9 KX ⊂ Ω is overt (not open), with existential quantifier and ♢-modal operator

∃_{KX} ≡ E · I ⊣ Σ^{!_{KX}} and E = ∃_{KX} · Σ^{i}.

Proof We require θ ≤ λℓ. σ iff ∃ℓ. θℓ ≤ σ. Forwards, Θ ≤ λL. σ ⊢ E_{∞}Θ ≤ σ (Lemma 4.6). Conversely, E_{∞}ΘL ≤ E_{∞}Θ = E_{∞}(E_{∞}Θ) (Lemmas 4.7 and 4.8). From this we also have ∃_{KX} · Σ^{i} = E_{∞} · I · Σ^{i} = E_{∞} · E_{∞} = E_{∞}. □

Besides equational and fixed point induction (Axiom 2.6 and Proposition 4.4), we shall need two other principles in the rest of the paper. The idea of the first one is that Θ_{⊤}L means ∃ℓ. L ∼ ℓ, and in fact Θ_{⊤} = E_{∞}⊤.

Lemma 4.10 Let ⊢ Θ_{⊤} : Σ^{Ω} be the least solution of

Θ_{⊤}(N, P) = N⊥ ∨ ∃x. Θ_{⊤}(SxN, P) ∧ P {x}.

Then L : KX ⊢ Θ_{⊤}L = ⊤, i.e. Θ_{⊤}(N, P) = ⊤ for all admissible (N, P). □

Proposition 4.11 We have the induction scheme

Γ ⊢ Θ : Σ^{Ω}  Γ ⊢ Θ nil = ⊤  Γ, L : Ω, ΘL = ⊤ ⊢ Θ(x :: L) = ⊤ ; = ; Γ ⊢ Θ ≤ 𝕊xΘ
Γ, L : KX ⊢ ΘL = ⊤

Proof Θ(N, P) ≥ $E_{∞}Θ(N, P)

= E_{0}Θ(N, P) ∨ ∃x. E_{∞}(𝕊xΘ)(SxN, P) ∧ P {x}
≥ N⊥ ∨ ∃x. E_{∞}Θ(SxN, P) ∧ P {x}

but Θ_{⊤} is the least (pre)fixed point of this, so Θ_{⊤} ≤ Θ. Hence if (N, P) is admissible then Θ(N, P) ≥ Θ_{⊤}(N, P) = ⊤. □

Although the form of this result is very familiar, its usefulness is rather limited, as it only tells us about open subspaces. Ultimately, Corollary 10.12 will provide an induction scheme of the form that any subspace that includes nil and is closed under :: is the whole space. The principle that we shall invoke repeatedly in Section 6 is the following.

Proposition 4.12 Let Γ ⊢ Θ, Φ : Σ^{Ω} (i.e. particular Θ and Φ are given). Then

Γ, L : Ω ⊢ E_{0}ΘL ≤ ΦL
Γ, E ≤ id nucleus, L : Ω, EΘL ≤ ΦL ⊢ $EΘL ≤ ΦL
Γ, L : KX ⊢ ΘL ≤ ΦL

i.e. ΘL ≤ ΦL for all admissible L.

Proof By equational induction (Axiom 2.6), Γ, n : ℕ ⊢ $^{n}E_{0}Θ ≤ Φ, so Γ ⊢ E_{∞}Θ = ∃n. $^{n}E_{0}Θ ≤ Φ. Hence if L is admissible then ΘL = E_{∞}ΘL ≤ ΦL. □

5 Stages in the construction

Definition 5.1 Recall from [B] that Γ ⊢ E : Σ^{Ω} → Σ^{Ω} is a nucleus on Ω if

Γ, H : Σ^{3}Ω ⊢ E(λL:Ω. H(λΘ:Σ^{Ω}. (EΘL)))L = E(λL:Ω. H(λΘ:Σ^{Ω}. ΘL))L.

Beware that we have shamelessly appropriated this word from locale theory, in which a nucleus j satisfies id ≤ j ≤ j^{2}. Nuclei in ASD need not in general be order-related to id, but those in this paper will satisfy E ≤ id.

A nucleus Γ ⊢ E : Σ^{Ω} → Σ^{Ω} on Ω admits a term Γ ⊢ L : Ω if

Γ, Θ : Σ^{Ω} ⊢ EΘL = ΘL or Γ ⊢ λΘ. EΘL = λΘ. ΘL.

If the context Γ is empty, [B] allows us to introduce a subtype i : {Ω | E} ↣ Ω with Σ-splitting I for which E = I · Σ^{i}. Then L belongs to the subtype iff E admits it. In this paper we shall need to define nuclei in non-trivial contexts, but we will not introduce the corresponding dependent types.

Definition 5.2 Following Remark 4.3, we construct the subspace KX ⊂ Ω using the nucleus E_{∞} that is defined as the least fixed point of the operator $ : (Σ^{Ω} → Σ^{Ω}) → (Σ^{Ω} → Σ^{Ω}), where

$EΘ(N, P) = E_{0}Θ(N, P) ∨ ∃x. E(𝕊xΘ)(SxN, P) ∧ P {x}

and E_{0} ≡ $⊥ ≡ λΘL. [L]⊥ ∧ Θ nil ≡ λΘNP . N⊥ ∧ Θ(⊤, ⊥).

The objects X^{(n)} ≡ {Ω | $^{n}E_{0}} that are obtained as the successive unwindings of this equation intuitively represent the collections of subsets of X with at most n elements.

Lemma 5.3 F⊤ ∧ F ⊥ ≤ FF.

Proof Apply Axiom 2.4 to F ⊥ = ⊤ ⊢ ⊤ = F ⊢ F⊤ = FF. □

This result shows how the singleton { nil } is embedded as a subspace of Ω.

Lemma 5.4 The singleton i : { nil } Ω is a Σ-split subspace, where

σ : Σ^{{ nil }} ⊢ Iσ ≡ λNP . σ ∧ N⊥
Θ : Σ^{Ω} ⊢ E_{0}Θ ≡ I(Σ^{i}Θ) = λNP . Θ nil ∧ N⊥.

Moreover E_{0} ≤ id, so I ⊣ Σ^{i}, and if E is any nucleus on Ω that admits nil then E_{0} ≤ E. □

Lemma 5.5 Θ(N, x :: P) ∧ P {x} = Θ(N, P) ∧ P {x}

(x :: SxN) = (x :: N) ≤ N ≤ SxN = Sx(x :: N)
P ≤ (x :: P)  (x :: P){x} = ⊤  P {x} ∧ ϕx ≤ P ϕ

Proof Apply Axiom 2.4 to

ϕx = ⊤ ⊢ Nϕ = SxNϕ, {x} ≤ ϕ and P {x} = ⊤ ⊢ x ::: P = P.  □

Lemma 5.6 E(𝕊xΘ) ≤ 𝕊x($EΘ). □

Lemma 5.7 If E ≤ id then $E ≤ id. □

Lemma 5.8 If E is a nucleus with E ≤ id then so is $E.

Proof Expanding the definition of the outer $E, in which H : Σ^{3}Ω,

$E(λL. H(λΘ. (\underline{$E}ΘL)))(N, P)
= E_{0}(λL. H(λΘ. (\underline{$E}ΘL)))
∨ ∃x. E(𝕊x(λL. \underline{$E}H(λΘ. ΘL)))(SxN, P) ∧ P \{x\},

and we have to show that we may delete the inner ones. First note that Θ nil ≤ $EΘ nil ≤ Θ nil , by Definition 5.2 and Lemma 5.7. Then

E_{0}(λL′. H(λΘ. $EΘL′))
= λL. (λL′. H(λΘ. $EΘL′)) nil ∧ [L]⊥
= λL. H(λΘ. $EΘ nil ∧ [L]⊥)
= λL. H(λΘ. Θ nil ) ∧ [L]⊥  above
= λL. (λL′. H(λΘ. ΘL′)) nil ∧ [L]⊥
= E_{0}(λL′. H(λΘ. ΘL′))
E(𝕊x(λL. H(λΘ. ΘL)))
≥ E(𝕊x(λL. H(λΘ. $EΘL)))  $E ≤ id
= E(λL. H(λΘ. $EΘ(x :: L))))  def 𝕊x
≥ E(λL. H(λΘ. E(𝕊xΘ)L))  Lemma 5.6
= E(λL. (H · Σ^{𝕊x})(λΘ. EΘL))  def Σ^{(−)}
= E(λL. (H · Σ^{𝕊x})(λΘ. ΘL))  E nucleus wrt H · Σ^{𝕊x}
= E(λL. H(λΘ. (𝕊xΘ)L))  def Σ^{(−)}
= E(λL. H(λΘ. Θ(x :: L)))  def 𝕊x
= E(𝕊x(λL. H(λΘ. ΘL)))  def 𝕊x □

As we have said, the ASD calculus does not currently allow us to define X^{(n)} as a type dependent on n, but we can at least introduce $^{n}E_{0} as a term dependent on n.

Proposition 5.9 n : ℕ ⊢ $^{n}E_{0} : Σ^{Ω} → Σ^{Ω} are nuclei with n : ℕ ⊢ $^{n}E_{0} ≤ $^{n+1}E_{0} ≤ id.

Proof The term n : ℕ ⊢ $^{n}E_{0} is formed by recursion. The base case of the induction is that ⊢ E_{0} ≤ id is a nucleus, which is Lemma 5.4. The induction step,

E : (Σ^{Ω})^{(Σ^{Ω})}, E ≤ id, E nucleus ⊢ E ≤ $E ≤ id, $E nucleus,

was proved in Lemmas 5.7 and 5.8; it has equations as hypotheses and conclusions. From these things we may deduce the result by equational induction on ℕ (Axiom 2.6). □

Proposition 5.10 ⊢ E_{∞} ≡ ∃n. $^{n}E_{0} is a nucleus with E_{∞} ≤ id. Proof By the previous result, $^{n}E_{0} = $^{n+1}⊥ is an ascending chain of nuclei with $^{n}E_{0} ≤ id. Writing

E : (Σ^{Ω})^{(Σ^{Ω})} ⊢ F E, GE : Σ

for the two sides of Definition 5.1 for a nucleus, Axiom 1.9 gives

⊢ F E_{∞} = F (∃n. $^{n}E_{0}) = ∃n. F ($^{n}E_{0})
= ∃n. G($^{n}E_{0}) = G(∃n. $^{n}E_{0}) = GE_{∞},

so E_{∞} is a nucleus. Lemma 5.7 showed that $id ≤ id, so id is a pre-fixed point of $, whence E_{∞} ≤ id by Proposition 4.4. □

This justifies Definition 4.5 and so the other results of the last section, apart from showing that all definable finite subsets give rise to admissible pairs.

Lemma 5.11 $E admits nil , since Θ nil ≤ $EΘ nil ≤ Θ nil . □

Lemma 5.12 If E admits L then $E admits x :: L. Proof

Θ(x :: L) = (𝕊xΘ)L = E(𝕊xΘ)L
≤ 𝕊x($EΘ)L = $EΘ(x :: L)
≤ (𝕊xΘ)L.

So Θ : Σ^{Ω} ⊢ Θ(x :: L) = EΘ(x :: L) as required. □

Lemma 5.13 If ⊢ E ≤ id is a nucleus then the pair

1 ^{nil} {Ω | $E} ^{::} X × {Ω | E}

is jointly Σ-split epi. Proof We have just shown that the two maps are well defined. In the diagram

{Ω | $E} [figure: nil , ::]  1 + X × {Ω | E}
Σ^{{Ω|$E}}[figure: Σ^{nil , ::}] Σ × Σ^{X×{Ω|E}}

Σ^{Ω}

[figure: $E]

Θ ↦ (Θ nil , λxL. E(𝕊xΘ)L)
λL. σ ∧ [L]⊥ ∨ ∃x. Φx(Sx[L], ⟨L⟩) ∧ ⟨L⟩{x} ← (σ, Φ)

Σ × Σ^{X×Ω} [figure: id × E^{X}]

we have to show that the inverse image map is given by the formula shown, and is split mono.

Let Θ : Σ^{{Ω|$E}}, x : X and L : {Ω | E}, i.e. E admits L. This means that

Θ(x :: L) = 𝕊xΘL = E(𝕊xΘ)L = ΦxL,

which justifies the inverse image map. Now the composite takes

Θ ↦ (σ, Φ) ↦ λL. σ ∧ [L]⊥ ∨ ∃x. Φx(Sx[L], ⟨L⟩) ∧ ⟨L⟩{x}
= λL. Θ nil ∧ [L]⊥ ∨ ∃x. E(𝕊xΘ)(Sx[L], ⟨L⟩) ∧ ⟨L⟩{x},

which is $EΘ, but the hypothesis on Θ says that Θ = $EΘ. □ Hence 1 + X ↠ X^{(1)}, 1 + X + X^{2} ↠ X^{(2)}, 1 + X + X^{2} + X^{3} ↠ X^{(3)}, ...

Proposition 5.14 The pair 1 ^{nil} KX ^{::} X × KX is jointly Σ-split epi. □

6 Admissible implies modal

Now we use the induction scheme in Proposition 4.12 to prove that all admissible pairs Γ ⊢ (N, P) : KX satisfy the modal laws, starting with the properties of the “possibility” operator P.

Lemma 6.1 Σ^{X} ◁ Σ^{Σ^{X}} by π ↦ λϕ. ∃x. ϕx ∧ πx and P ↦ λx. P {x}. □

Indeed, if (N, P) is admissible then P is recovered from π:

Lemma 6.2

L : KX, ϕ : Σ^{X} ⊢ ⟨L⟩ϕ = ∃x. ⟨L⟩{x} ∧ ϕx ≡ ∃x. πx ∧ ϕx ≡ ∃x. x ∈ L ∧ ϕx.

Proof (∃x. P {x} ∧ ϕx) ≤ P ϕ by Lemma 5.5, so we have to prove ≥.

Consider Θ ≡ λNP . P ϕ and Φ ≡ λNP . ∃y. P {y} ∧ ϕy in the context Γ ≡ [ϕ : Σ^{X}]. Then ⊢ E_{0}Θ ≤ Φ and E, EΘ ≤ Φ ⊢ $EΘ ≤ Φ. Hence L : KX, ϕ : Σ^{X} ⊢ ⟨L⟩ϕ ≡ ΘL ≤ ΦL ≡ ∃x. ⟨L⟩{x} ∧ ϕx by Proposition 4.12. □

Corollary 6.3 ⟨L⟩⊥ = ⊥, ⟨L⟩(ϕ ∨ ψ) = ⟨L⟩ϕ ∨ ⟨L⟩ψ ⟨L⟩(ϕ ∧ π) = ⟨L⟩ϕ. □ Next we consider the “necessity” operator N.

Lemma 6.4 (N, P) : KX ⊢ Nπ ≡ N(λx. P {x}) = ⊤, so (N, P) ∼ (N, P).

Proof Consider Θ(N, P) = N(λx. P {x}). Then Θ nil = ⊤ and

(𝕊xΘ)(N, P) = (x :: N)(λy. (x :: P){y})
= N(λy. P {y} ∨ y = x) ∧ (P {x} ∨ x = x)
≥ N(λy. P {y}) = Θ(N, P),

so by Proposition 4.11, H(N, P) = ⊤ for all admissible (N, P). □

Lemma 6.5 If L : KX then [L] preserves finite meets.

Proof We can show that N⊤ = ⊤ using Θ(N, P) ≡ N⊤ in Proposition 4.11. For Nϕ ∧ Nψ ≤ N(ϕ ∧ ψ) consider Θ(N, P) ≡ Nϕ ∧ Nψ and Φ(N, P) ≡ N(ϕ ∧ ψ) in Proposition 4.12. □

Corollary 6.6 [L]⊤ = ⊤, [L](ϕ ∧ ψ) = [L]ϕ ∧ [L]ψ and [L](ϕ ∧ π) = [L]ϕ.

Proof The last uses Lemma 6.4. □

Lemma 6.7 L : KX, x : X, ϕ : Σ^{X} ⊢ x ∈ L ∧ [L]ϕ ≤ ϕx, where (x ∈ L) ≡ ⟨L⟩{x}.

Proof With L = (N, P), this says that Nϕ ∧ P {x} ≤ ϕx.

Consider Θ(N, P) = Nϕ ∧ P {x} and Φ(N, P) = ϕx in Proposition 4.12. □

Corollary 6.8 [L](ϕ ∨ ψ) ≤ [L]ϕ ∨ ⟨L⟩ψ and ⟨L⟩(ϕ ∧ ψ) ≥ ⟨L⟩ϕ ∧ [L]ψ. □

Theorem 6.9 KX is overt discrete and has no proper open subalgebra for nil and ::.

Proof We have just shown that all L : KX are modal. For modal L_{1}, L_{2}, Proposition 3.10 said that L_{1} = L_{2} : Ω iff (L_{1} ∼ L_{2}) = ⊤, which is an open equivalence relation. Proposition 4.9 said that KX is overt. Lemmas 5.11–5.12 provided the algebra structure and Corollary 4.11 said that this is minimal. □

Unfortunately + is missing: we are not yet in a position to show that L_{1} + L_{2} is admissible when L_{1} and L_{2} are. This is because if L_{1} : X^{(n)} and L_{2} : X^{(m)} we would expect L_{1}+L_{2} : X^{(n+m)}, whereas our method of induction only takes us from n to n + 1. We shall show that + is well defined in Lemma 10.9, using the recursion scheme for nil and ::, but that is still a long way ahead.

7 K as a functor

We must show how K acts on f : X → Y between overt discrete objects, but we shall also prove that it preserves monos and inverse images, and that it takes coproducts (X = Y +Z) to products (KY × KZ). This means that any Kuratowski-finite subset L : KX may be partitioned between Y and Z. (We already know from Corollary 3.13 that K0 = 1.)

Remark 7.1 Recall that f : X → Y acts contravariantly on predicates, turning ψ : Σ^{Y} into Σ^{f}ψ ≡ λx. ψ(fx) : Σ^{X}, but covariantly on modal operators, so P : Σ^{Σ^{X}} becomes

Σ^{2}fP ≡ Σ^{Σ^{f}} P ≡ P · Σ^{f} ≡ λψ. P (Σ^{f}ψ) ≡ λψ. P (λx. ψ(fx)),

i.e. the composite with the inverse image Σ^{f} along f. In the case of an inclusion i : Y ↪ X, we may similarly compose with the direct image ∃_{i} ⊣ Σ^{i}, i.e.

(P · ∃_{i})ψ ≡ P (λx. ∃y. x = iy ∧ ψy).

In the case of the coproduct, Y ⊂ X = Y + Z is also closed, with Σ^{i} ⊣ ∀_{i}. For ψ : Σ^{Y} and y : Y, ∀_{i}ψ(iy) = ψy, whilst for z : Z, ∀_{i}ψ(jz) = ⊤, so

(N · ∀_{i})ψ = N(λx. (∃y. x = iy ∧ ψy) ∨ (∃z. x = jz)).

Locale theorists will recognise this construction as a special case of the relationship with open proper maps that we shall discuss in Section 11.

Lemma 7.2 If Γ ⊢ (N, P) : Ω_{X} is modal then so are Γ ⊢ Kf(N, P) ≡ (N · Σ^{f}, P · Σ^{f}) and Ki^{−1}(N, P) ≡ (N · ∀_{i}, P · ∃_{i}) : Ω_{Y}. □

But we have to show that they are admissible to KY whenever L : KX. Writing R(N, P) for either of them, we shall do the two cases in parallel, the analogy being that the second is for a partial map f : X ⇀ Y with decidable support (the “inverse” of i : Y ↪ X). In Lemma 7.9 we shall have to expand an ∃x in the definition of $E_{X}; the second case has two sub-cases, in which x = iy (so y = fx) and x = jz (so fx is undefined). The following lemmas therefore have three cases. We write E_{X}^{(n)} = $^{n}E_{0} and E_{X}^{(∞)} = ∃n. $^{n}E_{0} for the nuclei on Ω_{X} and similarly for Y.

In all three cases, R preserves the empty subset and unions:

Lemma 7.3 R nil_{X} = nil_{Y}, so [L]⊥ ≤ [RL]⊥ and E_{X}^{(0)}(Θ · R) ≤ (E_{Y}^{(0)}Θ) · R.

Proof Σ^{f}⊤ = ∀_{i}⊤ = ⊤ and Σ^{f}⊥ = ∃_{i}⊥ = ⊥.

[RL]⊥ = [L](H⊥) ≥ [L]⊥ where H = Σ^{f} or ∀_{i}.

E_{X}^{(0)}(Θ · R)L = Θ(R nil )) ∧ [L]⊥ ≥ Θ nil ∧ [RL]⊥ = (E_{Y}^{(0)}Θ)(RL). □

Lemma 7.4 L_{1}, L_{2} : Ω_{X} ⊢ R(L_{1} + L_{2}) = RL_{1} + RL_{2}, so + on Ω is natural in f : X → Y.

Proof (N_{1} ∧ N_{2}) · H = N_{1} · H ∧ N_{2} · H and (P_{1} ∨ P_{2}) · H = P_{1} · H ∨ P_{2} · H, where H = Σ^{f}, ∀_{i} or ∃_{i}. □

R either applies the function f to individual elements x, or “filters” the defined values y = fx = f(iy) from the undefined ones with x = jz.

Lemma 7.5 R\{ ; |x| ; \} = \begin{matrix}\{ \\ | & fx & | \\ \} \end{matrix}, R\begin{aligned}\{ \\ | & iy & | \\ & \} \end{aligned} = \{ ; |y| ; \} and R\begin{aligned}\{ \\ | & jz & | \\ & \} \end{aligned} = nil .

Proof We do □, the proof for ♢ being similar.

[\{ ; |x| ; \}](Σ^{f}ψ) = ηx(Σ^{f}ψ) = (Σ^{f}ψ)x = ψ(fx) = η(fx)ψ = [\begin{matrix}\{ \\ | & fx & | \\ \} \end{matrix}]ψ

[\begin{matrix}\{ \\ | & iy & | \\ & \} \end{matrix}](∀_{i}ψ) = η(iy)(∀_{i}ψ) = (∀_{i}ψ)(iy) = ψy = ηyψ = [\{ ; |y| ; \}]ψ

[\begin{matrix}\{ \\ | & jz & | \\ & \} \end{matrix}](∀_{i}ψ) = η(jz)(∀_{i}ψ) = (∀_{i}ψ)(jz) = ⊤ = [ nil ]ψ. □

Corollary 7.6 𝕊x(Θ · R) = (𝕊(fx)Θ) · R, 𝕊(iy)(Θ · R) = (𝕊yΘ) · R and 𝕊(jz)(Θ · R) = Θ · R. Proof Θ · R({ ; |x| ; } + L) = Θ(R{ ; |x| ; } + RL), which is respectively Θ(\begin{matrix}\{ \\ | & fx & | \\ \} \end{matrix} + RL), Θ(\{ ; |y| ; \} + RL) and Θ( nil + RL). □

Lemma 7.7 P {x} ≤ (P · Σ^{f}){fx}, P {iy} = (P · ∃_{i}){y} and P {jz} = (P · ∃_{j}){z}. Proof {x}x′ = (x = x′) ≤ (fx = fx′) = Σ^{f}{fx}x′ and {iy}x′ = (iy = x′) = ∃y′. (y = y′) ∧ (iy′ = x′) = ∃_{i}{y}x′. □

Lemma 7.8 “fL \ fx ⊂ f(L \ x)” in the sense that (SxN) · Σ^{f} ≤ S(fx)(N · Σ^{f}), so R(SxN, P) ≤ S(fx)(R(N, P)), (S(iy)N) · ∀_{i} = Sy(N · ∀_{i}), so R(S(iy)N, P ) = Sy(R(N, P)), and (S(jz)N) · ∀_{i} = (N · ∀_{i}), so R(S(jz)N, P ) = R(N, P).

Proof ((SxN) · Σ^{f})ψ = N(λx′. x′ = x ∨ ψ(fx′))

≤ N(λx′. fx′ = fx ∨ ψ(fx′))
= N(Σ^{f}(λy. y = fx ∨ ψy))
= (S(fx)(N · Σ^{f}))ψ
((S(iy)N) · ∀_{i})ψ = N(λx. x = iy ∨ ∀_{i}ψx)
= N(λx. ∃y′. x = iy′ ∧ (iy′ = iy ∨ ∀_{i}ψ(iy′))
∨ ∃z′. x = jz′ ∧ (jz′ = iy ∨ ∀_{i}ψ(jz′)))
= N(λx. ∃y′. x = iy′ ∧ (y′ = y ∨ ∀_{i}ψy′)
∨ ∃z′. x = jz′ ∧ (⊥ ∨ ⊤))
= (N · ∀_{i})(λy′. y = y′ ∨ ψy′)
= Sy(N · ∀_{i})ψ
((S(jz)N) · ∀_{i})ψ = N(λx. x = jz ∨ ∀_{i}ψx)
= N(λx. ∃y′. x = iy′ ∧ (iy′ = jz ∨ ∀_{i}ψ(iy′))
∨ ∃z′. x = jz′ ∧ (jz′ = jz ∨ ∀_{i}ψ(jz′)))
= N(λx. ∃y′. x = iy′ ∧ (⊥ ∨ ψy′)
∨ ∃z′. x = jz′ ∧ (z = z′ ∨ ⊤))
= N(λx. ∃y′. x = iy′ ∧ ψy′) ∨ ∃z′. x = jz′)
= (N · ∀_{i})ψ  □

Lemma 7.9 λΦ. E_{X}(Φ · R) ≤ λΦ. (E_{Y} Φ) · R ⊢ λΘ. $E_{X}(Θ · R) ≤ λΘ. ($E_{Y} Θ) · R. Proof We expand $E_{X} (Definition 5.2). By Lemma 7.3,

$E_{X}(Θ · R)(N, P) = E_{X}^{(0)}(Θ · R)(N, P) ∨ ∃x. (⋯)
≤ (E_{Y}^{(0)}Θ)(R(N, P)) ∨ ∃x. (⋯),

where the term (⋯) has three cases:

In the first, for f, use Corollary 7.6 and the premise with Φ ≡ 𝕊(fx)Θ:

E_{X}(𝕊x(Θ · R)) ≤ E_{X}((𝕊(fx)Θ) · R) ≤ (E_{Y} (𝕊(fx)Θ)) · R.

Hence, using Lemmas 7.7 and 7.8, and putting y ≡ fx,

(⋯) ≡ E_{X}(𝕊x(Θ · R))(SxN, P) ∧ P {x}
≤ (E_{Y} (𝕊(fx)Θ))(R(SxN, P)) ∧ (P · Σ^{f}){fx}
≤ (E_{Y} (𝕊yΘ))(Sy(R(N, P))) ∧ ⟨R(N, P)⟩{y}
≤ $E_{Y} Θ(R(N, P))  def $E_{Y}

Similarly, E_{X}(𝕊(iy)(Θ · R)) ≤ E_{X}((𝕊yΘ) · R) ≤ (E_{Y} (𝕊yΘ)) · R, so

(⋯) ≡ E_{X}(𝕊(iy)(Θ · R))(S(iy)N, P) ∧ P {iy}
≤ (E_{Y} (𝕊yΘ))(R(S(iy)N, P)) ∧ (P · ∃_{i}){y}
≤ (E_{Y} (𝕊yΘ))(Sy(R(N, P))) ∧ ⟨R(N, P)⟩{y}
≤ $E_{Y} Θ(R(N, P))

Finally, E_{X}(𝕊(jz)(Θ · R)) ≤ E_{X}(Θ · R) ≤ (E_{Y} Θ) · R ≤ ($E_{Y} Θ) · R, so

(⋯) ≡ E_{X}(𝕊(jz)(Θ · R))(S(jz)N, P) ∧ P {jz}
≤ $E_{Y} Θ(R(S(jz)N, P))
≤ $E_{Y} Θ(R(N, P))  □

Proposition 7.10 If L : KX then RL : KY in all three cases. Proof By Lemma 7.3, ⊢ λΘ. E_{X}^{(0)}(Θ · Ω_{f}) ≤ λΘ. (E_{Y}^{(0)}Θ) · Ω_{f}, and

n : ℕ, λΦ. E_{X}^{(n)}(Φ · R) ≤ λΦ. (E_{Y}^{(n)}Φ) · R
λΘ. E_{X}^{(n+1)}(Θ · R) ≤ λΘ. (E_{Y}^{(n+1)}Θ) · R,

by Lemma 7.9. So by equational induction (Axiom 2.6),

n : ℕ ⊢ λΘ. E_{X}^{(n)}(Θ · Ω_{f}) ≤ λΘ. (E_{Y}^{(n)}Θ) · Ω_{f},

whence Θ : Σ^{Σ_{Y}} ⊢ E_{X}^{(∞)}(Θ · Ω_{f}) ≤ (E_{Y}^{(∞)}Θ) · Ω_{f}.

As Γ ⊢ L : KX = {Ω_{X} | E_{X}^{(∞)}}, we have Γ, Φ : Σ^{Ω_{X}} ⊢ ΦL = E_{X}^{(∞)}ΦL. Putting Φ = Θ · R,

Θ(RL) = ΦL = (E_{X}^{(∞)}Φ)L = E_{X}^{(∞)}(Θ · R)L ≤ (E_{Y}^{(∞)}Θ)(RL) ≤ Θ(RL),

so these are equal and Γ ⊢ RL : {Ω_{Y} | E_{Y}^{(∞)}} = KY. □

We exploit the first case to define K as a functor.

Theorem 7.11 Let f : X → Y between overt discrete spaces and L : KX.

(a) Then KfL ≡ RL : KY,

(b) the inclusion K(−) ↣ Ω_{(−)} is natural in f,

(c) Kf is a homomorphism in the sense that Kf nil_{X} = nil_{Y} and Kf(x :: L) = fx :: KfL;

(d) K is a covariant functor, i.e. Kid_{X} = id_{KX} and K(g · f) = Kg · Kf.

(e) In fact, Kf(L + L′) = KfL + KfL′, but we don’t yet know that this is admissible. Proof [a] Proposition 7.10, [b] Lemma 7.3 and Corollary 7.6, [c] Remark 7.1 and [d] Lemma 10.9.

□

The other two cases almost show that K(Y + Z) ≅ KY × KZ.

Lemma 7.12 If (N, P) : Ω_{X}, (N_{1}, P_{1}) : Ω_{Y} and (N_{2}, P_{2}) : Ω_{Z} are modal then the following are inverse:

[figure: ((N_{1}, P_{1}), (N_{2}, P_{2})); (N_{1} · Σ^{i} ∧ N_{2} · Σ^{j}, P_{1} · Σ^{i} ∨ P_{2} · Σ^{j}); ((N · ∀_{i}, P · ∃_{i}), (N · ∀_{j}, P · ∃_{j})); (N, P)]

If (N, P) is admissible then so are (N_{1}, P_{1}) and (N_{2}, P_{2}). Conversely, if (N_{1}, P_{1}) = { ; |y| ; } and (N_{2}, P_{2}) is admissible then so is (N, P) = iy :: Kj(N_{2}, P_{2}).

Proof The isomorphism uses the equations

∀_{i} · Σ^{i} ∧ ∀_{j} · Σ^{j} = id_{Σ^{2}X} = ∀_{i} · Σ^{i} ∧ ∀_{j} · Σ^{j}
Σ^{i} · ∀_{i} = id_{Σ^{Y}} = Σ^{i} · ∃_{i} Σ^{j} · ∀_{j} = id_{Σ^{Z}} = Σ^{j} · ∃_{j}
Σ^{i} · ∀_{j} = ⊤ Σ^{j} · ∀_{i} = ⊤ Σ^{i} · ∃_{j} = ⊥ Σ^{j} · ∃_{i} = ⊥

Finally, Ki{ ; |y| ; } + KjL = (iy) :: KjL. □

This is enough for us to proceed to the investigation of ListX. With the aid of that, we shall later be able to prove that + is admissible, making KX a semilattice — indeed, the free one on X. This will also remove the restriction in the previous result.

We conclude this section by considering a non-complemented inclusion i : U ⊂ X. In this case we no longer have ∀_{i}, but we can instead apply ∃_{i} to both N and P.

Lemma 7.13 Let i : U ↪ X be a mono between overt discrete spaces, classified by ϕ : X → Σ. Then Ki : KU → KX is a split mono, classified by □ ϕ : KX → Σ.

[figure: U; 1; KU; 1; X; i; ∩; ϕ; Σ; ⊤; KX; Ki; ∩; □ ϕ; Σ; ⊤]

Proof Ki is split mono since

(N, P) ^{Ki} (N · Σ^{i}, P · Σ^{i}) ^{K ˆ∃_{i}} (N · Σ^{i} · ∃_{i}, P · Σ^{i} · ∃_{i}) = (N, P).

The square on the right commutes, since

L : KU ⊢ □ ϕ(KiL) = [KiL]ϕ = [L](Σ^{i}ϕ) = [L]⊤ = ⊤.

If Γ ⊢ L : KX with □ ϕL ≡ [L]ϕ = ⊤ then [L](ϕ ∧ ψ) = [L]ϕ ∧ [L]ψ = [L]ψ and ⟨L⟩ψ = [L]ϕ ∧ ⟨L⟩ψ ≤ ⟨L⟩(ϕ ∧ ψ) ≤ ⟨L⟩(ψ). Hence

Ki(K ˆ∃_{i}L) = ([L] · ∃_{i} · Σ^{i}, ⟨L⟩ · ∃_{i} · Σ^{i})
= (λψ. [L](ϕ ∧ ψ), λψ. ⟨L⟩(ϕ ∧ ψ))
= (λψ. [L]ψ, λψ. ⟨L⟩ψ) = L,

so L belongs to the retract, which is KU. □

Theorem 7.14 K preserves monos and their inverse images.

[figure: U; V; 1; KU; KV; 1]

[figure: X; i; ∩; f; Y; j; ∩; ϕ; Σ; ⊤; KX; Ki; ∩; Kf; KY; Kj; ∩; □ ϕ; Σ; ⊤]

Proof Since V and U are classified by ϕ and ϕ · f, we have just shown that KV and KU are classified by □ ϕ and □(ϕ · f), so we just need to check that

□(ϕ · f) = λL. [L](ϕ · f) = λL. ([L] · Σ^{f})ϕ = □ ϕ · Kf.  □

8 Lists, heads and tails

We shall derive the recursive properties of KX from those of ListX. The idea of the representation is that a list or sequence of length n is a partial function ℕ ⇀ X with support {0, 1, …, n − 1}, encoded as a finite set of pairs.

Definition 8.1 ListX ⊂ K(ℕ × X) is the open subspace classified by

\begin{matrix}λL. & [L](λnx. [L](λmy. n ≠ m ∨ x = y)) \\ ∧ & [L](λnx. n = 0 ∨ ⟨L⟩(λmy. n = m + 1)). \end{matrix}

In more suggestive notation (which will be justified in Lemma 9.10) ListX consists of the finite sets L of pairs such that ∀(n, x), (m, y) ∈ L. n ≠ m ∨ x = y and ∀(n, x) ∈ L. n = 0 ∨ ∃(m, y) ∈ L. n = m + 1. The first condition says that L, considered as a binary relation, is functional, and the second that this function is defined on an initial segment.

Proposition 8.2 ListX is overt discrete, being an open subspace of an overt discrete space. □

Definition 8.3 For z : X, L : ListX, let (z ::: L) ≡ Ki{ ; |z| ; } + KjL and tail L = Kj^{−1}L, where

[figure: X; i = (0, id); ℕ × X; j = succ ×id; ℕ × X.]

Expanding the definitions from the previous section,

[z ::: L]ϕ ≡ ϕ(0, z) ∧ [L](λmy. ϕ(m + 1, y))
⟨z ::: L⟩ϕ ≡ ϕ(0, z) ∨ ⟨L⟩(λmy. ϕ(m + 1, y))
[tail L]ϕ ≡ [L](λnx. n = 0 ∨ ∃m. n = m + 1 ∧ ϕ(m, x))
⟨tail L⟩ϕ ≡ ⟨L⟩(λnx. ∃m. n = m + 1 ∧ ϕ(m, x)).

Lemma 8.4 nil ∈ ListX, whilst if z : X and L : ListX then (z ::: L) : ListX.

Proof As [ nil ]ϕ = ⊤, the two conditions in Definition 8.1 are easily satisfied.

Lemma 7.12 is enough to show that z ::: L is in K(ℕ × X). To show that it is in ListX, we expand first the outer [z ::: L] and then the inner [z ::: L] or ⟨z ::: L⟩, using Corollaries 6.3 and 6.6 and some basic arithmetic.

[z ::: L](λnx. [z ::: L](λmy. n ≠ m ∨ x = y))
= [z ::: L](λmy. 0 ≠ m ∨ z = y)
∧ [L](λnx. [z ::: L](λmy. n + 1 ≠ m ∨ x = y))
= (0 ≠ 0 ∨ z = z) ∧ [L](λmy. 0 ≠ m + 1 ∨ z = y)
∧ [L](λnx. n + 1 ≠ 0 ∨ x = z))
∧ [L](λnx. [L](λmy. n + 1 ≠ m + 1 ∨ x = y))
= ⊤ ∧ ⊤ ∧ ⊤ ∧ [L](λnx. [L](λmy. n + 1 ≠ m + 1 ∨ x = y))
= [L](λnx. [L](λmy. n ≠ m ∨ x = y)) = ⊤
[z ::: L](λnx. n = 0 ∨ ⟨z ::: L⟩(λmy. n = m + 1))
= (0 = 0 ∨ ⟨z ::: L⟩(λmy. 0 = m + 1))
∧ [L](λnx. n + 1 = 0 ∨ ⟨z ::: L⟩(λmy. n + 1 = m + 1))
= ⊤ ∧ [L](λnx. ⊥ ∨ n + 1 = 0 + 1 ∨ ⟨L⟩(λmy. n + 1 = m + 1 + 1))
= [L](λnx. n = 0 ∨ ⟨L⟩(λmy. n = m + 1)) = ⊤  □

From this we can show that List is a functor to the category of internal (imposed) monoids.

Theorem 8.5 Let f : X → Y between overt discrete spaces and L : ListX. Then

List(f)(L) ≡ K(ℕ × f)(L) : List(Y),

List(f) is a homomorphism for nil and :::, i.e.

List(f)( nil_{X}) = nil_{Y} and List(f)(x ::: L) = fx ::: List(f)(L),

and List is a covariant functor, i.e.

List(id_{X}) = id_{List(X)} and List(g · f) = List(g) · List(f).

Functional programmers write mapfL for ListfL.

Proof We have K(ℕ × f)(L) : K(ℕ × Y) by Proposition 7.11, so we have to show that it satisfies Definition 8.1, and also show that Listf is a homomorphism for :::.

[K(ℕ × f)(L)](λny. [K(ℕ × f)(L)](λmy′. n ≠ m ∨ y = y′))
= Σ^{2}(ℕ × f)[L](λny. Σ^{2}(ℕ × f)[L](λmy′. n ≠ m ∨ y = y′))  7.11
= [L](λnx. [L](λmx′. n ≠ m ∨ fx = fx′))  Remark 7.1
≥ [L](λnx. [L](λmx′. n ≠ m ∨ x = x′)) = ⊤  (x = x′) ≤ (fx = fx′)
[K(ℕ × f)(L)](λny. n = 0 ∨ ⟨K(ℕ × f)(L)⟩(λmy′. n = m + 1))
= [L](λnx. n = 0 ∨ ⟨L⟩(λmx′. n = m + 1)) = ⊤  Proposition 7.11
K(ℕ × f)(x ::: L)
= K(ℕ × f)((0, x) :: K(succ ×X)L)  Definition 8.3
= (0, fx) :: K(ℕ × f) · K(succ ×X)L  Proposition 7.11
= (0, fx) :: K(succ ×Y) · K(ℕ × f)L  def (succ ×f)
= K(succ ×Y)(fx ::: K(ℕ × f)L)  Proposition 7.11

The other parts follow directly from Proposition 7.11. □

Next we show that every list is either empty or has a unique head and tail.

Lemma 8.6 For L : ListX and n : ℕ,

(∃x. (n + 1, x) ∈ L) ≤ (∃y. (n, y) ∈ L) ≤ (∃z. (0, z) ∈ L).

Proof Write α_{n} ≡ ⟨L⟩(λmx. n = m) ≡ (∃x. (n, x) ∈ L). The second part of Definition 8.1 for L : ListX says

[L](λnx. n = 0 ∨ ⟨L⟩(λmy. n = m + 1)),

which, together with the hypothesis α_{n+1} = ⊤, gives

(n + 1 = 0 ∨ ⟨L⟩(λmy. n + 1 = m + 1)) = ⊤,

which is equivalent to α_{n} = ⊤. Hence by Axiom 2.4 we have α_{n+1} ≤ α_{n} and

L : ListX, n : ℕ, α_{n} ≤ α_{0} ⊢ α_{n+1} ≤ α_{0},

which is the induction step for proving L : ListX, n : ℕ ⊢ α_{n} ≤ α_{0}. □

Lemma 8.7 If L : ListX then L = nil ∨ ∃!z. (0, z) ∈ L.

Proof From Proposition 3.12, either L ∼ nil or ∃nx. (n, x) ∈ L. In the latter case the previous result applies, giving ∃z. (0, z) ∈ L, which is unique by the first part of Definition 8.1. □

Lemma 8.8 Let L : ListX and x : X. Then tail L : K(ℕ × X), tail (x ::: L) = L, and if (0, z) ∈ L : ListX then L = z ::: tail L.

Proof These are corollaries of Lemma 7.12.

tail (z ::: L) = Kj^{−1}(Ki{ ; |z| ; } + KjL)
= (Kj^{−1} · Ki){ ; |z| ; } + (Kj^{−1} · KjL) = nil + L
z ::: tail L = Ki{ ; |z| ; } + Kj(tail L)
= Ki(Ki^{−1}L) + Kj(Kj^{−1}L) = L  { ; |z| ; } = Ki^{−1}L □

Lemma 8.9 If L : ListX then tail L : ListX.

Proof

[tail L](λnx. [tail L](λmy. n ≠ m ∨ x = y))
= [L](λnx. n = 0 ∨ (∃n′. n = n′ + 1 ∧ [L](λmy. m = 0
∨ ∃m′. m = m′ + 1 ∧ (n′ ≠ m′ ∨ x = y))))
≥ [L](λnx. n = 0 ∨ (n ≠ 0 ∧ [L](λmy. n ≠ m ∨ x = y)))
≥ [L](λnx. [L](λmy. n ≠ m ∨ x = y)) ≥ ⊤
[tail L](λnx. n = 0 ∨ ⟨tail L⟩(λmy. n = m + 1))
= [L](λnx. n = 0 ∨ ∃n′. n = n′ + 1 ∧ (n′ = 0
∨ ⟨L⟩(λmy. ∃m′. m = m′ + 1 ∧ n′ = m′ + 1)))
≥ [L](λnx. n = 0 ∨ n ≠ 0 ∧ (n = 1 ∨ ⟨L⟩(λmy. n = m + 1 ≠ 1)))
≥ [L](λnx. n = 0 ∨ n ≠ 0 ∧ ⟨L⟩(λmy. n = m + 1))
≥ [L](λnx. ⟨L⟩(λmy. n = m + 1)) ≥ ⊤  □

Proposition 8.10 ListX ≅ 1 + X × ListX, cf. Proposition 5.14 for KX. In particular,

(a) L : ListX ⊢ (L =_{ListX} nil ∨ ∃xL′. L =_{ListX} x ::: L′) = ⊤, and

(b) x, y : X, L, L′ : ListX ⊢ (x ::: L =_{ListX} y ::: L′) = (x =_{X} y) ∧ (L =_{ListX} L′). □

9 Recursion over lists

Lemma 9.1 Define ↓ : ℕ → List(1) by recursion,

↓ 0 = nil and ↓(n + 1) = ⋆ ::: (↓ n),

where ⋆ : 1, so ↓ is a homomorphism. Then ((k, ⋆) ∈ ↓ n) = (k < n),

[↓ n] = λϕ. ∀k < n. ϕ(k, ⋆) and ⟨↓ n⟩ = λϕ. ∃k < n. ϕ(k, ⋆).

Proof The recursive definition says that [↓ 0]ϕ = ⊤ and

[↓(n + 1)]ϕ = ϕ(0, ⋆) ∧ [↓ n](λky. ϕ(k + 1, y)),

but λϕ. ∀k < n. ϕ(k, ⋆) satisfies the same equations (Remark 3.2), so they are equal by the universal property of ℕ. Similarly for ⟨↓ n⟩ with ⊥, ∨ and ∃ in place of ⊤, ∧ and ∀. □

Remark 9.2 This means that

↓ 1 = \begin{matrix}\{ \\ | & (0, ⋆) & | \\ \} \end{matrix}, ↓ 2 = \begin{matrix}\{ \\ | & (0, ⋆), (1, ⋆) & | \\ \} \end{matrix}, ↓ 3 = \begin{matrix}\{ \\ | & (0, ⋆), (1, ⋆), (2, ⋆) & | \\ \} \end{matrix}, …

but we shall ignore the ⋆ from now on, and regard List(1) ⊂ K(ℕ).

Lemma 9.3 There is a unique map |−| : List(1) → ℕ such that

(n < |L|) = (n ∈ L) ≡ ⟨L⟩(λx. x = n)

and (|L| ≤ n) = (n ∉ L) ≡ [L](λx. x ≠ n).

Proof We must define |L| in terms of the presence or absence of numbers in the list, as it would be begging the question to use recursion on List(1).

The two properties n ∈ L and n ∉ L (as defined by ≡ above) are complementary by the modal laws, in particular Corollary 6.8.

⊤ = [L](λx. x ≠ n ∨ x = n)
≤ [L](λx. x ≠ n) ∨ ⟨L⟩(λx. x = n) ≡ (n ∉ L) ∨ (n ∈ L)
⊥ = ⟨L⟩(λx. x ≠ n ∧ x = n)
≥ [L](λx. x ≠ n) ∧ ⟨L⟩(λx. x = n) ≡ (n ∉ L) ∧ (n ∈ L).

Now ϕ ≡ λn. (x < n) satisfies the premise of Axiom 1.9, so

⊤ = [L](λx. ∃n. x < n) = ∃n. [L](λx. x < n)
≤ ∃n. [L](λx. x ≠ n) = ∃n. n ∉ L.

Hence we may use general recursion or sobriety [A, Lemma 9.11] to define |L| ≡ μn. n ∉ L, which therefore satisfies (n < |L|) ≤ (n ∈ L) and (|L| ≤ n) ≥ (n ∉ L). These are actually equalities, as Lemma 8.6 said that

(n + 1 ∈ L) ≤ (n ∈ L), and so (n ∉ L) ≤ (n + 1 ∉ L),

and indeed (m ≥ n ∉ L) ≤ (m ∉ L) by induction. □

Proposition 9.4 |−| and ↓ make List(1) ≅ ℕ.

Proof We show that ↓ and |−| are inverse. Using Lemmas 9.1, 9.3 and 6.2,

⟨↓ |L|⟩ϕ = ∃x < |L|. ϕx = ∃x. x < |L| ∧ ϕx
= ∃x. ⟨L⟩(λy. x = y) ∧ ϕx = ⟨L⟩ϕ,

so ↓ |L| = L by Proposition 3.10. On the other hand,

(|↓ m| > n) = ⟨↓ m⟩(λx. x = n) = (∃x < m. x = n) = (n < m)

by Lemmas 9.3 and 9.1, so |↓ m| = m. □

Corollary 9.5 For any overt discrete object X there is a map |−| : ListX → ℕ such that

|L| = 0 ⟺ L = nil , and |z ::: L| = |L| + 1.

The number |L| is called the length of the list.

Proof Define |L| ≡ |List(!_{X})L|, which is the composite of one homomorphism with the inverse of another. By Lemma 8.7, (L = nil ) is decidable. If L ≠ nil then L = x ::: L′ for some x and L′, so |L| = |L′| + 1 ≠ 0. □

Now we can start to define recursion over lists, in a way that will be very familiar to functional programmers. The first result depends on Proposition 8.10 and establishes existence, and the second uses Corollary 9.5 and gives uniqueness.

Lemma 9.6 Let A = Σ^{U} for some object U, equipped with an action of X:

Γ ⊢ ζ : A and Γ, x : X, α : A ⊢ σ(x, α) : A.

Then the term Γ ⊢ ϵ : A^{ListX} is a homomorphism in the sense that

ϵ nil = ζ and ϵ(x :: L) = σ(x, ϵL).

iff it satisfies the fixed point equation

ϵ = λL. (L = nil ∧ ζ) ∨ ∃x:X. ∃L′:ListX. (L = x ::: L′) ∧ σ(x, ϵL′).

Proof If ϵ is a homomorphism then by Proposition 8.10(a),

ϵL = (L = nil ∧ ϵL) ∨ ∃xL′. (L = x ::: L′ ∧ ϵL)
= (L = nil ∧ ζ) ∨ ∃xL′. L = x ::: L′ ∧ σ(x, ϵL′)

Conversely, if it is a fixed point then by Proposition 8.10(b),

ϵ nil  = ( nil = nil ∧ ζ) ∨ ∃xL′. ⊥ ∧ σ(x, ϵL′) = ζ
ϵ(y ::: L) = (y ::: L = nil ∧ ζ) ∨ ∃xL′. (y ::: L = x ::: L′) ∧ σ(x, ϵL′)
= ⊥ ∨ ∃xL′. (x = y) ∧ (L = L′) ∧ σ(x, ϵL′)
= σ(y, ϵL).  □

The simplicity of the last step is one reason why we have done this part of the argument for lists: the corresponding argument for finite subsets would be much more difficult. The other reason is that lists have a well defined length, which is the key to proving uniqueness, and more generally equational induction for lists.

Proposition 9.7 Let Γ, L : ListX ⊢ αL, βL : A ≡ Σ^{U}. Then, cf. Axiom 2.6,

Γ ⊢ α nil = β nil Γ, L : ListX, x : X, αL = βL ⊢ α(x ::: L) = β(x ::: L)
Γ, L : ListX ⊢ αL = βL

Proof Consider α_{n} ≡ λL. |L| ≤ n ∧ αL and β_{n} ≡ λL. |L| ≤ n ∧ βL, both of type Σ^{A×ListX}. Then α_{0} = β_{0} because (L = nil ) ⟺ (|L| = 0) by Corollary 9.5.

Suppose that α_{n} = β_{n}. Then if L′ : ListX with |L′| ≤ n, we have αL′ = α_{n}L′ = β_{n}L′ = βL′ and so α(x ::: L′) = β(x ::: L′) by hypothesis. Hence, using Proposition 8.10(a) and Corollary 9.5,

α_{n+1} = λL. (L = nil ∨ ∃x. ∃L′. (L = x ::: L′)) ∧ (|L| ≤ n + 1) ∧ αL
= λL. (L = nil ∧ α nil )
∨ ∃x. ∃L′. (L = x ::: L′) ∧ (|L′| ≤ n) ∧ α(x ::: L′)
= (the same for β) = β_{n+1}.

Thus α_{n} = β_{n} by equational induction for ℕ (Axiom 2.6), and

αL = (|L| ≤ |L|) ∧ αL = α_{|L|}L = β_{|L|}L = βL.  □

Theorem 9.8 ListX is the free (imposed, :::) monoid on X. It also obeys equational induction at all types.

Proof Let M be any type with an action Γ ⊢ z : M, r : X × M → M. We have already shown that some homomorphism ListX → M exists and is unique in the case where M = Σ^{U}, so we consider A ≡ Σ^{Σ^{M}}, ζ = λψ. ψx : A and σ : X × A → A by σ(x, F) = λψ. F (λm. (ψ · r)(x, m)).

Then there is a unique map ϵ : ListX → A such that

ϵ nil  = ζ = λψ. ψz
ϵ(x ::: L) = σ(x, ϵL) = λψ. ϵL(λm. (ψ · r)(x, m)).

Now we use Proposition 9.7 to show that ϵL is prime [A, §4]. Clearly ϵ nil is prime. Suppose that ϵL is prime, so (with F : Σ^{3}M)

λF. F(ϵL) = λF. ϵL(λm. F(λψ. ϕm)).

We shall show that ϵ(x ::: L) is also prime (with respect to G : Σ^{3}M), using

F ≡ λF. G(λψ. F (λm. (ψ · r)(x, m)))

in the primality equation for ϵL, so

G(ϵ(x ::: L)) = G(λψ. ϵL(λm. (ψ · r)(x, m)))  def ϵ(x ::: L)
≡ F(ϵL)  def F
= ϵL(λm. F(λψ. ψm))  ϵL prime (hypothesis)
= ϵL(λm. G(λψ. (ψ · r)(x, m)))  def F
= (λψ′. ϵL(λm. (ψ′ · r)(x, m)))(λm′. G(λψ. ψm′))  (λβ)^{−1}
= ϵ(x ::: L)(λm′. G(λψ. ψm′))  def ϵ(x ::: L)

Hence ϵL = λψ. ψ(eL) for some unique map e : ListX → M, which also satisfies e nil = z and e(x ::: L) = r(x, eL). □

We can now define all sorts of operations on lists in the usual way. We shall need the following in particular. Lemma 9.9 n < |L| iff ∃!x:X. (n, x) ∈ L, so we may define L@n by description [A, Section 9]. □ Lemma 9.10 [L]ϕ = ∀n < |L|. ϕ(n, L@n) and ⟨L⟩ϕ = ∃n < |L|. ϕ(n, L@n). Proof They satisfy the same recursion equations (cf. Remark 3.2). □ Definition 9.11 We define concatenation (++) on ListX in the usual way by recursion:

nil ++ L_{2} = L_{2} and (x ::: L_{1}) ++ L_{2} = x ::: (L_{1} ++ L_{2}).

Beware that ++ on ListX is not the same as + on K(ℕ × X) or Ω_{ℕ×X}. Proposition 9.12 Using list induction we prove in the usual way that

(a) ++ is associative with unit nil ;

(b) for any f : X → Y, Listf is a homomorphism for nil and ++; and

(c) ListX is the free monoid on X with respect to ++. □ Lemma 9.13 x = L@m for some m iff L = L′ ++{ ; |x| ; }++L′′ for some L′, L′′, where L′ = take (L, m) and L′′ = drop (L, m + 1) in functional programming notation. □ Lemma 9.14 List preserves equalisers. Proof Let X ^{i} Y [figure: f; g] Z be an equaliser of overt discrete spaces. (This exists, given f and g, because Z is discrete.) We show, using equational list induction on Γ ⊢ L : ListY, that if Γ ⊢ ListfL = ListgL : ListZ then Γ ⊢ ∃!L′:ListX. L = ListiL′. For the base case, nil_{Y} = Listi nil_{X}. For the induction step,

fy ::: ListfL ≡ Listf(y ::: L) = Listg(y ::: L) ≡ gy ::: ListgL

iff fy = gy ∧ ListfL = ListgL. Hence if L = ListiL′ (by the induction hypothesis) and y = ix then y ::: L = Listi(x ::: L′). □ Lemma 9.15 List preserves pullback over 1, i.e.

[figure: X + Y; Y; List(X × Y); Y]
[figure: X; 1; ListX; |−|; ℕ; |−|]

Proof Define zip : ListX × ListY → List(X × Y) by

zip (x ::: L_{1}, y ::: L_{2}) = (x, y) ::: zip (L_{1}, L_{2})
zip (L_{1}, nil )  = nil = zip ( nil , L_{2}).

Now if Γ ⊢ L_{1} : ListX and Γ ⊢ L_{2} : ListY make a commutative square, i.e. |L_{1}| = |L_{2}|, then L_{1} = Listπ_{0}(zip (L_{1}, L_{2})) and L_{2} = Listπ_{1}(zip (L_{1}, L_{2})), and Γ ⊢ zip (L_{1}, L_{2}) : List(X × Y) is the unique thing that does this. □

Theorem 9.16 List preserves all finite connected limits.

Proof They may be obtained from equalisers and pullbacks like this. □

10 The free semilattice

Now that we have the free monoid, and [C, Section 11] showed how to construct (stable effective) quotients of overt discrete objects by open equivalence relations, the free semilattice exists. We want to show that this free semilattice is in fact KX. One way to do this would be to follow the motivation in Section 3, which we have now made legitimate. Instead, we shall identify the quotient map ListX ↠ KX for the semilattice laws directly.

Recall from Theorem 7.11 that Kπ_{1} is a homomorphism in the sense that Kπ_{1} nil = nil and Kπ_{1}(x ::: L) = x :: Kπ_{1}L.

Lemma 10.1 Kπ_{1} is a homomorphism: Kπ_{1}(L_{1} ++ L_{2}) = Kπ_{1}L_{1} + Kπ_{1}L_{2}. □

Proposition 10.2 Kπ_{1} : ListX → KX is an open surjection.

Proof It is an open map since both ListX and KX are overt discrete [C, Lemma 10.2]. For it to be an open surjection [C, Definition 10.4] we have to show that Θ ≡ ∃_{Kπ_{1}}⊤ = ⊤ : Σ^{KX}, where

S : KX ⊢ ΘS ≡ ∃_{Kπ_{1}}⊤S = ∃L:ListX. (Kπ_{1}L = S).

Since Kπ_{1} nil = nil , we have Θ nil = ⊤. Then

ΘS ≡ ∃L. (Kπ_{1}L = S)
≤ ∃L. (Kπ_{1}(x ::: L) = x :: S)  above
≤ ∃L′. (Kπ_{1}L′ = x :: S)  where L′ = x ::: L
= Θ(x :: S) = 𝕊xΘS

so Θ ≤ 𝕊xΘ. Hence Θ = λS. ⊤ by Corollary 4.12. □

Lemma 10.3 Kπ_{1} is a natural transformation from List to K.

Proof Both composites in the square are of the form (N, P) ↦ (N · H, P · H), where H = Σ^{π_{1}} · Σ^{f} = Σ^{id×f} · Σ^{π_{1}}. □

Notation 10.4 Write L_{1}, L_{2} : ListX ⊢ L_{1} ≈ L_{2} : Σ for the open congruence generated by the semilattice laws. Explicitly, this is of the form ∃L:List(ListX). (⋯), where (⋯) says that the list L of lists begins L_{1}, ends L_{2} and its successive members are related by one of the semilattice laws. Being a congruence also means that if L_{1} ≈ L_{2} and L_{3} ≈ L_{4} then L_{1} ++ L_{3} ≈ L_{2} ++ L_{4}.

Lemma 10.5 Kπ_{1} : ListX → KX coequalises these laws, i.e. if L_{1} ≈ L_{2} then Kπ_{1}L_{1} = Kπ_{1}L_{2}.

Proof This is an equational induction over the list L, in which the induction step considers a single instance of a semilattice law L_{1} ≈ L_{2} in which two elements are either interchanged or coalesced. But Kπ_{1} is a homomorphism for +, and these laws hold in KX. □

Lemma 10.6 Kπ_{1}L_{1} ⊂ Kπ_{1}L_{2} iff (∀n < |L_{1}|. ∃m < |L_{2}|. L_{1}@n = L_{2}@m).

Proof Kπ_{1}L_{1} ⊂ Kπ_{1}L_{2} = [Kπ_{1}L](λx. ⟨Kπ_{1}L_{2}⟩(λy. x = y))  Notation 3.3

= Σ^{2}π_{1}[L](λx. Σ^{2}π_{1}⟨L_{2}⟩(λy. x = y))  Remark 7.1
= [L](λnx. ⟨L_{2}⟩(λmy. x = y))
= (∀n < |L_{1}|. ∃m < |L_{2}|. L_{1}@n = L_{2}@m)  L. 9.10 □

Lemma 10.7 If Kπ_{1}L_{1} ⊂ Kπ_{1}L_{2} then L_{1} ++ L_{2} ≈ L_{2}.

Proof By equational list induction on L_{1}. For the base case, nil ++ L_{2} = L_{2}. Suppose that x ∈ Kπ_{1}L. Then x = L@m for some m < |L|, so L = L ++ { ; |x| ; } ++ L for some lists L and L by Lemma 9.13, whence

(x ∈ Kπ_{1}L) ≤ ({ ; |x| ; } ++ L ≈ L) : Σ.

Hence for the induction step,

(Kπ_{1}(x ::: L_{1}) ⊂ Kπ_{1}L_{2}) = (x ∈ Kπ_{1}L_{2}) ∧ (Kπ_{1}L_{1} ⊂ Kπ_{1}L_{2})
≤ (x ∈ Kπ_{1}(L_{1} + L_{2})) ∧ (L_{1} ++ L_{2} ≈ L_{2})
≤ (x ::: (L_{1} ++ L_{2}) ≈ (L_{1} ++ L_{2})) ∧ (L_{1} ++ L_{2} ≈ L_{2})
≤ ((x ::: L_{1}) ++ L_{2} ≈ L_{2})  □

Corollary 10.8 Kπ_{1}L_{1} = Kπ_{1}L_{2} iff L_{1} ≈ L_{1} ++ L_{2} ≈ L_{2}, and so KX = ListX/≈. This coequaliser is valid in S as well as in E [C, Lemma 10.8]. □

Lemma 10.9 + : KX × KX → KX is well defined and is preserved by Kf.

[figure: ListX × ListX; Kπ_{1} × Kπ_{1}; KX × KX; Ω_{X} × Ω_{X}]

[figure: ListX; ++; Kπ_{1}; KX; . . . . . . . . . . . . . . . . .; Ω_{X}; +]

Proof The rectangle commutes by Lemma 10.1, the top left map is a surjection by Proposition 10.2 and the bottom right is a Σ-split mono, so there is a unique fill-in. The map f : X → Y turns the diagram into a commutative cuboid, since K ↣ Ω. Kπ_{1}, + and ++ are natural by Theorem 7.11(b), Lemma 10.3, Lemma 7.4 and Proposition 9.12(b). □

Theorem 10.10 KX is the free semilattice (in the sense of +) on X in S.

[figure: ListX; Kπ_{1}; KX; Ω]

.............. ϵ

[figure: X; \begin{matrix}\{ \\ | & (0, −) & | \\ \} \end{matrix}; M; δ; . . . . . . . . . . . . . . . . .]

Proof If M is an (imposed) semilattice then it is in particular a monoid, so by Proposition 9.12(c) there is a unique homomorphism (for nil , ::: and ++) ϵ : ListX → M. But as M also obeys the semilattice laws, ϵ factors through the coequaliser (Corollary 10.8), giving the required mediator δ : KX → M. This is a homomorphism (for nil and +) because Kπ_{1} is, and is surjective. If δ′ : KX → M is another homomorphism for nil and + then δ′ · Kπ_{1} : ListX → M is a homomorphism for nil and ++, so δ′ · Kπ_{1} = δ · Kπ_{1}, and δ′ = δ because Kπ_{1} is surjective. □

Proposition 10.11 Let Γ, L : KX ⊢ αL, βL : A ≡ Σ^{U}. Then, cf. Axiom 2.6 and Proposition 9.7,

Γ ⊢ α nil = β nil Γ, L : KX, x : X, αL = βL ⊢ α(x :: L) = β(x :: L)
Γ, L : KX ⊢ αL = βL

Proof Consider ᾱ ≡ α · Kπ_{1}, β̄ ≡ β · Kπ_{1} : ListX ↠ KX ⇉ A. These satisfy Proposition 9.7, so ᾱ = β̄, whence α = β since Kπ_{1} is surjective. □

Corollary 10.12 Any Σ-split subspace U ⊂ KX that contains nil and is closed under :: is U = KX.

Proof U can be expressed as the equaliser of some α, β : KX ⇉ A [B, Proposition 4.14]. □

11 Overt compact subspaces

After this lengthy manipulation in the logical calculus of ASD, you may be left wondering what “admissible” or “modal” terms L : KX ever had to do with “finite subsets” or “compact open subspaces” of X. In fact, the topological results follow from the modal laws in Definition 3.4, and it is these that we assume of L : Ω, rather than admissibility (L : KX), which we deduce on the basis of Axiom 1.10. In view of the lack of a theory of parametric types for ASD, we first consider a global (non-parametric) modal element ⊢ L : Ω.

Proposition 11.1 The open subspace i : U ⊂ X classified by π is overt (and discrete), with existential quantifier ∃_{U} = ⟨L⟩ · ∃_{i} and modal operator ⟨L⟩ = ∃_{U} · Σ^{i}. This justifies the notation ⟨L⟩ϕ ≡ ∃x ∈ L. ϕx, cf. the last version of Lemma 6.2.

Proof The space X is overt by hypothesis, and U is an open subspace of it classified by π, so U is itself overt, with ∃_{U} = ∃_{X} · ∃_{i}. What we have to show, therefore, is that

⟨L⟩ · ∃_{i} = ∃_{X} · ∃_{i} and ⟨L⟩ · ∃_{i} · Σ^{i} = ⟨L⟩.

As usual, we regard an open predicate θ on the open subspace U ⊂ X (which is classified by π) as a predicate on X itself, with θ ≤ π. This means that we represent ∃_{i} by id and Σ^{i} by π ∧ (−). Using the last of the eight modal laws, the first equation is then

⟨L⟩(∃_{i}θ) = ⟨L⟩θ = ∃x. πx ∧ θx = ∃x. θx = ∃_{X}(∃_{i}θ)

and the second, for ϕ : Σ^{X}, is ⟨L⟩(∃_{i} · Σ^{i}ϕ) = ⟨L⟩(π ∧ ϕ) = ⟨L⟩ϕ. □

Proposition 11.2 The subspace i : U ⊂ X is also compact, with universal quantifier ∀_{U} = [L] · ∃_{i} and modal operator [L] = ∀_{U} · Σ^{i}. This justifies the notation [L]ϕ ≡ ∀x ∈ L. ϕx.

Proof We have to show that Σ^{!} ⊣ [L] · ∃_{i} and [L] · ∃_{i} · Σ^{i} = [L]. Again we represent ∃_{i} by id and Σ^{i} by π ∧ (−). Let σ : Σ and u : U, i.e. u : X with πu = ⊤.

Suppose σ ≤ [L]ψ. Then σ ≤ [L]ψ ∧ πu ≤ ψu by Remark 3.6, so (λu:U . σ) ≤ ψ.

Conversely, suppose λu:U . σ ≤ ψ, so x : X ⊢ σ ∧ πx ≤ ψx. Then

σ = σ ∧ [L]π  7th modal law
≤ [L](λx. σ ∧ πx)  Euclid
≤ [L]ψ  hypothesis

For the modal operator, with ϕ : Σ^{X}, [L](∃_{i} · Σ^{i}ϕ) = [L]ϕ. □

The subspace U need not be Hausdorff, i.e. have decidable equality, as we haven’t assumed this of X itself.

Proposition 11.3 Conversely, let U ⊂ X be compact open. Then ⊢ (N, P) : Ω is modal, where P ≡ ∃_{U} · Σ^{i} and N ≡ ∀_{U} · Σ^{i}.

Proof As for Proposition 11.10 below without γ. □

Once again we have a result for modal L : Ω when we really want one for admissible L : KX, but now at last we are able to state, and so invoke, the Scott continuity Axiom 1.10.

Theorem 11.4 ⊢ L : Ω_{X} is admissible iff it is modal, and such terms correspond bijectively to compact open subspaces U ⊂ X. Moreover, a subspace U ⊂ X is compact open iff it is listable.

Proof Without loss of generality U = X. Applying Axiom 1.10 to F ≡ ∀_{X}, α_{ℓ} = ⊤ and ϕ_{ℓ} = π_{ℓ}, where X is a compact overt discrete space, we have

⊢ ⊤ = ∀_{X}⊤ = ∃ℓ:KX. ∀_{X}(λx. x ∈ ℓ) = ∃ℓ:KX. (∀x:X. x ∈ ℓ).

This means that (∀_{X}, ∃_{X}) ⊂ ℓ, where ℓ is admissible and (∀_{X}, ∃_{X}) is modal, whilst ℓ ⊂ (∀_{X}, ∃_{X}) since (∀_{X}, ∃_{X}) is the greatest modal pair (Proposition 3.8). Hence (∀_{X}, ∃_{X}) ∼ ℓ, which means that (∀_{X}, ∃_{X}) is admissible (and ∃ℓ above is unique). Notice that the two universal quantifiers in

∃ℓ:KX. (∀y ∈ ℓ. ∃u:U . x = iu) ∧ (∀u:U . ∃x ∈ ℓ. x = iu) : Σ

are legitimate because both U and ℓ define compact spaces.

In the last part, ⇐ follows from well known topological results, namely that the image of a compact overt space is compact overt, and that any overt subspace of a discrete space is open [C]. The more significant ⇒ comes from the fact that ListX ↠ KX. □

Remark 11.5 We have to be careful with the notion of listability: we may legitimately use a listing to prove results about U only if the statements of those results does not depend on the choice of listing [8, §6.6].

Definition 11.6 An object X that is listable in the above sense is called Kuratowski finite. If it is also Hausdorff then there is a listing without repetitions, in which case we say that X is simply finite. Recall from Propositions 3.8–3.9 that KX has a greatest element iff X is Kuratowski finite, and is a lattice (in fact a Boolean algebra) iff X is finite.

Encouraged by this success, we use the same Axiom and proof for the

Theorem 11.7 Any Γ ⊢ L : Ω is admissible iff it is modal.

Proof We have a directed union in the sense of Axiom 1.10,

π : Σ^{X}, x : X ⊢ πx = ∃ℓ:KX. (∀y ∈ ℓ. πy) ∧ (x ∈ ℓ).

This is preserved by any Γ ⊢ N : Σ^{Σ^{X}}, so

Γ ⊢ ⊤ = N(λx. P {x})  7th modal law
= N(∃ℓ. (∀y ∈ ℓ. P {y}) ∧ (λx. x ∈ ℓ))  above
= ∃ℓ. (∀y ∈ ℓ. P {y}) ∧ N(λx. x ∈ ℓ)  Axiom 1.10
= ∃ℓ. (ℓ ⊂ (N, P)) ∧ (N, P) ⊂ ℓ))  Notation 3.3
= ∃ℓ:KX. (ℓ = (N, P)),  Corollary 3.11

where ℓ is unique and admissible, so (N, P) is itself admissible. □

What are the results for parametric Γ ⊢ L : KX corresponding to the compact open subspace U ⊂ X above? If we had a theory of parametric types, in place of a single object U, we would have a display map U − ; − ; ▷ Γ [8, Chapter VIII]. The idea that each U_{γ} is overt compact is expressed by saying that p : U − ; − ; ▷ Γ is an open proper map [C, §7]. Also, where U ⊂ X was an open subspace, U ⊂ Γ × X is an open binary relation Γ ↽ ⇀ X. We call this a Kuratowski-finite subset of X dependent on Γ.

Proposition 11.8 Let Γ ⊢ (N, P) : KX. Then there is a diagram as shown, in which the open subspace i : U ↪ X × Γ is classified by λxγ. P γ{x} : Σ^{X×Γ}, the three squares are pullbacks, and p is an open proper map.

[figure: U; (∈); 1]

[figure: X × Γ; i; ∩; X × KX; ∩; x, (N′, P′) ↦ P′{x}; Σ; ⊤]

[figure: p; Γ; π_{1}; (N, P); KX; π_{1}]

Proof The composite p = π_{1} · i is open since X is overt. To show that p is proper, we must find the right adjoint of Σ^{p} and verify the dual Frobenius law [C, Definition 7.3] and Beck– Chevalley condition. In fact, we shall also give another formula for the left adjoint, and I claim that E · ∃_{i} = ∃_{X}^{Γ} · ∃_{i} = ∃_{p} ⊣ Σ^{p} ⊣ A · ∃_{i}.

[figure: Σ^{U}; \underline{Σ^{i}}; ⊤; ∃_{i}; Σ^{X×Γ}; A : ψ ↦ λγ. Nγ(λx. ψ(x, γ)); E : ψ ↦ λγ. P γ(λx. ψ(x, γ)); Σ^{Γ}; \overline{Σ^{p}}]

First recall that (∃_{i} · Σ^{i}ψ)(x, γ) = ψx ∧ (x, γ) ∈ U = ψx ∧ P γ{x}, and let x : X, γ : Γ, θ : Σ^{Γ} and ψ : Σ^{X×Γ}.

For the left adjoint we require E · (∃_{i} · Σ^{i}) = ∃_{X}^{Γ} · (∃_{i} · Σ^{i}).

For the unit of the right adjoint, id_{Σ^{Γ}} ≤ A · (∃_{i} · Σ^{i}) · Σ^{π_{1}}.

For the counit, (∃_{i} · Σ^{i}) · (Σ^{π_{1}} · A) · (∃_{i} · Σ^{i}) ≤ (∃_{i} · Σ^{i}).

For the dual Frobenius law, A · ∃_{i}(ϕ ∨ Σ^{p}θ)γ = A(∃_{i}ϕ)γ ∨ θγ.

Finally, we must show stability under pullback along s : Δ → Γ. This follows by application of the same results, but for Δ ⊢ (s^{∗}N, s^{∗}P) : KX.

[figure: Σ^{s^{∗}U}; Σ^{U}; s^{∗}U; U; (∈); 1]

[figure: Σ^{X×Δ}; ∃_{j}; Σ^{X×s}; Σ^{X×Γ}; ∃_{i}; X × Δ; j; ∩; X × s; X × Γ; i; ∩; X × KX; ∩; Σ; ⊤]

[figure: Σ^{Δ}; A′; Σ^{s}; Σ^{Γ}; A; Δ; π_{1}; s; Γ; π_{1}; (N, P); KX; π_{1}]

The Beck–Chevalley condition for the top left square is that for the inverse image of an open inclusion [C, Proposition 3.11]. In the the bottom left square, where

A′θ ≡ λδ. N(sδ)(λx. θ(x, δ)),

the Beck–Chevalley condition is

Σ^{s}(Aψ)δ = N(sδ)(λx. ψ(x, sδ)) = A′(Σ^{X×s}ψ)δ.  □

Corollary 11.9 In particular, (∈) ↪ X × KX → KX is open and proper. □

Proposition 11.10 Conversely, let i : U ↪ X × Γ be open such that p ≡ (π_{1} · i) : R → Γ is (open and) proper. Then Nγϕ = ∀_{p}(λu. ϕ(qu)) and

P γϕ = ∃_{p}(λu. ϕ(qu)) = ∃x. ϕx ∧ (x, γ) ∈ U = ∃x. ϕx ∧ P γ{x}

are modal (where q ≡ (π_{0} · i) : R → X). We recover U from P as P γ{x} = ((x, γ) ∈ U). □

Theorem 11.11 KX classifies Kuratowski finite subsets of X, in the sense that open proper relations Γ ↽ ⇀ X as above = Γ ⟶ KX

□

Theorem 11.12 KX classifies Kuratowski finite subsets of X.

[figure: U; (∈); Γ; p; KX]

Indeed (∈) : X ↽ ⇀ KX is the generic Kuratowski-finite subset of X (dependent on KX). By this we mean that any pullback of it as shown is a Kuratowski-finite subset of X dependent on Γ, and every Kuratowski-finite subset of X dependent on Γ arises uniquely in this way. □

References

[1] Cockett, J. R., List-arithmetic distributive categories: Locoi, Journal of Pure and Applied Algebra 66 (1990), pp. 1–29.

[2] Hofmann, M., “Extensional concepts in intensional type theory,” Ph.D. thesis, Edinburgh (1995).

  URL http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327

[3] Johnstone, P., “Stone Spaces,” Number 3 in Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1982.

[4] Johnstone, P. T., Vietoris locales and localic semi-lattices, in: R.-E. Hoffmann and K. H. Hoffmann, editors, Continuous Lattices and their Applications, Marcel Dekker, 1985 pp. 155–180.

[5] Lambek, J. and P. J. Scott, “Introduction to Higher Order Categorical Logic,” CUP, 1986.

[6] Maietti, M. E., Joyal’s arithmetic universes via type theory, ENTCS 69 (2003).

[7] Maietti, M. E., Reflection into models of finite decidable FP-sketches in an arithmetic universe, ENTCS ? (2005).

[8] Taylor, P., “Practical Foundations of Mathematics,” CUP, 1999.

[9] Vickers, S. J., “Topology Via Logic,” Cambridge Tracts in Theoretical Computer Science 5, Cambridge University Press, 1988.

[10] Winskel, G., Powerdomains and modality, in: M. Karpinski, editor, Foundations of Computation Theory, number 158 in LNCS (1983), pp. 505–514.

My papers on abstract Stone duality may be obtained from

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

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

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

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

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

[F] Scott domains in abstract Stone duality. March 2002.

[G–] Local compactness and the Baire category theorem in abstract Stone duality. Electronic Notes in

Theoretical Computer Science 69, Elsevier, 2003.

[G] Computably based locally compact spaces. Logical Methods in Computer Science, 2005, to appear. [H-] An elementary theory of the category of locally compact locales. APPSEM Workshop, Nottingham,

March 2003.

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

[I] The Dedekind reals in abstract Stone duality. December 2004.

[J] A λ-calculus for real analysis. December 2004.

I would like to thank Peter Aczel, Andrej Bauer, Robin Cockett, Maria Emilia Maietti and Gavin Wraith for their helpful comments. This paper was accepted for Category Theory and Computer Science 10, which was held in Copenhagen in August 2004, and an abridged version appeared in the printed proceedings. However, I was unable to attend, as I had broken my leg two weeks earlier. Research on Abstract Stone Duality has been funded since September 2003 by the EPSRC project GR/S58522 of the same title, but the basic results of Sections 3–6 had been found in July–August 2003.