Intuitionistic Sets and Ordinals

Paul Taylor

1993

Abstract

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.

We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifes the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.

Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.

We treat ordinals as order-types, and develop a corresponding set theory similar to Osius’ transitive set objects. This presents Mostowski’s theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski’s theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.

The comparison between sets and toposes is developed as far as the identification of replacement with completeness and there are some suggestions for further work in this area.

Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy.

Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.

Presented at Category Theory and Computer Science 5, Amsterdam, September 1993. Published in the Journal of Symbolic Logic 61 (1996) 705–744.

1 Well founded induction Transfinite induction is very widely and readily used in classical mathematics. In its extreme form — the Procrustean enumeration of elements of arbitrary sets known as the “well” ordering principle — it is equivalent to choice and is irreconcilable with constructivity. However ordinals are also used in proof theory and infinitary algebra to extend the iterative constructions used in finitary cases, so it would be of great benefit to include them in an intuitionistic categorical account.

Georg Cantor [4] defined ordinals as well founded relations which satisfy the trichotomy law,

(x ≺ y) ∨ (x = y) ∨ (y ≺ x),

but to show that unions of ordinals have this property depends on excluded middle. However trichotomy is provable (classically, Proposition 4.8)^{1} if ordinals are re-defined as “transitive sets of transitive sets,” i.e. transitive extensional well founded relations. William Powell [25] showed that this definition allows intuitionistic transfinite recursion, but as Robin Grayson [10] pointed out, the successor operation, α ↦ α ∪ {α}, is poorly behaved. A new kind of successor, more intuitionistic in character, is defined in Proposition 5.5.

1I have been unable to identify who first discovered this (non-trivial) fact, which certainly deserves credit.

(For the sake of orientation, you may find it helpful to read Sections 5 or 7 first.)

The other part of the Cantor’s definition, that a relation ≺ on a carrier is well founded if every nonempty subset has a ≺-minimal element, must also be changed. It is not satisfied by the natural numbers and cannot prove the theorems without excluded middle, so I don’t understand why intuitionists bother to mention it. We want well-foundedness to perform induction and recursion.

Definition 1.1 The induction scheme is the rule

∀x. [∀x′. x′ ≺ x ⇒ ϕ(x′)] ⇒ ϕ(x) ≺-induction

∀x. ϕ(x)

for each predicate ϕ (possibly involving other variables besides x) on X, where ≺ is a binary relation on a carrier X. We say that ≺ is well founded if the induction scheme is valid [20]. Note that x ≺ x never holds.

Definition 1.2 If x ≺ y then we call x a child of y, and we write ≺ ≺ for the (irreflexive) transitive closure, so x ≺ ≺ y means that x is a descendant of y. Contrary to tradition, ∅ is the ultimate descendant, not the original ancestor. A subset U ⊂ X such that

∀x ∈ X, u ∈ U. x ≺ u ⇒ x ∈ U

is called an initial segment. (A subset satisfying the similar closure property with respect to a reflexive relation will be called a lower subset; for ordinals, being a lower set with respect to ⊂ implies being an initial segment with respect to ∈, but not conversely.) This is a unary closure condition, so the intersection or union of initial segments is initial. In particular we write X ↓ x for the slice,^{2} i.e. the initial segment which x generates. We also write

\overline{≺} : X → P(X) by x ↦ \{y : y ≺ x\}

Remark 1.3 We shall occasionally regard propositions as values in Ω, the type of truth values (known in topos theory as the subobject classifier). In particular the predicate (≺) ⊂ X × X defines a function (≺) : X → X → Ω. Then \overline{≺} : X → Ω^{X} ≅ P(X) is the λ-abstraction or exponential transpose of this. In order to see the difference intuitionistic logic makes to powersets and ordinals, it suffices to think of Ω as the lattice of open sets of a topological space, the world E being the category of sheaves. Each proposition corresponds to the open set on which it is true. The theorems we prove assert ⊢ ϕ, that ϕ is true everywhere. To illustrate the distinction we occasionally give (“weak”) counterexamples: these do not claim ⊢ ¬ϕ (that ϕ is true nowhere) but ⊬ ϕ (we cannot prove that ϕ holds everywhere, though in fact it may hold, and we may know that it holds, in some places).

The general recursion theorem extends inductive proof to recursive construction.

Proposition 1.4 Let A be a carrier equipped with a system of operations R_{x} : P(A) → A for x ∈ X. Then the equation

f(x) = R_{x}({f(x′) : x′ ≺ x})

has a unique solution f : X → A.

2This notation is used here in the sense that x ∈ X ↓ x. The slice is one of several ideas adopted from (categories or) posets, but since well founded relations are irreflexive it is not clear whether one ought to include or exclude the element x itself in X ↓ x. The slice plays a similar rôle in this work to the transitive closure of a set in set theory.

Proof An attempt is a partial function f : X ⇀ A whose support is an initial segment, and which satisfies the equation in the sense that if the left hand side is defined then so is the right, and then they are equal. Any two attempts agree on the intersection of their supports, so the union of all attempts is an attempt. By applying the equation to this it is shown to be defined throughout X. □

The function R could instead be an (infinitary) algebraic operation, giving different values to R(a, b), R(a, a, b) and R(b, a). The general recursion theorem is presented this way in [30]. However in this paper ≺ will normally be extensional, in which case R is unable to tell when its arguments are repeated or permuted. However one position may stand out intrinsically, for example by being necessarily the largest of the arguments.

Remark 1.5 Gerhard Osius [22], citing Richard Montague [20], expresses the general recursion theorem as f = R ∘ P(f) ∘ \overline{≺}.

[figure: P(X); P(f); P(A); X; \overline{≺}; f; A; R]

The diagram-chasing style will be developed in [31], where it is shown that using posets, semilattices and domains for the carriers X and A and various functors in place of the powerset (Remarks 4.6 and 6.10) allows divers idioms of induction to be expressed in a unified style. The most difficult steps in this generalisation turn out to be the innocent pasting together of attempts in Proposition 1.4 and the universal quantifier in the auxiliary predicate ψ used to prove Proposition 1.7a.

Often the validity of an induction principle is demonstrated not by showing directly that the sub-argument relation is well founded, but by assigning a complexity measure such as the length of a list or the height of a tree. In proving that a recursive program terminates, this is known as a loop variant. This method implicitly uses Proposition 1.7a. When ω (ℕ with the strict arithmetical order) is inadequate, lexicographic products are brought in, and finally general ordinals. Ordinals are useful because they admit a peculiar kind of arithmetic (Proposition 7.5), into which crude but efficient translations of syntax can be made.

Definition 1.6 Let (X, ≺^{X}) and (Y, ≺^{Y}) be carriers with binary relations. Then a function f : X → Y satisfying

∀x, x′. x′ ≺^{X} x ⇒ f(x′) ≺^{Y} f(x)

we shall call strictly monotone. Constant functions are not strictly monotone, because of irreflexivity. Identities and composites are, so we have a category Wfr.

For any predicate ϕ on X, we say that x is hereditarily ϕ if all of its descendants satisfy ϕ, i.e.

(Hϕ)(x) =^{def} ∀y. y ≺ ≺ x ⇒ ϕ(y).

Proposition 1.7

(a) Strictly monotone functions reflect well-foundedness, i.e. if ≺^{Y} is well founded then so is ≺^{X} in the notation of the Definition (Osius 6.3a).

(b) In particular, any relation which is sparser than a well founded relation is itself well founded.

(c) If (X, ≺^{X}) and (Y, ≺^{Y}) are well founded then so is the relation on X×Y given by (x′, y′) ≺^{(X×Y)} (x, y) if x′ ≺^{X} x ∧ y′ ≺^{Y} y, justifying simultaneous induction.

(d) If ϕ satisfies the premise of the induction scheme then Hϕ satisfies the strict premise, i.e. ∀x. [∀x′. x′ ≺ x ⇒ Hϕ(x′)] ⟺ Hϕ(x).

(e) The transitive closure of a well founded relation is well founded.

(f) Well-foundedness is a local property in the sense that (X, ≺) is well founded iff (the relation restricted to) X ↓ x is well founded for all x ∈ X.

Proof In (a), the induction rule for a predicate ϕ on X is proved using that for ψ(y) ≡ ∀x ∈ X. [f(x) = y ⇒ ϕ(x)] on Y. See [30] for more details. □

Remark 1.8 The ideas in this paper are inevitably set-theoretic, and the word “set” arises in three senses:

(a) The mainstream meaning is a naked mathematical object waiting to be clothed with some kind of structure. It may always be replaced with any bijective copy. In other subjects the structure might consist of algebraic operations or a topology, but here it is a binary relation (≺). Apart from the fact that well-foundedness involves quantification over (typed) predicates, ordinals are no different from groups. A set in this sense might be a type in a model of simple type theory [17, 30] or an object of an elementary topos [13, 2]. We shall use the word “carrier” for something which is intended to be an arbitrary such object and not necessarily have a set-theoretic structure.

(b) In distinction to a “proper class”; this sense is indicated by the adjective “admissible.”

(c) An ∈-structure in the manner of set theory. Sections 2 and 3 develop a mathematical structure (ensembles) which is meaningful in any elementary topos and provides an interpretation for set-theoretic language. A set in this sense is an element x ∈ X of an ensemble (Remark 3.2).

In view of the fact that all but a few of the objects mentioned in this paper can necessarily be interpreted in the third sense, this is the convention which is adopted here. Beware that this goes against the grain for me, so there is a danger that you will mis-interpret my use of language if you attribute set-theoretic meaning to it too readily. In particular, an individual element x ∈ X may represent a set here, not by virtue of some God-given nature, but because other elements y ∈ X of the structure satisfy y ≺ x. If some of these other elements are taken away (because we consider a substructure U ⊂ X), the set represented by x changes. An example of a statement prone to mis-interpretation is that, classically, any subset of an ordinal is an ordinal (Remark 7.7).

Remark 1.9 Cantor’s ordinals, like ours, were order types — the carrier could be anything we please — but John von Neumann [34] and set theorists following him said that the order had to be membership. For them, ω2 does not exist without the axiom of replacement [6, 19, 26], whereas for us it is easy to make it “by hand” as the even numbers followed by the odd ones.

In categorical terms, replacement says that the topos of sets is (externally) complete and cocomplete with respect to diagrams indexed by its hom-sets. Proposition 3.18 explains how this formulation relates to the traditional one in set theory.

We do not need replacement to define ordinals in any of the senses we discuss in this paper. But ...

Remark 1.10 Consider the following converse to 1.7a. For any given well founded relation (X, ≺), is there necessarily an ordinal α and a strictly monotone function X → α? Theorem 7.10 and Remark 8.10 show that there is. The least (in whatever sense is meaningful) such ordinal is called the rank of (X, ≺).

There is a well known formula for the rank, which appears to be the only way of constructing it in the plump sense (Theorem 7.10), but this uses replacement. However, it is clear that we may find the transitive closure of any relation within Zermelo’s set theory, simple type theory or in an elementary topos. We shall show that extensionality (Theorem 2.11) and hereditary directedness (Corollary 8.9) can also be imposed by means of the basic machinery alone.

Remark 1.11 Whether we accept Cantor’s presentation or von Neumann’s, sets and ordinals behave alike. Indeed to treat sets as a weak kind of ordinal completes the “free algebra” picture of André Joyal and Ieke Moerdijk [15] which we discuss in Section 7.

This work primarily considers what it is to be an ordinal; only in passing does it discuss the collection of all ordinals. The remarkable thing about ordinals, though, is that the class of all ordinals, equipped with a suitable relation, closely resembles the individuals, except for the question of size (the Burali-Forti paradox). This issue may be traced to an algebraic difference: the join operations of the totality are everywhere defined, whereas those of the individuals are partial. [30, 31] suggest how individual ordinals may be treated as partial algebras analogous to the total ones, without the foundational machinery which Joyal and Moerdijk need.

Remark 1.12 Foundational questions are inevitably asked here.

The development may be made within higher order (“simple”) type theory [17] or an elementary topos. Quantification and the formation of subsets are always bounded, though the bound is not always stated explicitly. When we occasionally talk about “all ordinals” we intend a scheme of assertions; the class of ordinals, when we mention it, is to be understood in the traditional ad hoc fashion, like the category of groups. Joyal and Moerdijk, on the other hand, discuss classes of ordinals throughout, so they need to extend the ambient logic to handle classes. (Worse than this, the universal property of their class-algebras involves quantification over the super-class of class-algebras.)

The axiom of infinity is, of course, needed for ω to exist, but not for any of the main definitions or constructions.

For me it is important not to be specific about which model is to be “the” universe of mathematics. I am interested in synthetic domain theory, which postulates exotic universes in which every function is to be computable, just as there are models of synthetic differential geometry where all functions are continuous. At the present stage of research in these subjects there is no “preferred” model — and I have no intention of making a choice in the future. Many other foundational techniques, such as forcing and sheaf theory, also make use of ordinary mathematical results in extraordinary circumstances. The purpose of this paper is to make ordinals (and set-theoretic notation) available in such worlds.

After finishing this paper I tracked down Dimitry Mirimanoff’s paper [19a]. This has a clear account of well-foundedness (or otherwise) of set membership and anticipates von Neumann’s representation of ordinals using the element relation. It states the Burali-Forti paradox in the form of Corollary 2.6 and introduces the notion of rank (Theorem 3.10), although there is no proof of the general recursion theorem (Proposition 1.4) or discussion of the axiom of replacement.

2 Ensembles and simulations This section develops the structure underlying set theory without its ontology; that is, the raw material is already present (the objects of a topos or types in a model of simple type theory), and the “sets” are identified up to isomorphism by their structure and relationships to each other. These relationships are membership and inclusion, which we shall characterise in an order-theoretic fashion. We shall also prove Mostowski’s theorem without Replacement.

The preliminary results were proved by Gerhard Osius [22] and reproduced in [13, §9.2], but our Theorem 2.11 is original. Osius used a diagram-chasing style; in particular he defined ϵ to be extensional if the exponential transpose \overline{ϵ} : X → P(X) by x ↦ \{y : y ϵ x\} is mono. This operation “parses” an object x as the set-forming operation applied to the “argument-list” {y : y ϵ x} (see [30] for a treatment of parsing for free algebras for algebraic theories without equations, with application to the unification algorithm).

Definition 2.1 A binary relation ≺ is extensional if

∀x, y. \begin{matrix}∀z. z ≺ x ⇔ z ≺ y \\ = & ext \\ x = y \end{matrix}

An ensemble is a carrier together with an extensional well founded relation. We shall write ϵ (or ∈) for such a relation, but note that ϵ is used in this section for any ā priori extensional relation, which is sometimes that on X but sometimes on Y.

Examples 2.2 The following are ensembles:

(a) ∅, P∅, P(P∅), P(P(P∅)), P(P(P(P∅))), P(P(P(P(P∅)))) and so on under the membership relation; classically they have respectively 0, 1, 2, 4, 16 and 65536 elements and 0,

{∅, {∅}}  {{∅}}
[figure]
{∅}

[figure]

∅

0, 1, 4, 32 and 524288 instances of the ∈ relation. We see that P(P(P∅)) is not in fact a tree, as the bracket notation for sets would suggest.

(b) Any initial segment (Definition 1.6) of an ensemble (Osius 6.3b).

(c) ℕ with the successor relation; the numerals are those implicit in Ernst Zermelo’s formulation of the axiom of infinity [36]: 0 = ∅, 1 = {∅}, 2 = {{∅}}, 3 = {{{∅}}}, ..., i.e. n + 1 = {n}.

(d) ω (ℕ with the strict arithmetic order), the numerals being the von Neumann ordinals [34]: 0 = ∅, 1 = {∅}, 2 = {∅, {∅}}, 3 = {∅, {∅}, {∅, {∅}}}, ..., i.e. n + 1 = n ∪ {n}.

(e) ℕ, with n ϵ m if the nth bit is 1 in the binary expansion of m. This consists of (codes for) the hereditarily finitely enumerated sets. In particular ∅ = 0, {n} = 2^{n}, P(n) = 2^{n+1} − 1 and the lattice operations are given bitwise. The iterated powersets are coded as 0, 1, 3, 15, 65535, ..., the Zermelo numerals as 0, 1, 2, 4, 16, 65536, ... and the von Neumann ordinals as 0, 1, 3, 11, 2059. (This example is due to Wilhelm Ackermann.)

(f) John Conway’s games [5] generalise ensembles, with two element relations; the premise of the extensionality axiom is that the children of both kinds agree. Richard Dedekind’s construction of the real numbers as cuts of the rationals is shown to be included.

(g) Process algebra generalises further to a family of relations labelled by “actions”; extensionality is known as bisimulation and well-foundedness corresponds to termination. Nonterminating processes are also of interest, and Peter Aczel [1] has generalised set theory accordingly.

Examples 3.7, 4.2 and 6.3 show the effect of intuitionistic logic, plumpness and directedness on these examples, and on the numerals 2 and 3 in particular; 0 = ∅ and 1 = P(∅) = {∅} stay the same.

Andrzej Mostowski [21] showed that any extensional well founded relation is isomorphic to the membership relation on a unique set, by the recursive formula

f(x) = {f(x′) : x′ ≺ x},

but this approach relies on the axiom of replacement, cf . Theorem 7.10.

Eliminating the set-brackets from this equation, we have what categorists will recognise as almost the definition of a discrete fibration:

Definition 2.3 Let (X, ≺) and (Y, <) be carriers with binary relations and f : X → Y a strictly monotone function, i.e. x′ ≺ x ⇒ f(x′) < f(x). If the following “lifting” property holds:

∀x. ∀y′. [y′ < f(x) ⇔ ∃x′. x′ ≺ x ∧ y′ = f(x′)]

then (motivated by process algebra) we say that f is a simulation.

[figure: x′; ≺; x; y′; f; <; f(x); f]

An injective simulation is exactly the inclusion of a initial segment. Osius, who only considered simulations between ensembles, called these maps inclusions (§6) and defined them by the equation \overline{<} ∘ f = P(f) ∘ \overline{≺}:

[figure: P(X); P(f); P(Y); X; \overline{≺}; f; Y; \overline{<}]

This equation says that f is a homomorphism of co-algebras for the covariant powerset functor, which is the idea used in [31].

Lemma 2.4 Let X →^{f} Y →^{g} Z be strictly monotone functions between carriers with binary relations. Then

(a) If both f and g are simulations then so is g ∘ f.

(b) If f is surjective and g ∘ f is a simulation, then g is also a simulation.

(c) The pullback of a simulation against any strictly monotone function is a simulation. □

Lemma 2.5 Let (Y, ϵ) be an ensemble and f, g : (X, ≺) ⇉ (Y, ϵ) two simulations. Then f = g. (Osius 6.5)

Proof (X, ≺) is well founded by Proposition 1.7a, so we shall show that f(x) = g(x) by induction on x ∈ X. Let y ϵ f(x), so by the lifting property for f there is some x′ ≺ x with y = f(x′). By the induction hypothesis y = g(x′), and since g is strictly monotone y ϵ g(x). Thus ∀y. y ϵ f(x) ⇒ y ϵ g(x) and the converse is similar; so f(x) = g(x) by extensionality. □

Hence extensionality, which has a local flavour to it, is equivalent to a global property, rigidity. This is closely related to the Russell and Burali-Forti paradoxes. It depends crucially on the use at several points in the argument of equality as an induction predicate. It is interesting to note that Cesare Burali-Forti got the definition of well-foundedness wrong in his original paper [3], but that the argument remained valid when this was corrected, and was subsequently used in other logical systems. So the idea has some claim to be a real part of the mathematical world. However it is a feature which will have to be eliminated from the theory of ordinals if this is to be reformulated for weaker fragments of logic such as in computation, where we expect to find “ordinals” for which the successor function has a fixed point. (The Lemma and Corollary do, however, survive the generalisation.)

Corollary 2.6 Ensembles have no automorphisms apart from the identity. Indeed, a well founded relation is extensional iff there is no nontrivial isomorphism between two initial segments. □

Lemma 2.7 Let (X, ≺) be well founded and f : (X, ≺) → (Y, <) be a surjective simulation. Then (Y, <) is also well founded.

Proof Let ϕ be a predicate on Y and y = f(x). The induction hypothesis is

∀y′. y′ < f(x) ⇒ ϕ(y′) ≡ ∀y′. [∃x′. x′ ≺ x ∧ y′ = f(x′)] ⇒ ϕ(y′)
≡ ∀y′. ∀x′. [x′ ≺ x ∧ y′ = f(x′) ⇒ ϕ(y′)]
≡ ∀x′. x′ ≺ x ⇒ ϕ(f(x′))

Suppose now that ϕ satisfies the premise of the <-induction scheme. Then by ≺-induction on X for ϕ ∘ f, we have ∀x. ϕ(fx), whence ∀y. ϕ(y) by surjectivity. □

Lemma 2.8 Now let (X, ϵ) be an ensemble and f : (X, ϵ) → (Y, ≺) be a simulation. Then f is an isotomy, i.e. it induces an isomorphism X ↓ x ≅ Y ↓ f(x) for each x ∈ X.

Proof Fix x_{0} ∈ X and write ≺ ≺ and ϵ ϵ for the transitive closures of the relations. We may restrict attention to the initial segment Y′ = Y ↓ f(x_{0}). Since it is a simulation, f is surjective onto Y′: any y ≺ ≺ f(x_{0}) has some lifting x ϵ ϵ x_{0} with y = f(x). Lemma 2.7 now justifies induction on y ∈ Y′, by which we prove that

∃!x. x ϵ ϵ x_{0} ∧ y = f(x).

Suppose that x_{1}, x_{2} ϵ ϵ x_{0} are liftings of y ≺ ≺ f(x_{0}), i.e. y = f(x_{1}) = f(x_{2}). Let x′_{1} ϵ x_{1} and put y′ = f(x′_{1}). By the induction hypothesis, y′ ≺ ≺ f(x_{0}) has a unique lifting, and this is x′_{1} ϵ ϵ x_{0}. Since f is a simulation, there is a lifting x′_{2} ϵ x_{2} of y′ ≺ f(x_{2}). But then x′_{2} ϵ ϵ x_{0} is a lifting of y′ ≺ ≺ f(x_{0}), so x′_{1} = x′_{2} ϵ x_{2}. Thus ∀x′. x′ ϵ x_{1} ⇒ x′ ϵ x_{2} and the converse is similar, so by extensionality x_{1} = x_{2}. □

Corollary 2.9 Let (X, ϵ) be an ensemble and f : (X, ϵ) → (Y, ≺) be a simulation. Then f is injective and identifies X with a initial segment of Y. If both X and Y are ensembles then f is unique (Osius, 6.1).

Proof Let x_{1}, x_{2} ∈ X with f(x_{1}) = f(x_{2}). Then f restricts to isomorphisms X↓x_{1} ≅ Y ↓f(x_{1}) = Y ↓ f(x_{2}) ≅ X ↓ x_{2} by Lemma 2.8. Hence x_{1} = x_{2} by Corollary 2.6. □

Definition 2.10 Write Wfib for the category of well founded relations and simulations, and Ens ⊂ Wfib for the full subcategory of ensembles. We have shown that Ens is a (class) preorder, so for ensembles X and Y, write X ⊴ Y if there is a morphism between them, i.e. X is (uniquely) isomorphic to a initial segment of Y. We shall treat Ens as a category, preorder or (class) poset as convenient.

Now we prove a categorical form of Mostowski’s theorem.

Theorem 2.11 Ens is a reflective subcategory of Wfib.

That is, for any carrier (X, ≺) with a well founded relation,

(E, ϵ) = X/∼ ......................^{h} (E′, ϵ′)
[figure: g]
(X, ≺)^{f }

there is an ensemble (E, ϵ) and a simulation f : X → E, with the universal property that, for any simulation g : X → E′, where (E′, ϵ′) is an ensemble, there is a unique simulation h : E → E′ such that g = h ∘ f.

Moreover f, which is called the unit of the reflection, is surjective.

Proof First consider the universal property. Extensionality of E′ at g(x) and g(y), where x, y ∈ X, says

[∀e′. e′ ϵ′ g(x) ⇔ e′ ϵ′ g(y)] ⇒ g(x) = g(y).

Writing x ∼ y in place of g(x) = g(y), the simulation property gives

(∀x′ ≺ x. ∃y′ ≺ y. x′ ∼ y′) ∧ (∀y′ ≺ y. ∃x′ ≺ x. x′ ∼ y′) ⇒ x ∼ y

which, in process algebra, is called the bisimulation relation.

By simultaneous recursion (Proposition 1.7c), this defines a function (∼) : X × X → Ω which is the sparsest such relation, and has equality instead of implication. By induction on x, ∼ is reflexive, and by simultaneous induction it is symmetric. Similarly, by a three-fold induction, we can show that

\begin{matrix}∀x′ ≺ x. ∃y′ ≺ y. x′ ∼ y′ \\ ∀y′ ≺ y. ∃z′ ≺ z. y′ ∼ z′ \end{matrix} \} ⇒ ∀x′ ≺ x. ∃z′ ≺ z. x′ ∼ z′,

so it is transitive. Let f : X ↠ E = X/∼ ⊂ P(X) be the quotient by this equivalence relation. Now for e, e′ ∈ E define

e′ ϵ e if ∃y, y′. (e′ = f(y′) ∧ e = f(y) ∧ y′ ≺ y)

so that f is strictly monotone. For the simulation property, if e′ ϵ f(x), where e′ = f(y′), f(x) = f(y) and y′ ≺ y, then x ∼ y, so there is some x′ ≺ x with x′ ∼ y′, so e′ = f(x′). Well-foundedness of (E, ϵ) now follows from Lemma 2.7.

For extensionality, ∀e′. [e′ ϵ f(x) ⇔ e′ ϵ f(y)] is equivalent by the above argument to x ∼ y, i.e. f(x) = f(y). Finally x ∼ y ⇒ g(x) = g(y), so the mediator h : E → E′ is well defined; it is a simulation by Lemma 2.4b. □

A simpler proof, based on iterated image factorisation, will be given in [31].

Corollary 2.12 Ens has unions, ⋃, of arbitrary families and intersections, ⋂ of inhabited families.

Proof Coproducts (disjoint unions) and intersections in Wfib are computed for the carriers. Since the inclusion Ens ⊂ Wfib is a right adjoint it preserves limits, so intersections in Ens are also computed for the carriers. Left adjoints preserve coproducts, so the union in Ens is the extensional quotient of the disjoint union. □

Remark 2.13

(a) The axiom of replacement is needed in the ambient world to form infinitary unions.

(b) The colimit of a filtered diagram of ensembles and simulations may be computed for the carrier, as for finitary algebraic theories.

(c) Osius (6.6) used recursion to construct the set-theoretic binary intersection X ↩ X ∩Y ↪ Y first, and then X ∪ Y as the pushout of this. The proof that this is extensional uses partial functions X ⇀ Y; a simpler form of Osius’ argument in given in [31].

(d) Binary intersection distributes over arbitrary union. □

The general recursion theorem (Proposition 1.4) specialises from well founded relations to ensembles, but we shall present another form of it, similar to transfinite recursion on ordinals, in Theorem 5.9a.

3 Recovering set theory The construction of type theory (cartesian products, functiontypes, etc.) out of set theory is familiar. In this section we shall do the converse: given an ambient model of simple type theory (elementary topos E) we try to “fill it with sets.”

Remark 3.1 An ensemble is a model of a fragment of set theory, specifically of the axioms of extensionality and intuitionistic foundation. In set theory, a set cannot stand alone: its transitive closure is needed to make public the private framework of elements of ... elements which is hidden behind it. In our treatment ensembles play this rôle: (X, ϵ) is the framework and, for a “set” x_{0} ∈ X in it, ∥x_{0}∥ =^{def} {y ∈ X : y ϵ x} is the substance of the set itself.

The word “transitive” is used in set theory to mean that the grandchildren and great-grandchildren of a particular set are also children, but the great-grandchildren need not be grandchildren. Since we have a different way of dealing with the framework, we do not need this meaning. On the other hand, an ensemble whose relation is transitive in the order-theoretic sense (hereditarily, as the set-theorists might say) is the simplest notion of ordinal, so we shall employ this usage.

Remark 3.2 An actual “set” can be coded in three ways in such a model:

(a) either as an element x_{0} ∈ X of an ensemble (X, ϵ),

(b) or as the slice ensemble X ↓ x_{0}, in which x_{0} is the unique orphan,

(c) or as the ensemble^{3} (X ↓ x_{0}) \ {x_{0}} together with its subset ∥x_{0}∥ =^{def} {x : x ϵ x_{0}}. Osius (7.14) uses this definition.

The power of set theory comes from the inter-play amongst these three codings. But this is also what makes it confusing, because the usual type disciplines of mathematics are broken: for example in the assertion

γ ∈ β ∈ α ⇒ γ ∈ α

γ goes from being a grandchild to a child of α. In general the elements of an ensemble are not themselves ensembles, but they are when the transitive law holds.

For elements x, y of an ensemble (X, ≺),

x ∈ y means x ≺ y, and
x ⊂ y means ∥x∥ ⊂ ∥y∥ i.e. ∀z ∈ X. z ≺ x ⇒ z ≺ y.

We say that a subset U ⊂ X of the carrier is representable if U = ∥x∥ for some x ∈ X, which is unique by extensionality.

Remark 3.3 Any inclusion X ⊂ Y between transitive sets, understood in the set-theoretic sense, is the inclusion of an initial segment (and hence a simulation) when seen in terms of ensembles. Corollary 2.9 showed that every simulation to Y is of this form, i.e. that (in this straightforward case) simulation captures the set-theoretic subset relation.

This result makes it possible to extend the membership and subset relations defined above for a common ambient ensemble to free-standing “sets” (X, ϵ^{X}, x_{0}) and (Y, ϵ^{Y} , y_{0}):

(X, ϵ^{X}, x_{0}) ∈ (Y, ϵ^{Y} , y_{0}) if i(x_{0}) ϵ^{Z} j(y_{0})
(X, ϵ^{X}, x_{0}) ⊂ (Y, ϵ^{Y} , y_{0}) if ∀z ∈ Z. z ϵ^{Z} i(x_{0}) ⇒ z ϵ^{Z} j(y_{0})

for some simulations i : X ⊴ Z and j : Y ⊴ Z, such as the union Z = X ∪ Y (Corollary 2.12). In the first case, if X = X ↓ x then Z = Y will do, but the results of the previous section ensure that the choice of (Z, ϵ^{Z}) is unimportant.

3We may re-adjoin the deleted element x_{0} as, for x ∈ X ↓ x_{0}, it is decidable whether x = x_{0}. This is because ϵ is irreflexive.

Lemma 3.4 Let (X, ϵ^{X}, x_{0}), (Y, ϵ^{Y} , y_{0}) and (Z, ϵ^{Z}, z_{0}) be sets. Then

(X, ϵ^{X}, x_{0}) ∈ (Y, ϵ^{Y} , y_{0}) ⟺ (X ↓ x_{0}, ϵ^{X}, x_{0}) ∈ (Y, ϵ^{Y} , y_{0})

identifying x_{0} with the same y ϵ y_{0} ∈ Y, and it suffices to embed them in Z = Y. Similarly for ⊂, although ∥x_{0}∥ need not be representable in Y itself. Hence the following are equivalent:

• (X, ϵ^{X}, x_{0}) ⊂ (Y, ϵ^{Y} , y_{0}) ∧ (X, ϵ^{X}, x_{0}) ⊃ (Y, ϵ^{Y} , y_{0});

• X ↓ x_{0} ≅ Y ↓ y_{0} in Ens;

• (X, ϵ^{X}, x_{0}) ∈ (Z, ϵ^{Z}, z_{0}) identifying x_{0} with z ϵ^{Z} z_{0} iff (Y, ϵ^{Y} , y_{0}) ∈ (Z, ϵ^{Z}, z_{0}) identifying y_{0} with the same z.

In other words the ensemble (Z↓z_{0}, ϵ^{Z}) is isomorphic to the class of equivalence classes of hereditary elements of (Z, ϵ^{Z}, z_{0}). □

Notation 3.5 We write Ens for the class of equivalence classes of “sets” equipped with the ∈ relation. The Lemma says that this is the union of all ensembles, i.e. the (inadmissible) colimit of the filtered diagram id : Ens → Ens (cf . Remark 2.13b). In the sense suggested by Proposition 1.7f, Ens is well founded. Beware that the elements of Ens are not ensembles but sets.

Theorem 2.11 may also be used to develop the type-theoretic structure of the von Neumann Hierarchy. The idea is to use the powerset to add some of the missing sets to a given fragmentary model. Recall that \overline{ϵ}(x) = \{y : y ϵ x\}.

Proposition 3.6 Let (X, ϵ^{X}) be an ensemble. Then the relation

U ϵ^{P(X)} V ⟺ ∃x. U = \overline{ϵ^{X}}(x) ∧ x ∈ V

makes P(X) an ensemble such that \overline{ϵ^{X}} : X ⊴ P(X).

Proof Osius (6.8) defined \overline{ϵ^{P(X)}} = P(\overline{ϵ^{X}}), and this will also be used in [31].

We may also use Theorem 2.11. First consider the disjoint union X + P(X) with the relation ≺ defined as follows:

x′ ≺ x if x′ ϵ x
x ≺ U if x ∈ U
U ≺ x, U ≺ V  never

To show that this is well founded, consider a predicate satisfying the premise of the induction scheme on the union, and in particular on X. Then by well-foundedness of X the predicate holds throughout X and its subsets. One further application of the premise gives the predicate on P(X).

Let (Y, <) be the extensional quotient, so X ↪ X + P(X) ↠ Y is a simulation (Lemma 2.4a) and hence injective (Proposition 2.9). By extensionality, the function P(X) ↪ X +P(X) ↠ Y is a bijection (it has no structure to preserve). The only non-trivial identifications are x ∼ {x′ : x′ ϵ x}.

We could have made the extensional quotient do even more of the work by taking the class of raw formulae instead of P(X), since formulae are inter-provable iff they are extensionally equal. □

Examples 3.7

(a) The set Ω = P(P(∅)) of truth values is an ensemble, where the proposition ϕ is identified with the set {∅ : ϕ} (this is the subset of the singleton {∅} defined by comprehension of the predicate ϕ) and in particular ⊥ (falsity) corresponds to ∅. The membership relation is ψ ϵ ϕ if ¬ψ ∧ ϕ: notice that this is much sparser than the reflexive relation of containment (implication).

(b) The ensemble P(P(P(∅))) consists of subsets U ⊂ Ω of propositions, in which ϕ is identified with the set {ψ : ¬ψ ∧ ϕ} = {⊥ : ϕ}. For U, V ⊂ Ω, we have U ϵ V iff ∃ϕ ∈ Ω. U = {⊥ : ϕ} ∧ ϕ ∈ V. □

Proposition 3.8 Let X be an ensemble. Then P(X), with x ↦ {x′ : x ϵ x}, is the ⊴-least ensemble (Y, <) with h : X ⊴ Y for which the axiom of comprehension holds in the following three forms:

(a) unboundedly on X: for any predicate ϕ on X, there is a unique y ∈ Y such that

∀y′. y′ < y ⇔ ∃x′. y′ = h(x′) ∧ ϕ(x′);

i.e. every U ⊂ X is representable in P(X);

(b) boundedly on Y: for y_{0} ∈ Y and ψ a predicate on Y, there is a unique y ∈ Y such that

∀y′. y′ < y ⇔ [y′ < y_{0} ∧ ψ(y′)];

(c) boundedly on X: for x_{0} ∈ X and ϕ a predicate on X, there is a unique y ∈ Y such that

∀y′. y′ < y ⇔ ∃!x′. [y′ = h(x′) ∧ x′ ϵ x_{0} ∧ ϕ(x′)].

Unbounded comprehension on Y is forbidden by Cantor’s Theorem. Proof The assignments

X ↾ ϕ = {x : ϕ(x)}
y_{0} ↾ ψ = {x′ : x′ ∈ y_{0} ∧ ψ(x′)}
x_{0} ↾ ϕ = {x′ : x ϵ x_{0} ∧ ϕ(x′)}

satisfy the axioms, and are unique by extensionality. If Z is another ensemble satisfying unbounded comprehension on X, so P(X) ↪ Z, then Y ⊴ Z by the universal property of the extensional quotient. □

Examples 3.9 Let (X, ϵ) be an ensemble and x, y ∈ X. Then the following subsets are representable in P(X):

(a) empty set, ∅;

(b) singleton, {x};

(c) unordered pair, {x, y};

(d) binary union, x ∪ y ≡ {z ∈ X : z ϵ x ∨ z ϵ y};

(e) thin successor: x ∪ {x};

(f) internal union: union(x) = {z ∈ X : ∃y ∈ X. z ϵ y ϵ x}.

In P^{2}(X) we have x ∪ y = union({x, y}). □

Lemma 3.10 The ordered pair defined by Kazimierz Kuratowski and Norbert Weiner,

⟨x, y⟩ = {{x}, {x, y}},

is representable in P^{2}(X) and satisfies

{{x}, {x, y}} = {{x′}, {x′, y′}} ⟺ x = x′ ∧ y = y′.

So x × y = {⟨x′, y′⟩ : x′ ϵ x ∧ y′ ϵ y} is representable in P^{3}(X) and is the product.

Proof Since {u, v} ⊂ Y ⇔ u ∈ Y ∧ v ∈ Y, the equation {a, b} = {c, d} resolves into a disjunction of sixteen cases, fourteen of which reduce to a = b = c = d and the other two give (a = c ∧ b = d) ∨ (a = d ∧ b = c). The result follows by applying this to the pair formula. □

Remark 3.11 By considering Ω×Ω in the presheaf topos Set^{•→•}, it is necessary to use the double powerset, and (by enumerating terms) this is the only way of coding pairs with bracket depth at most two. □

Remark 3.12 P(X) consists of all subsets provided by the ambient world E. In building a hierarchy, the axioms of powerset and comprehension (for the new model) play different rôles. Let x_{0} ∈ X be a “set” already present in the model X.

(a) Let ϕ be a predicate ranging over ∥x_{0}∥. Then comprehension says that subset U = {y ∈ X : y ϵ x_{0} ∧ ϕ(y)} is to be representable in (the next attempt X′ at) the model. The predicates ϕ to which we apply comprehension could be restricted to some subclass. Considering only the decidable ones gives a Boolean model. By admitting those predicates which are definable in terms of X we can build Kurt Gödel’s constructible hierarchy L [9] instead of the full von Neumann hierarchy V.

(b) Put p(x_{0}) = {u ∈ X : ∀z ∈ X. z ϵ u ⇒ z ϵ x_{0}} for the collection of subsets which are already representable; then the powerset axiom says that p(x_{0}) is to become representable. To ensure that p(x_{0}) is a lattice we must use some form of comprehension over an underlying logic.

Definition 3.13 A Zermelo ensemble X is one in which empty set, pairs, unions, powerset and comprehension (over predicate calculus) for elements of X are already representable within X. That is, Ernst Zermelo’s axioms [36] plus (intuitionistic) Foundation, but not necessarily Choice or Infinity, hold.

Proposition 3.14 Let (X, ϵ) be an ensemble. Then

(a) there is a (small) category X with obX =^{def} X such that ∥−∥ : X → E is a full and faithful functor, i.e. a morphism x → y in X is a function ∥x∥ → ∥y∥; (E is the ambient topos.)

(b) if (X, ϵ) is a Zermelo ensemble then X is an (internal) elementary topos and the functor ∥−∥ : X → E creates limits, colimits and function types. That is, for any diagram D in X, if the limit L (etc.) of the image diagram ∥D∥ exists in E, then there is a structure S in X, which is unique (up to unique isomorphism) such that ∥S∥ ≅ L, and, moreover, S is the limit (etc.) of D in X.

(c) if it satisfies comprehension for arbitrary predicates in E, i.e. all subsets are representable, then ∥−∥ is a logical functor, i.e. the powersets in X and E also agree;

(d) if it satisfies the axiom of infinity, i.e. there is some x ∈ X with ∅ ϵ x and ∀n. n ϵ x ⇒ {n} ϵ x, then X has a natural numbers object and this too is preserved by the functor. □

Remark 3.15 For the analogous construction with Ens instead of X, let S be the category whose objects are sets (X, ϵ, x_{0}) and whose morphisms (X, ϵ^{X}, x_{0}) → (Y, ϵ^{Y} , y_{0}) are functions {x ∈ X : x ϵ^{X} x_{0}} → {y ∈ Y : y ϵ^{Y} y_{0}}. Then S is an elementary topos and the functor ∥−∥ : S ↪ E is full and faithful, logical and creates all of the other structure. Osius chose obS = Ens, identifying bisimilar sets, but this is unnecessary from the point of view of category theory. Our category is equivalent to his, but has lots of (harmless) isomorphic copies of what are, in terms of extensionality, the same set. The category S is large (it has a proper class of objects) but locally small (there is an admissible set of morphisms between any two objects).

The functor S ↪ E compares set theory with topos theory. There are various circumstances in which they are equivalent.

(a) The crudest is to impose the axiom of choice in E, so that every object carries the structure not just of a “set” but of a (classical) ordinal.

(b) If E was itself obtained from a model of set theory then S ≃ E and Ens is isomorphic to the model.

(c) Similarly, if E is a model of pure type theory, so every object occurs as a subobject of some type-expression involving ∅, products and powersets but not any base types, then again every object has a set-theoretic representation.

(d) Base types may be added by introducing their terms as ur-elements.

Definition 3.16 We might say that a topos E satisfies the axiom of foundation if S ≃ E. For Osius (4.4) this was an axiom: “any set [object of E] is a subset of a transitive set [ensemble].”

Definition 3.17 An ensemble (X, ϵ) obeys the axiom of replacement if for every “set” x_{0} ∈ X and (externally defined) function f : ∥x_{0}∥ → X the subset {f(i) : i ∈ ∥x_{0}∥} ⊂ X is representable. This is traditionally expressed as a scheme ranging over binary predicates ϕ(i, x) which are functional in i ∈ ∥x_{0}∥. (See also Osius 9.4.)

To the categorist or algebraist, this definition simply appears to assert the existence of the image of any function, but this can be built out of equivalence classes. However there are recursive type equations whose smallest solution classically has cardinality ℶ_{ω} = ⋃_{n∈ℕ} P^{n}(∅). For example any ensemble X may be embedded in a Zermelo ensemble ⋃_{n∈ℕ} P^{n}(X), and there are similar problems in other subjects such as domain theory. The existence of these objects cannot be deduced from Zermelo’s axioms, but needs replacement. So what does replacement mean?

Proposition 3.18 The following are equivalent for a Zermelo ensemble X:

(a) the ensemble (X, ϵ) satisfies replacement;

(b) the union of any I-indexed family of representable subsets is representable, where I = ∥x_{0}∥ for some x_{0} ∈ X;

(c) for any family of sets x_{i} ∈ X indexed by any hom-set I = X (p, q), with p, q ∈ obX, there is a set u ∈ X and a family of injective functions ν_{i} : ∥x_{i}∥ ↪ ∥u∥;

(d) the category X has coproducts indexed by any such I;

(e) X has I-indexed products for any such I;

(f) X has colimits of any diagram-type I whose class of arrows is bijective with some X (p, q) with p, q ∈ obX;

(g) X has limits of any such type I;

(h) X has limits and colimits of any diagram-type which is a subposet of the lattice of subobjects of some p ∈ obX.

Proof For [a⇒b], [b⇒a] and [c⇒d],

⋃_{i∈I} x_{i} = union({x_{i} : i ∈ I})
{x_{i} : i ∈ I} = ⋃_{i∈I} {x_{i}}
∐_{i∈I} x_{i} = ⋃_{i∈I} ({i} × x_{i}) ⊂ I × ∥u∥

Since X is a cartesian closed category, I = X (p, q) ≅ X ({⋆}, q^{p}) is just another way of referring to an arbitrary set in the model.

For [d⇒b], Corollary 2.12 showed how to find the set-theoretic union of ensembles as a quotient of the disjoint union; for sets x_{i} ∈ (X_{i} ↓ x_{i}) and ⋃_{i} x_{i} ⊂ ⋃_{i} X_{i}.

Equivalence amongst parts (d–h) is shown by standard categorical techniques [30]. □ This suggests the following definition for category theory:

Definition 3.19 An elementary topos is said to satisfy replacement if it is (externally) complete and cocomplete for all diagrams indexed by its hom-sets. If the topos E obeys replacement then so do the topos S and class-ensemble Ens.

Question 3.20 In what (natural) circumstances does the functor S → E have adjoints? (It preserves limits and colimits, and, being logical, if it has one adjoint then it has both [13, page 34].) The general adjoint functor theorem appears to be of no help. We want to know whether an arbitrary object can be the set of (top-level) elements of some set-theoretic structure, but we have no way of knowing how big the ambient ensemble (transitive closure) needs to be, and this structure is not at all canonical.

However, if the adjoints do exist, and a suitable boundedness condition holds, then E is the category of sheaves for a topological groupoid in S. In fact it is a group since the right adjoint (the global sections functor) preserves coproducts. This suggests that a tighter connection between set theory and topos theory may be achieved by considering permutation models.

Conjecture 3.21 Every Grothendieck topos whose sheaves take values in a model of set theory is equivalent to a permutation model of set theory, and for localic toposes no permutations are needed.

Remark 3.22 Zermelo ensembles whose carriers are admissible objects of E, unqualified, with the axiom of infinity and with the axiom of replacement, provide possible formulations of various notions of inaccessible cardinals in a manner suitable for use in category theory. In fact the existence of a Zermelo ensemble is equivalent to the existence of an internal topos. Likewise a Zermelo ensemble with replacement corresponds to an internal topos which is complete in the above sense.

Bill Lawvere [18] aimed to remove the membership relation from set theory, but for a long time afterwards, toposes still had to be justified in terms of sets. To achieve agreement, the notion of elementary topos was compromised by such restrictions as the two-valued axiom. The difference between S and E is a mathematical question which we should consider with an open mind. Turning the tables on set theory, how can it can be altered to match toposes exactly?

4 Plumpness Often excluded middle can be eliminated from (abstract) mathematics merely by careful use of language, but the received account of the ordinals seems to depend rather heavily on it. This is ironic, considering that John von Neumann was rather more sympathetic to intuitionism than were the other founders of set theory. With hindsight, the cause of the difficulty was that β ⊴ α is confused classically with β ∈ α ∨ β = α. By introducing a new concept, which strengthens transitivity,^{4} we identify which relation should be used at each point in the traditional development, and excluded middle is no longer needed.

Since ordinals provide a generic proof by induction they must reflect the features of particular inductive arguments, so the theory is inevitably rather difficult: the definition of plumpness is recursive, and that of hereditary directedness is a bit complicated.

Definition 4.1 Let α be a set in an ensemble (X, ϵ). Then α is (a) plump if whenever β and γ are ordinals with γ ⊂ β ϵ α then γ ϵ α;

4In fact, [31] shows that plumpness is an instance of a generalised notion of extensionality rather than of transitivity. This explains why well-foundedness, transitivity and directedness are meaningful without extensionality but plumpness is not.

(b) hereditarily plump if its elements are plump, i.e. whenever β, γ and δ are ordinals with δ ⊂ γ ϵ β ϵ α then δ ϵ β;

(c) an ordinal if it is plump and its elements are ordinals (so it is hereditarily plump).

The question of whether a particular set actually possesses the property of being an ordinal is therefore a recursive one, and we shall have to prove that this recursion is well founded. We shall show that α is (hereditarily) transitive and so may be treated as an ensemble (Remark 3.2c).

Note that the subset γ in (a) is not ā priori representable. Taking it to be so gives yet another notion of ordinal, intermediate between transitive and plump [31], but we shall not discuss this.

Examples 4.2 ∅ is plump, as is any ϕ ≡ {∅ : ϕ} ∈ Ω. Also U ⊂ Ω is plump iff it is a lower subset, i.e. ∀ϕ, ψ ∈ Ω. (ψ ⇒ ϕ) ∧ (ϕ ∈ U) ⇒ ψ ∈ U. The plump numeral 2 is therefore Ω, and 3 is the set of lower subsets of Ω. □

Proposition 4.3 The recursive definition of plumpness is sound.

Proof We treat the question ϑ(α) of whether a given set α (in an ensemble X) meets the criteria for being an ordinal not as a predicate but as a value of type Ω (Remark 1.3).

First we establish that it suffices to take P(X) as the domain of definition of the function ϑ. The “sets”

V ⊂ b ϵ α W ⊂ d ∈ V

which arise in the recursive consideration of the question ϑ(α) (and more generally ϑ(U) for U ⊂ X) are all, at worst, subsets of X. In fact we define ϑ : E → Ω, where

E = {V ⊂ X : ∃a ∈ X. V ⊂ a} ⊂ P(X).

Using capitals for subsets of X and lower case letters for its elements, recall that

V ϵ U means ⋁_{d∈X} [d ∈ U ∧ ⋀_{e∈X}(e ∈ V ⇔ e ϵ d)]
V ⊂ b means ⋀_{e∈X}(e ∈ V ⇒ e ϵ b).

Now ϑ : E → Ω is to satisfy the equation

ϑ(U) = ⋀ {ϑ(∥b∥) ∧ ϑ(V) ⇒ V ϵ U : V ⊂ b ∈ U}
∧ ⋀ {ϑ(V) : V = ∥b∥ ∧ b ∈ U}.

This has a unique solution by the general recursion theorem (Proposition 1.4), so long as we can show that its sub-argument relation

V ≺ U if ∃b ∈ X. V ⊂ b ∈ U

is well founded on E.

Consider also the set F ⊂ P(X) × X × P(X) of triples (V, b, U) such that V ⊂ b ∈ U, with the relation

(V′, b′, U′) < (V, b, U) if U′ = V.

Then the projection π_{1} : (F, <) → (X, ϵ) is a strictly monotone function since b′ ϵ b, so (F, <) is well founded by Proposition 1.7a. The projection π_{0} : F → E is a simulation: if W ≺ V because W ⊂ c ∈ V, then (W, c, V) is a lifting of W to (V, b, U). It is surjective because V ⊂ a ∈ X, so (E, ≺) is also well founded by Lemma 2.7.

Finally, let h : X ⊴ Y. Then since subsets in P(X) agree with those in P(Y), the functions ϑ_{X} : E_{X} → Ω and ϑ_{Y} : E_{Y} → Ω agree on E_{X} ⊴ E_{Y}. Hence the notion of ordinal is independent of the ambient ensemble X and ϑ : Ens → Ω can also be defined. □

Lemma 4.4 Let α be an ordinal in an ensemble (X, ϵ). Then the restriction of ϵ to X ↓ α is transitive.

Proof We show by induction on z ∈ X ↓ α that x ϵ y ϵ z ⇒ x ϵ z. By the induction hypothesis, ∀w. w ϵ x ϵ y ⇒ w ϵ y, i.e. x ⊂ y ϵ z, so by plumpness x ϵ z. □

Remark 4.5 Putting γ = ⋃ {δ^{+} : δ ∈ γ} (Remark 5.4) in γ ⊴ β ∈ α ⇒ γ ∈ α, plumpness is equivalent to the principle that ordinals are closed under bounded unions. That is, if δ_{i} ϵ β ∈ α for i ∈ I then ⋃_{i} δ_{i} is (representable as) an element of α. In particular, since α is the ⊴-greatest element of α^{+}, the circularity in the definition of ordinals could be eliminated by defining the successors to be closed under unions. We did not adopt this approach because we intend to add a further condition (hereditary directedness, Section 6), thereby altering the effect of the plumpness condition whilst retaining its form.

Remark 4.6 Plumpness makes the relation ϵ a monotone function (ϵ) : X × X^{op} → Ω, where X is regarded as a poset under ⊴:

δ ⊴ γ ∧ γ ϵ β ∧ β ⊴ α ⇒ δ ϵ α.

Just as this paper made progress by dis-engaging ⊴ from ⪯, [31] takes the partial order on X to be ā priori independent of ⊴, and proving that, in the presence of extensionality, it has to be the subset relation induced by ≺.

Transitivity similarly makes (ϵ) : X ×X^{op} → Ω strictly monotone with respect to the irreflexive relation ϵ on X. Unfortunately this notion of ordinal — the simplest from the point of view of set theory — does not fit in to the pattern of [31].

Remark 4.7 Plumpness, unlike transitivity (Remark 3.2), is a stratified formula, i.e. it obeys the type discipline: β and γ are sets and α is a set of sets on both sides of the implication.

To illustrate that plumpness is not new (only newly recognised), we prove the

Theorem 4.8 Classically, the following are equivalent for a well founded relation:

(a) it is an ordinal,

(b) it is trichotomous,

(c) it is extensional and transitive.

Moreover

(d) for any two ordinals β and γ, we have γ ϵ β ⟺ γ ⊴ β ∧ γ ≠ β.

Proof Let (α, ϵ) be such a structure.

[a⇒b] (Cantor) We show by simultaneous induction on β, γ ∈ α that

(β ϵ γ) ∨ (β = γ) ∨ (γ ϵ β).

Let δ = β ∩ γ be the common part. We shall show that it is the whole of either β or γ by considering (using excluded middle) the four cases when β ⊴ γ and γ ⊴ β do and do not hold.

Suppose β ⋬ γ. Then (δ ⊴ β) ∧ (δ ≠ β), so by excluded middle there is some β′ ϵ β with ¬(β′ ϵ δ). By the induction hypothesis, we may use trichotomy for β′ and any γ′ ϵ δ ⊴ γ, but two cases give β′ ϵ δ by transitivity, leaving γ′ ϵ β′. Thus δ ⊴ β′ ϵ β, so δ ϵ β using plumpness of β, and δ = γ ϵ β.

Similarly γ ⋬ β gives β = δ ϵ γ. In the case where both inclusions fail, δ ϵ β ∩ γ = δ, which is not allowed, whereas if both hold we already have β = γ.

[a,b⇒d] We have γ ϵ β ⇒ (γ ⊴ β) ∧ (γ ≠ β) by transitivity. Conversely, there exists γ′ ϵ β \ γ by excluded middle. For δ ϵ γ, if γ′ ϵ δ or γ′ = δ then γ′ ϵ δ, so δ ϵ γ′ by trichotomy of β. Thus γ ⊴ γ′ ∈ β, so by plumpness γ ∈ β.

[b⇒c] If the relation has a loop, γ ≺ β ≺ γ, or δ ≺ γ ≺ β ≺ δ, etc., then ≺ is not well-founded. So if β and γ have the same children, γ ≺ β and β ≺ γ are forbidden, leaving γ = β. Similarly if δ ≺ γ ≺ β, excluding β ≺ δ and β = δ leaves δ ≺ β.

[c⇒a] We must show by induction on α that it is plump. Let γ ⊴ β ∈ α. Then by the induction hypothesis β satisfies all four parts of the Theorem, so either γ ϵ β or γ = β, whence γ ∈ α by transitivity. □

In the first part one might try to show ¬¬(β ϵ γ ∨ β = γ ∨ γ ϵ β) intuitionistically, but the induction step only gives ∀γ′. γ′ ϵ δ ⇒ ¬¬γ′ ϵ β′, which is not enough to deduce ¬¬δ ⊴ β′. So excluded middle is very thoroughly built in to this proof.

Even if you don’t like the notion of plumpness and choose only to consider the transitive notion of ordinal, the idea is unavoidable: the well founded relation (E, ≺) used in the proof of Proposition 4.3 is needed to define subtraction of transitive ordinals (Remark 7.7).

5 Plump and transitive ordinals We now have all the tools we need to present the usual theory of ordinals, but intuitionistically. Simply choosing those ensembles whose relation is (hereditarily) transitive provides a viable notion of ordinal, although the successor is poorly behaved. This section has been written as a parallel treatment of classical, plump and transitive ordinals. Ensembles also fit in to this picture. Transitivity allows us to switch from treating ordinals as elements of an ensemble to regarding each of them as a free-standing structure.

When comparing the different notions, we shall use the phrase plump ordinal for the “ordinals” defined in the previous section; beware that this does not refer to some sub-class of “general” ordinals which happen to be plump. Similarly transitive ordinal means transitive ensemble, where now we do mean an ensemble which is transitive.

Notation 5.1 Write On_{P} ⊂ On_{T} ⊂ Ens for the classes of plump and transitive ordinals, considered as class-ensembles with the ∈ relation. Also write On_{P} ⊂ On_{T} ⊂ Ens ⊂ Wfib for the categories (in fact preorders) whose morphisms are simulations, i.e. inclusions of initial segments. Finally WOrd_{P} ⊂ WOrd_{T} ⊂ Wfr are the categories composed of strictly monotone functions. All of these structures arise in common usage, for example Jean-Yves Girard’s dilators [8] are functors WOrd → WOrd which preserve pullbacks and filtered colimits.

Proposition 5.2 The set-theoretic union (Corollary 2.12) of a family of transitive or plump ordinals, and the intersection of two of them, is an ordinal of the same kind. Moreover binary intersection distributes over arbitrary unions.

Proof Let (α_{i} : i ∈ I), β and γ be plump ordinals with γ ⊴ β ∈ ⋃ α_{i}. Then β ∈ α_{i} for some i ∈ I, so γ ∈ α_{i} ⊴ ⋃_{i} α_{i}. The other parts are similar. □

Definition 5.3 The thin successor of a transitive ensemble α is α ∪ {α}. That is, we add an extra element ⋆ to the carrier of α, and extend its well founded relation by β ϵ ⋆ for all β ∈ α; then we use “α” as a name for ⋆. But as Robin Grayson [10, page 407] observed, this only satisfies

\begin{aligned}β^{+} ϵ α^{+} & ⇒ & β^{+} ⊴ α & ⇔ & β ϵ α \\ β^{+} ⊴ α^{+} & ⇔ & β ϵ α^{+} & ⇒ & β ⊴ α. \end{aligned}

These properties are formal consequences of the principles

α ∈ α^{+} α ⊴ α^{+} β ∈ α ⇒ β^{+} ⊴ α β^{+} ⊴ α^{+} ⇒ β ⊴ α

which are essential for the development of the theory (the last is deducible by Remark 5.6).

Remark 5.4 The first and third conditions are necessary and sufficient for ordinal to be the union of the successors of its elements:

β = ⋃ {γ^{+} : γ ∈ β}

cf . x ∈ {x} and x = ⋃ {{y} : y ∈ x} for sets. □

Proposition 5.5 For any plump ordinal α, the plump successor,

α^{+} =^{def} {β : β ⊴ α ∧ β ∈ On_{P} }

is again a plump ordinal. Moreover the implications above are all reversible, i.e. the plump successor operation preserves (and reflects) both the ϵ and ⊴ relations.

Proof By construction, α^{+} is a set of subsets of α, so it carries the reflexive ⊴ relation. However it is Proposition 3.6 which provides the (irreflexive) well founded ϵ relation. Then α^{+} is an initial segment of P(α) since γ ∈ β ⊴ α ⇒ γ ∈ α, so γ ⊴ α by transitivity, and γ is plump because α is hereditarily plump.

For plumpness of α^{+}, let γ be an ordinal with γ ⊴ β ∈ α^{+}. Then γ ⊴ β ⊴ α so γ ⊴ α and γ ∈ α^{+}. Its elements are ordinals by construction.

Finally, to show β ∈ α ⇒ β^{+} ⊴ α, let γ ∈ β^{+}, i.e. γ is an ordinal with γ ⊴ β ∈ α, so by plumpness γ ∈ α. The remaining implications are trivial. □

In [31], the plump successor is shown to be related to the unit η of the covariant powerset monad, and the predecessor and union to its “multiplication” μ.

Classically all initial segments are either proper or entire, and any proper one is represented by the least element of its complement, so the plump successor reduces to the thin one.

Remark 5.6 We can try to define the predecessor α^{−} by

α^{−} =^{def} ⋃ α = {γ : ∃β. γ ϵ β ∈ α} ⊴ α.

Then α^{+−} = α, so α^{+} ⊴ β^{+} ⇒ α ⊴ β, but more interestingly (in the plump case),

(a) if α^{−} is (representable as) an element of α then we have α^{−} ∈ α^{−+} ⊴ α, but β ∈ α ⇒ β ⊴ α^{−} ⇒ β ∈ α^{−+} (the last by plumpness), so α is a successor, namely of α^{−}. In this case α is closed under unions, with ∅ and α^{−} is its ⊴-least and greatest elements. The thin successor of ϕ ∈ Ω fails this: ∅ ∈ ϕ^{+} ⇔ ϕ ∨ ¬ϕ.

(b) if α^{−} = α then it is a limit since it can be expressed as a join of strictly smaller ones (β). Now α is closed under successor, because if γ ∈ α then γ ϵ β ∈ α for some β by construction of α^{−}, so γ^{+} ⊴ β ∈ α and γ^{+} ∈ α by plumpness.

Classically one or other of these holds, and it is also usual to consider zero separately from the other (infinite) limit ordinals, i.e. we require ∅ ∈ λ.

Remark 5.7 Since an ordinal α is a special case of a well founded relation, for any system of operations R_{β} : P(A) → A for β ∈ α, the equation

f(β) = R_{β}({f(γ) : γ ∈ β})

has a unique solution (Proposition 1.4). However what distinguishes the idiom of transfinite recursion over the ordinals is the analysis into the three cases of zero, successor and limit analogous to primitive recursion over ℕ.

Suppose that the carrier A is equipped with an element z ∈ A, and functions s_{β} : A → A for each β ∈ α and r_{λ} : P(A) → A for each limit ordinal λ ∈ α. Then classically there is a unique function f : α → A such that

f(0) = z
f(β^{+}) = s_{β}(f(β))
f(λ) = r_{λ}({f(β) : β ϵ λ})  if λ is a limit.

To derive this from the general recursion theorem of course we put R_{0}(∅) = z and R_{λ} = r_{λ}. However we want R_{β^{+}}(a_{γ} : γ ∈ β^{+}) = s_{β}(a_{β}), so for this form of the result without further hypothesis the more algebraic version of the general recursion theorem must be used, where a_{β} can be identified as the βth argument.

Remark 5.8 Alternatively f(β) must dominate {f(γ) : γ ∈ β^{+}}, i.e. stand out by its value alone, such as by being the greatest element. In

γ ∈ β^{+} ⇒ γ ⊂ β ⇒ f(γ) ≤ f(β)

the first implication holds when we read (−)^{+} as the singleton, thin successor or plump successor, and we aim to find conditions ensuring the second (monotonicity of f). Notice that, for the singleton, f(β) dominates {f(γ) : γ ∈ β^{+}} by being its only member.

The analysis into three cases is not valid as such intuitionistically, but we may recover the style by reading it as a system of equations to be solved: successors and limits are extreme cases or “boundary conditions.” In practice, infinitary operations are defined by universal properties: union (or join, ⋁, which is the case we treat), intersection (meet), limit and colimit. The seed z is similarly the least element (⊥), greatest element, terminal object or initial object of A, but assuming z = ⊥ is no real loss of generality, as we may consider the co-slice z ↓ A ≡ {a : z ≤ a} in place of A. The generalisation from joins to colimits also depends on the axiom of replacement, cf . Proposition 3.18 and Theorem 7.10.

We give the transfinite recursion theorem in parallel for sets, transitive ordinals and plump ordinals.

Theorem 5.9 Let A a complete lattice equipped with a system of operations s_{α} : A → A for α ∈ X, where X is either

(a) an ensemble; or

(b) a transitive ensemble, and assume a ≤ s_{α}(a) for all a ∈ A and α ∈ X; or

(c) a plump ordinal, and assume β ⊴ α ∧ b ≤ a ⇒ s_{β}(b) ≤ s_{α}(a).

Then there is a unique function f : X → A such that

f(0) = ⊥ f(α^{+}) = s_{α}(f(α))

for all α with α^{+} ∈ X and

f( ⋃_{i} α_{i}) = ⋁_{i} f(α_{i})

for all families (α_{i} ∈ X : i ∈ I) such that ⋃_{i} α_{i} ∈ X. In particular f is monotone in the sense that

γ ⊂ β ⇒ f(γ) ≤ f(β)

and for any limit ordinal λ ∈ X we still have

f(λ) = ⋁ {f(α) : α ϵ λ}).

Proof Define f : X → A by the general recursion theorem (Proposition 1.4) such that

f(α) = ⋁ {s_{β}(f(β)) : β ϵ α}.

Certainly this equation has a unique solution, and

f( ⋃_{i} α_{i}) = ⋁ {s_{β}(f(β)) : β ϵ ⋃_{i} α_{i}} = ⋁_{i} ⋁_{βϵα_{i}} {s_{β}(f(β))} = ⋁_{i} f(α_{i}).

Hence f is monotone and f(0) = ⋁ ∅ = ⊥ (assuming that 0 ∈ X). We have to check that the successor equation is satisfied, where by “successor” we mean either

(a) the singleton of a set, where f({α}) = ⋁ {s_{α}(f(α))};

(b) the thin successor of a transitive ordinal, where

f(α^{+}) = ⋁ {s_{β}(f(β)) : β ∈ α ∨ β = α} = f(α) ∨ s_{α}(f(α)) = s_{α}(f(α))

since a ≤ s_{α}(a);

(c) or the plump successor of a plump ordinal, where

f(α^{+}) = ⋁ {s_{β}(f(β)) : β ⊴ α} = s_{α}(f(α))

since, by monotonicity of f and s_{(−)}(−), this is the greatest term in the join.

Uniqueness of the solution of the stated equations follows from Remark 5.4, and the property for limit ordinals holds because they are closed under successor. □

Remark 5.10 For X ⊴ Y, the restriction of f_{Y} : Y → A to X is f_{X}, so we may form the union of these functions for all α ∈ On. Hence there are join-preserving functions f : Ens → A, f : On_{T} → A and f : On_{P} → A under the appropriate hypotheses on s_{α}. □

Remark 5.11 We want to be able to apply this method to the iteration of functors, for example in order to construct free algebras and solutions of equations between types such as X ≅ X^{X} in domain theory. However the domination condition above is implicitly idempotent, whereas coproducts are not in categories other than preorders (in particular they are disjoint in the category of sets and functions). So the construction must be understood as a colimit diagram with arrows f(γ) → f(β) whenever γ ⊴ β. The operations s_{α} : A → A must now be functors, and the monotonicity condition becomes a natural transformation s_{(−)} → s_{(−)}. Equivalently, s_{(−)}(−) : On_{P} × A → A is a functor of two variables. Now domination means being the terminal node of the diagram.

Classically, the union is directed (or the colimit filtered) by trichotomy. To recover directedness in the intuitionistic version we have to alter the definition of ordinal.

6 Directedness In categories of finitary structures, the construction of finite colimits is very complicated and might interfere with the process we wish to iterate. Filtered colimits are often better behaved, and classically only these are needed at the limit stages of transfinite operations. However ordinals cannot be trichotomous in the intuitionistic setting, and those which we have defined are not directed.

We shall not simply define a directed version of the plump ordinals, but also reconsider all of the other notions of induction we have. In this section we show how hereditary join replaces settheoretic binary union in the development of ensembles, transitive and plump ordinals. Section 8 is more radical and starts from well-foundedness. Directedness will be indicated by Ens^{↑}, On^{↑}, etc. As we said following Lemma 4.3, the definition of plumpness has changed because it depends on that of an ordinal, which has also changed.

The principle that every ordinal is a set of ordinals is essential to induction, so we have to define directedness hereditarily. Since ∅ must be an ordinal but is not directed in the standard sense, we omit the nullary cases from the

Definition 6.1 A carrier with a (reflexive) order relation ≤ is said to be directed if ∀xy. ∃z. x ≤ z ≥ y. It is a semilattice if there is a least such z (the join), and unital if there is also a least element ⊥.

Remark 6.2 An ensemble (X, ϵ) is hereditarily directed if each X ↓ z is directed, i.e.

∀xyz. x ϵ z ∧ y ϵ z ⇒ ∃u. x ⊂ u ∧ y ⊂ u ∧ u ϵ z.

Notice that the directedness property itself uses the reflexive relation ⊂ (since we cannot expect successor ordinals to be directed with respect to ϵ), whilst heredity is, as usual, defined in terms of the irreflexive one (ϵ). But then, putting x′, y′ and u for x, y and z (so x′, y′ ϵ u), we must have

∀x′ ϵ x, y′ ϵ y. ∃u′. x′ ⊂ u′ ∧ y′ ⊂ u′ ∧ u′ ϵ u.

Using set-theoretic notation, we define (recursively) the hereditary join:

x ⋓ y =^{def} ∥x∥ ∪ ∥y∥ ∪ {x′ ⋓ y′ : x′ ϵ x ∧ y′ ϵ y} ⊂ X

and then the bound must satisfy x ⋓ y ⊂ ∥u∥. In the plump case it follows automatically that x ⋓ y is representable in X and x ⋓ y ϵ z. Without plumpness, we only have to adjoin to X the successor of x ⋓ y and put z = x ⋓ y to force u = x ⋓ y. We are therefore only interested in x ⋓ y for u, so the directed notion of ordinal is characterised by closure under hereditary join, i.e. that x ⋓ y be representable in X for all x, y ∈ X. Propositions 6.7c and 8.8b support this. The proofs below involve a three-way case analysis, but we shall usually only mention the cross-terms x′ ⋓ y′.

The set-theoretic formula may be used to construct the hereditary join of two ensembles, using the axiom of replacement, but we show how to do without this in Section 8.

Example 6.3 ∅ and ϕ ≡ {∅ : ϕ} ∈ Ω are hereditarily directed. For ϕ, ψ ∈ Ω, the hereditary join ϕ ⋓ ψ is simply the disjunction (ϕ ∨ ψ), so U ⊂ Ω is hereditarily directed iff it is a subsemilattice. At the next level, U ⋓ V is the join of U and V in the lattice of subsemilattices of Ω. The directed transitive numerals agree with the transitive ones, and plump directed 2 is Ω, but the plump directed 3 consists of the down-closed subsemilattices of Ω. □

Definition 6.4 A hereditary semilattice is an ensemble (X, ϵ) such that every “set” z ∈ X is closed under the hereditary join operation, i.e. ∀xyz. x ϵ z ∧ y ϵ z ⇒ x ⋓ y ϵ z.

Proposition 6.5 The intersection in Ens of two hereditary semilattices, and the union of a directed family (^{⋃↑}, Remark 2.13b) of them are again hereditary semilattices. Binary intersection distributes over directed union. □

Hereditary join replaces binary union, so finite distributivity is no longer trivial; in fact it is surprising that it still holds.

Lemma 6.6 Let X be an ensemble and x ∈ X such that X ↓ x is a plump hereditary semilattice. Then x ∩ (y ⋓ z) = (x ∩ y) ⋓ (x ∩ z).

Proof Consider u = y′ ⋓ z′ with y′ ϵ y and z′ ϵ z. For [⊂], y′ ⊴ u ϵ x ⇒ y′ ϵ x by plumpness, and for [⊃], y′, z′ ϵ x ⇒ y′ ⋓ z′ ϵ x by directedness. □

Now we shall show how a hereditary semilattice is a partial algebra for ∅, ^{⋃↑} and various notions of successor, as well as for ⋓.

Proposition 6.7 Let x, y ∈ X in an ensemble such that X ↓x and X ↓y are hereditary semilattices, and x ⋓ y ∈ X. Then hereditary join

(a) preserves transitivity, i.e. if X ↓ x and X ↓ y are transitive then so is X ↓ (x ⋓ y);

(b) preserves hereditary directedness, i.e. X ↓ (x ⋓ y) is a hereditary semilattice;

(c) is the join with respect to ⊂ amongst hereditary semilattices, i.e. if X ↓z is also a hereditary semilattice with x ⊂ z and y ⊂ z then x ⋓ y ⊂ z;

(d) preserves plumpness, i.e. if x and y are plump (and hereditarily plump) then so is x ⋓ y.

Proof First note that X ↓ (x ⋓ y) consists of things like x_{n}, y_{n} and x_{n} ⋓ y_{n}, where x_{n} ϵ x_{n−1} ϵ ⋯ ϵ x_{1} ϵ x and y_{n} ϵ y_{n−1} ϵ ⋯ ϵ y_{1} ϵ y — notice that in order to form x_{n} ⋓ y_{n} we must take things from the same generation.

(a) If u ϵ w, and w is of this form then so is u.

(b) Similarly if u, v ϵ w are of this form then u ⋓ v ϵ w.

(c) This part re-states that X ↓ z is a hereditary semilattice.

(d) If u ⊴ w = x′ ⋓ y′ then u ∩ x′ ⊴ x′ ϵ x, so u ∩ x′ ϵ x by plumpness and similarly u ∩ y′ ϵ y, so u = (u ∩ x′) ⋓ (u ∩ y′) ϵ x ⋓ y by Lemma 6.6. □

In each case we have to define the successor operation and show that each ordinal is the directed union of the successors of its elements.

Proposition 6.8 Let x ∈ X in an ensemble such that X ↓ x is a hereditary semilattice. Suppose that the successor sx exists in X, where

(a) sx = {x} (singleton);

(b) sx = x ∪ {x} (thin successor) and X ↓ x is transitive; or

(c) sx = {y : y ⊴ x ∧ y ∈ On_{P}^{↑} } (plump successor) and x is a plump ordinal.

Then X ↓ (sx) is also a hereditary semilattice, and transitive or plump as appropriate. Moreover every ordinal of each kind satisfies

x ϵ sx  x ϵ y ⇔ sx ⊂ y  s(x ⋓ y) ⊂ sx ⋓ sy
x ⊂ x ⋓ y  y ⊂ x ⋓ y  x ⊂ z ∧ y ⊂ z ⇒ x ⋓ y ⊂ z  x ⊂ y ⊂ z ⇒ x ⊂ z.

Proof

(a) A singleton is trivially directed.

(b) For y ϵ x, check that x ⋓ y = x.

(c) If y, z ϵ sx then y, z ⊴ x, so y ⋓ z ⊴ x and y ⋓ z is a plump ordinal by Proposition 6.7(c,d).

Lastly, s(x ⋓ y) ⊂ sx ⋓ sy is formally equivalent (in the context of the other properties) to the definition of a hereditary semilattice, x, y ϵ z ⇒ x ⋓ y ϵ z. □

Directed ordinals were introduced in order only to consider directed joins in the target structure, so let us assess to what extent this objective has been achieved.

Theorem 6.9 For hereditary semilattices and their transitive and plump forms,

(a) the unions in Remarks 5.4 and 5.6 are directed: every directed ordinal is the directed union of the successors of its elements;

(b) in the Transfinite Recursion Theorem 5.9, the target structure A must still be a complete lattice but f : X → A preserves only directed joins and the least element;

(c) if s_{α⋓β}(a ∨ b) ≤ s_{α}(a) ∨ s_{β}(b) then f preserves binary (and hence all) joins;

(d) if s_{(−)}(−) is monotone then the union in the construction is directed, so A need only have ⊥ and directed joins.

Proof Consider

f(α ⋓ β) = ⋁_{γϵα} s_{γ}(f(γ)) ∨ ⋁_{δϵβ} s_{δ}(f(δ)) ∨ ⋁_{γϵα} ⋁_{δϵβ} s_{γ⋓δ}(f(γ ⋓ δ)).

For f to preserve binary joins we must be able to drop the cross-terms, for which we want

s_{γ⋓δ}(f(γ ⋓ δ)) ≤ s_{γ}(f(γ)) ∨ s_{δ}(f(δ)),

and this follows (by induction) from the given condition. If s_{(−)}(−) is also monotone then equality holds here, and this is sufficient to make

f(α) = ^{⋁↑}{s_{β}(f(β)) : β ∈ α}

a directed join. □

Remark 6.10 Hereditary directedness makes the ϵ relation a semilattice homomorphism (ϵ) : X × X^{op} → Ω, cf . Remarks 1.5 and 4.6.

7 Universal properties As often happens when we investigate classical structures intuitionistically, the definitions bifurcate. Those marked ∘ are discussed in [15], but ⊛ is also useful. The line joining the plump and directed plump ordinals is broken as a reminder that the definition of plumpness changes.

∘
[figure]
plump ∘  ⊛
[figure]
∘  •  • hereditary semilattice
[figure]
transitive •  extensional ∘  • well founded semilattice
[figure]

well founded •

Theorems 5.9 and 6.9 showed how ensembles with the transitivity, plumpness and directedness conditions may be regarded as partial algebras for least element, directed union, various notions of successor and either binary union or hereditary join. These are free in the sense that there is a unique structure-preserving function to any complete lattice equipped with endofunctions s_{α} satisfying certain conditions.

By way of summary we shall now re-state the transfinite recursion theorem as a family of universal properties. For clarity we shall consider the total algebras and drop the parameter from s_{α}.

Remark 7.1 The Burali-Forti paradox shows that each of these structures is a proper class. If it were admissible as a set it would be one of its own elements and hence isomorphic to a proper substructure, which is forbidden by Corollary 2.6.

Theorem 7.2 Each of the six structures Ens, On_{T}, On_{P}, Ens^{↑}, On_{T}^{↑} and On_{P}^{↑} has an endofunction s, defined in the second column, satisfying the condition in the third or fourth column for the undirected and directed versions respectively. The undirected structures are closed under arbitrary union; the directed ones under ∅, hereditary join and directed union.

Ens  {x}  (no equation)  s(x ⋓ y) ⊂ sx ⋓ sy
On_{T}  x ∪ {x}  x ⊴ sx  x ⊴ sx and s(x ⋓ y) ⊴ sx ⋓ sy
On_{P} {y ∈ On_{P} : y ⊴ x} x ⊴ y ⇒ sx ⊴ sy  s(x ⋓ y) = sx ⋓ sy

They are free in the sense that if A is a complete lattice with an endofunction s : A → A satisfying the same condition then there is a unique function f from the structure to A which preserves s and arbitrary joins.

On_{P}^{↑} is also the free algebra for a least element ⊥, monotone function s and directed unions. □

Remark 7.3 The rule x ϵ y ⇔ sx ⊂ y eliminates ϵ in favour of ⊂ and can be reduced further to y = sx ∪ y or y = sx ⋓ y. It is equivalent to

y = ⋃ {sx : x ϵ y}

(Remark 5.4) and was needed for uniqueness in the proof of Theorem 5.9. Each kind of ordinal has its own notion of successor: we cannot choose, say, transitive ensembles with the fat successor.

Remark 7.4 The algebras are proper classes because of the unbounded joins. Consider instead an algebra with a successor s and all joins of subsets indexed by objects I belonging to a certain class M. Suppose now that M is enlarged to contain all of the arities for which all joins exist. Then this class (is closed under isomorphism and) obeys the following closure conditions:

(a) all finite sets (including ∅) are in M;

(b) if I ∈ M and there is a surjective function I ↠ J then J ∈ M;

(c) and if I ∈ M and for each i ∈ I also J_{i} ∈ M then ⋃_{i∈I} J_{i} ∈ M.

These closure conditions, or rather their analogues in categorical form, arise in formal sheaf theory and characterise classes of open maps. André Joyal and Ieke Moerdijk [15], in complementary work, have described the total algebras analogous to Ens, On_{T}, On_{P} and On_{P}^{↑} but with joins of arities belonging to such a class. When M has an admissible set of isomorphism classes, the free algebra is also admissible.

Traditionally the first application of transfinite recursion is ordinal arithmetic.

Definition 7.5 We can define, as usual,

\begin{aligned}α + 0 & = & α & α + (β^{+}) & = & (α + β)^{+} \\ α0 & = & 0 & α(β^{+}) & = & (αβ) + α \\ α^{0} & = & 1 & α^{(β^{+})} & = & (α^{β})α \end{aligned}

such that each preserves inhabited (directed and binary) joins in the second argument. By defining α + (−) : On → α ↓ On ≡ {β ∈ On : α ⊴ β} and α^{(−)} : On → 1 ↓ On, these operations can be considered to preserve all joins.

Lemma 7.6 By induction on γ, one may prove successively that

α + (β + γ) = (α + β) + γ
α(β + γ) = (αβ) + (αγ)
α(βγ) = (αβ)γ
α^{β}α^{γ} = α^{β+γ}
(α^{β})^{γ} = α^{βγ}

but ω = 1 + ω ≠ ω + 1 = ω^{+}, ω = 2ω ≠ ω2 = ω + ω, ω = (2 + 3)ω ≠ 2ω + 3ω = ω2 and ω^{3}2 = (ω2)^{3} ≠ ω^{3}8. □

Remark 7.7 It is also possible to define subtraction, division and logarithm (essentially as the right adjoints of addition, multiplication and exponentiation), but these do not inherit the properties of their classical analogues.

For example, it may be shown that α + γ ∈ α + β ⇒ γ ∈ β (the proof is straightforward for plump ordinals, but for transitive ordinals it is done by induction over the relation ≺ which was used in Proposition 4.3), whence α + (−) is injective. This suggests {γ : β ⊴ γ ∈ α} as the carrier of α−β, but the restriction of ϵ to this non-lower subset of α need not be extensional. (Classically, any subset of an ordinal α is an ordinal with respect to the restriction of the relation.)

Example 7.8 1 − ϕ = ¬ϕ and ϕ + (1 − ϕ) = ϕ ∨ ¬ϕ. □

This does not entirely rule out any possibility of a Cantor Normal Form for arbitrary ordinals, but it would appear to be a loser.

Remark 7.9 For most practical purposes, the ordinals which can be expressed in terms of ω and the arithmetical operations suffice. In this algebra (called ε_{0}), the five equations above may be treated as reduction rules, and such expressions do have a (Cantor) normal form. Moreover, by comparing successive exponents of ω and their coefficients, the trichotomy law holds, just as it does in ℕ.

Transfinite recursion also gives the “ordinal reflection” of an arbitrary well founded relation. We begin with the traditional formula, which uses the Axiom of Replacement. This seems to be the only way of finding the plump rank; for the weaker notions of ordinal there is a construction within simple type theory (an elementary topos or Zermelo set theory, without replacement), but its universal property is not so good.

Theorem 7.10 Let (X, ≺) be a carrier with a well founded relation. Then its plump ordinal rank

rank(x) = ⋃ {rank(x′)^{+} : x′ ≺ x}

exists (given the axiom of replacement), and satisfies the universal property that for any strictly monotone function f : X → α to a plump ordinal, ∀x. rank(x) ⊴ f(x).

Proof The construction is similar to that in the general recursion theorem (Proposition 1.4), except that now an attempt assigns a set rather than a value. Replacement is needed to form the union of the attempts (Proposition 3.18).

The universal property is proved by induction on x. For x′ ≺ x we have

rank(x′) ⊴ f(x′) ∈ f(x)

so (rank(x′))^{+} ⊴ (f(x))^{+} ⊴ f(x),

so rank(x) = ⋃_{x′≺x} (rank(x′))^{+} ⊴ ⋃_{x′≺x} (f(x))^{+} ⊴ f(x).  □

The hereditarily directed plump rank has the same properties. Mostowski’s theorem (the extensional quotient, Theorem 2.11), also satisfies the rank formula (with singleton for successor), and so do the extensional quotient of the transitive closure and their directed versions. However they fail the universal property with respect to strictly monotone functions, which is unfortunate because this is all that complexity measures usually are (Remark 1.10).

Example 7.11 Let X = {0, 1} with 0 ≺ 1, so rank(0) = ∅ and rank(1) = {∅} according to any definition. Consider the strictly monotone functions f defined on X by

f(0) =  f(1) =  then ...
(a) ensemble  {∅}  {{∅}}  rank(1) ⋬ f(1)
(b) ensemble  {{∅}}  {{{∅}}}  rank(1) ∉ f(1)
(c) transitive ensemble  {∅ : ψ}  {∅ : ψ} ∪ {{∅ : ψ}}  rank(1) ⊴ f(1) ⇒ ψ ∨ ¬ψ □

Conjecture 7.12 Plump ω does not exist in the free topos with natural numbers, i.e. the term model of simple type theory or intuitionistic Zermelo set theory.

Remark 7.13 Definition 2.3 modified discrete fibrations (isotomies) so that Theorem 2.11 would make Ens a reflective subcategory. This had the valuable result of explaining the bizarre notion of union in set theory. The other five structures (On_{T}, On_{P}, Ens^{↑}, On_{T}^{↑} and On_{P}^{↑}) could also be made reflective in the categories of well founded relations with suitably modified notions of simulation, which for ordinals reduce to inclusions of initial segments.

These properties can also be expressed by saying that the forgetful functors On → Wfr are stable (have left adjoints on each slice), and by the

Proposition 7.14 WOrd (the category of ordinals, of any kind, and strictly monotone functions) admits a factorisation system in which On (the category, indeed preorder, composed of simulations) is the class of “monos”; the “epis” are cofinal maps. □

8 The hereditarily directed rank Theorem 2.11 showed that extensionality may be imposed on any well founded relation by “ordinary” mathematical techniques without the need for the axiom of replacement. The same is trivially so for transitivity. In this section we show how to do it for hereditary directedness.

Some recursive techniques, such as β-reduction and unification, reduce one complex structure to a proliferation of simpler ones. This means that we have to consider induction over (non-empty Kuratowski-) finite sets. For these applications the relation is ≺^{♭} defined below, but first we recall the simpler induction on the number of elements.

Definition 8.1 The unary Kuratowski induction scheme on a carrier X is

ϕ(∅) ∀x. ∀U. ϕ(U) ⇒ ϕ(U ∪ {x})

K

∀U. ϕ(U)

where U ∈ P_{f}(X). In fact this is the definition of P_{f}(X), the finite powerset: it is the smallest collection of subsets including the empty set and closed under adding elements. A subset U ∈ P_{f}(X) has a finite listing, possibly with repetition; [30] discusses how the familiar informal ways of handling finite sets relate to the formal introduction and elimination rules. See there or e.g. [13, §9.1] for a proof of:

Proposition 8.2 P_{f}(X) is the free unital semilattice on the carrier X. It is decidable whether U = ∅, and P_{f}^{+}(X) = P_{f}(X) \ {∅} is the free semilattice (cf . Definition 6.1). □

Definition 8.3 Given an irreflexive relation ≺ on a carrier X, the lower, flat, angelic or Hoare order ≺^{♭} on P_{f}(X) is

U ≺^{♭} V ⟺ (∃v ∈ V . ⊤) ∧ (∀u ∈ U. ∃v ∈ V . u ≺ v).

We intend to omit ∅ later, but to start with we want ∅ ≺^{♭} V for any inhabited V. The terminology is adapted from the theory of nondeterministic programs, in which (P_{f}(X), ≺^{♭}) is known as the lower (etc.) powerdomain of X; the musical notation was suggested by Carl Gunter (U ≤^{♯} V is ∀v ∈ V . ∃u ∈ U. u ≤ v and U ≤^{♮} V is U ≤^{♭} V ∧ U ≤^{♯} V; we used the latter, known as the Egli-Milner order, in Theorem 2.11).

Definition 8.4 A well founded semilattice is a carrier S with a well founded relation < and a commutative, associative, idempotent binary operation ⋓ such that

(a) if a < c and b < c then (a ⋓ b) < c,

(b) if a < b then a < (b ⋓ c).

(Beware that a < (a ⋓ b) need not hold, since a ≮ a = a ⋓ a.) It is called distributing (sic) if it satisfies the further condition that

(c) if a < (b_{1} ⋓ b_{2}) then either a < b_{1} or a < b_{2} or a = a_{1} ⋓ a_{2} for some a_{1} < b_{1} and a_{2} < b_{2}.

Lemma 8.5 Let (X, ≺) be any carrier with a binary relation. Then (P_{f}(X), ≺^{♭}, ∪) satisfies (a), (b) and (c). If ≺ is transitive then so is ≺^{♭}. □

Proposition 8.6 Let (X, ≺) be a carrier with a well founded relation. Then (P_{f}(X), ≺^{♭}) is also well founded.

Proof By Proposition 1.7d, without loss of generality we may suppose that the predicate ϕ(U) satisfies the strict ≺^{♭}-induction premise (this is used at line 25). Most of the proof is shown by the box method on the next page. □

Now we transfer Proposition 8.2 to strictly monotone functions and simulations. The empty set is omitted and S is not required to have a least element because, if we included them, part (a) would need ∀x. ⊥_{S} < f(x) and (b) would fail altogether.

Proposition 8.7 Let (X, ≺) be any carrier with a well founded relation. Then P^{♭}(X) =^{def} (P_{f}^{+}(X), ≺^{♭}, ∪) is a distributing, well founded semilattice. Moreover

(a) for any well founded semilattice (S, <, ⋓) and strictly monotone function f : X → S, there is a unique strictly monotone homomorphism f̄: P^{♭}(X) → S making the triangle commute;

(P_{f}^{+}(X), ≺^{♭}, ∪) .................^{f̄} (S, <, ⋓)
[figure: f]
(X, ≺)

1 ∀U. [∀V. V ≺^{♭} U ⇒ ϕ(V)] ⇔ ϕ(U)
2 ϕ(∅)  ∀E(1, def(≺^{♭}))
3 ψ(x) =^{def} ∀U.ϕ(U) ⇒ ϕ(U ∪ {x})
∀x  4 ∀y.y ≺ x ⇒ ψ(y)
∀V_{0}  5 ϕ(V_{0})
6 ϑ(W) =^{def} W ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W)
7 ϑ(∅)  def(6, 5)
∀W  8 ϑ(W)
∀y 9 W ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W) def(6)
10 W ∪ {y} ≺^{♭} {x} ≡ W ≺^{♭} {x} ∧ y ≺ x
11 ϕ(V_{0} ∪ W)  ⇒E(9, 10)
12 ψ(y) ≡ ∀V.ϕ(V) ⇒ ϕ(V ∪ {y})  ∀E(4, 10), def(3)
13 ϕ(V_{0} ∪ W ∪ {y})  ∀E(12, 11)
14 W ∪ {y} ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W ∪ {y})  ⇒I
15 ϑ(W ∪ {y})  def(6)
16 ϑ(∅) ∧ ∀y.∀W. [ϑ(W) ⇒ ϑ(W ∪ {y})]  ∧I(7, ∀I)
17 ∀W.ϑ(W)  K-induction for ϑ
18 ∀W. W ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W)  def(6)
19 ∀V_{0}. ϕ(V_{0}) ⇒ (∀W. W ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W))  ∀I
∀U 20 ϕ(U)
21 U = ∅ ∨ U ≠ ∅  Proposition 8.2
22 U = ∅ ⇒ ∀W. W ≺^{♭} (U ∪ {x}) ⇒ ϕ(W)  ∀E(19, V_{0} = ∅, 2)
∀V_{0} 23 V_{0} ≺^{♭} U
∀W 24 W ≺^{♭} {x}
25 ϕ(V_{0})  ∀⇐E(1, 20, 23)
26 ϕ(V_{0} ∪ W)  ∀E(19, 25, 24)
27 ∀V_{0}, W . V_{0} ≺^{♭} U ∧ W ≺^{♭} {x} ⇒ ϕ(V_{0} ∪ W)  ∀I
28 U ≠ ∅ ⇒ ∀V.V ≺^{♭} (U ∪ {x}) ⇒ ϕ(V)  Lemma 8.5
29 ∀V.V ≺^{♭} (U ∪ {x}) ⇒ ϕ(V)  ∨E(21, 22, 28)
30 ϕ(U ∪ {x})  ∀E(1, 29)
31 ∀U.ϕ(U) ⇒ ϕ(U ∪ {x}) ≡ ψ(x)  ∀I, def(3)
32 ∀x.[∀y. y ≺ x ⇒ ψ(y)] ⇒ ψ(x)  ∀I
33 ∀x.ψ(x)  ≺-induction for ψ
34 ϕ(∅) ∧ ∀x. ∀U. [ϕ(U) ⇒ ϕ(U ∪ {x})]  ∧I(2, def(3, 33))
35 ∀U. ϕ(U)  K-induction for ϕ

(b) if S is distributing and f is a simulation then so is f̄.

Proof

(a) Given U ≺^{♭} V, with a listing U = {u_{1}, …, u_{n}}, there is a sequence v⃗ ∈ V with u_{i} ≺ v_{i}. Then f̄(U) = f(u_{1}) ⋓ ⋯ ⋓ f(u_{n}) < f(v_{1}) ⋓ ⋯ ⋓ f(v_{n}), so f̄(U) < f̄(V).

(b) Given a < f̄(V), there is a listing V = {v_{1}, …, v_{n}}. The distributing property of S gives a subsequence, a = a_{1} ⋓ ⋯ ⋓ a_{k} with a_{i} < f(v_{i}). Since f is a simulation, a_{i} = f(u_{i}) with u_{i} ≺ v_{i} for some u⃗ ∈ X, so f̄(U) = a, where U = {u_{1}, … u_{k}} ≺^{♭} V. □

This result says that the forgetful functor from the category of well founded semilattices and strictly monotone homomorphisms to Wfr has a left adjoint. However it does not say the same of the forgetful functor from the category of distributing well founded semilattices and simulation homomorphisms to Wfib, because the “unit” X → P^{♭}(X) is not a simulation (a weaker but more complicated notion of simulation is required).

The lower powerdomain interacts well with extensionality.

Proposition 8.8 Let (X, ≺, ⋓) be a distributing well founded semilattice.

(a) Then the extensional quotient X/∼ is also a distributing well founded semilattice such that X ↠ X/∼ is a semilattice homomorphism.

Now suppose that ≺ is also extensional and re-name it ϵ. Then

(b) The binary operation is hereditary join (Remark 6.2), so X is a hereditary semilattice (Definition 6.4), and conversely every hereditary semilattice is an extensional distributing well founded semilattice.

(c) X is (uniquely isomorphic to) the extensional quotient of its lower powerdomain.

(d) Let Y be another hereditary semilattice and h : X ⊴ Y a simulation. Then h is a ⋓- homomorphism.

Proof

(a) We must show that ∼ from the proof of Theorem 2.11 is a semilattice congruence, i.e. by simultaneous induction that

a_{1} ∼ a_{2} ∧ b_{1} ∼ b_{2} ⇒ a_{1} ⋓ b_{1} ∼ a_{2} ⋓ b_{2}.

Let c_{1} ≺ a_{1} ⋓b_{1}. Then either c_{1} ≺ a_{1} or c_{1} ≺ b_{1} or c_{1} = d_{1} ⋓e_{1} for some d_{1} ≺ a_{1} and e_{1} ≺ b_{1}. In these cases there are, by definition of ∼, c_{1} ∼ c_{2} ≺ a_{2}, c_{1} ∼ c_{2} ≺ b_{2}, or d_{1} ∼ d_{2} ≺ a_{2}, e_{1} ∼ e_{2} ≺ b_{2}, with (by the induction hypothesis) c_{2} = d_{2} ⋓ e_{2} ∼ c_{1}. The required properties of X/∼ follow since X ↠ X/∼ is a simulation. For example, if [a] ϵ [b_{1}] ⋓ [b_{2}] = [b_{1} ⋓ b_{2}] then a′ ≺ b_{1} ⋓ b_{2} for some a ∼ a′ and the conclusions of the distributing property transfer from X to X/∼ because the map is a strictly monotone homomorphism.

(b) This translates the distributing property into set notation.

(c) Lift the simulation id : X → X to P^{♭}(X) and then its extensional quotient. The result is surjective because it completes the triangle, and injective by Corollary 2.9.

(d) The hereditary join is characterised set-theoretically, and so is preserved by simulations. Alternatively, use induction on X, the distribution property of both X and Y and the lifting property of h. □

Corollary 8.9 For any well founded relation (X, ≺), there is a hereditarily directed transitive ensemble α and a strictly monotone function X → α. □

Remark 8.10 To sum up the universal properties, (a) The transitive closure (Proposition 1.7e) lifts strictly monotone functions and simulations

whose targets are equipped with transitive well founded relations. It does not preserve extensionality or hereditary directedness. The inclusion is bijective and strictly monotone but is not a simulation.

(b) The lower powerdomain lifts strictly monotone functions targeted at well founded semilattices and simulations targeted at distributing ones (Proposition 8.7b). It preserves transitivity but not extensionality. The inclusion is strictly monotone but not a simulation.

(c) The extensional quotient lifts simulations targeted at ensembles (Theorem 2.11), but it does not lift strictly monotone functions. It preserves both transitivity and hereditary directedness. The quotient map is a surjective simulation.

So the constructions must be applied in the order (a), then (b), then (c). □

9 Tarski’s fixed point theorem The following is a typical application of transfinite recursion.

Lemma 9.1 Let (A, ≤) be a poset with least element ⊥ and joins of all directed subsets, and s : A → A a monotone endofunction. Then

(a) For any transitive hereditary semilattice X there is a unique function f : X → A preserving directed joins and such that f(0) = ⊥, f(α^{+}) = s(f(α)).

(b) Suppose a ∈ A is a fixed point, i.e. s(a) = a. Then ∀α. f(α) ≤ a.

(c) If f(β) is a fixed point and β ⊴ α then f(α) = f(β).

Proof (a) Theorem 6.9d. Monotonicity of s in the target structure is needed, but plumpness (monotonicity of successor for ordinals) is not. (b) Induction on α. (c) Monotonicity of f. □

Question 9.2 Does s : A → A necessarily have a fixed point?

Classically we shall see that it does; this is colloquially known as Tarski’s theorem.

By a very old idea, maybe we can find the fixed point by iteration, i.e. as some f(α). Intuitionistically, as well as classically, we can define ordinals and use them to iterate functions as often as we like, but when do we stop? Using the Burali-Forti idea,

Lemma 9.3 (Freidrich Hartogs [11]) For any carrier A, there is an ordinal α such that there is no injective function α ↪ A.

Proof Let I ⊂ P(A) × P(A × A) be the collection of all subsets U ⊂ A with ordinal structures (≺) ⊂ U ×U. The collection I carries the relation of membership between ordinals by Remark 3.3. If β is an ordinal with β ⊴ (U, ≺) ∈ I then (β, ϵ) ∈ I, so the extensional quotient of I is a plump ordinal, α. If there were some function α ↪ A then α ≅ U ⊂ A with (U, ≺) ∈ I and α would be isomorphic to one of its elements, which is forbidden by Corollary 2.6. □

Classically, this construction is the least such α.

Remark 9.4 The idea is to produce an ordinal which is “bigger” than A. We might say that A is smaller than B if there is either an injection A ↪ B or a surjection B ↠ A (classically, the axiom of choice makes the second redundant). The smallest transitive relation containing both of these possibilities is that A is a subquotient of B, i.e. A ↞ C ↪ B, and arises from a partial equivalence relation (symmetric and transitive but not necessarily reflexive) on B. The above construction can be adapted accordingly. Using the hereditarily directed rank (previous section) or, more crudely, by considering ordinal structures on subquotients of A × ℕ, the big ordinal can be taken to be hereditarily directed. I suggest that ℌ(A), and hence ω_{1} = ℌ(ℕ), be defined intuitionistically to be as large as is demanded by all of these generalisations. (For a cardinal κ, ℌ(κ) is the successor cardinal.)

Remark 9.5 The fixed point theorem holds in the following circumstances:

(a) The poset (A, ≤) is a complete lattice. Alfred Tarski [27] showed that there is a complete lattice of fixed points.

(b) The function s is Scott-continuous, i.e. preserves countable directed joins. Then f(ω) is already the fixed point.

(c) A function s is said to have rank κ if it preserves joins of diagrams I which are κ-directed (i.e. if F ⊂ I has cardinality < κ then it already has a bound in I) then f(κ) is the fixed point.

(d) The Hartogs construction provides an iteration which cannot be injective, so classically it must repeat itself. For if f(α) = f(β) with α ⋬ β then β ∈ α so β^{+} ⊴ α and f(β) = f(β^{+}) = f(α), i.e. there is a fixed point after β iterations.

(e) If the world E is a sheaf topos over (indeed any locally small category with an admissible set of generators with respect to) a Boolean topos then the classical result may be applied to the hom-sets of E and the intuitionistic one deduced via its external logic.

(f) The axiom of collection asserts that the image of a function f : On → A from a class to an admissible set is admissible and that there is an admissible set U ⊂ On with the same image. Joyal and Moerdijk [15] observe that this also gives the fixed point. However collection destroys the existence property, which is the outstanding feature of intuitionistic logic, and alters the class of provably total functions [7]. Personally, I can see no justification of this axiom by examples in parts of mathematics other than set theory, and I also feel that constructive mathematicians ought to emphasise the fact that infinitary equational theories behave very differently from finitary ones in the absence of the axiom of choice.

Question 9.6 Can one develop an intuitionistic notion of the rank of a functor based on [15]?

Conjecture 9.7 The result also holds under any of these assumptions:

(a) A is ¬¬-separated i.e. ¬¬(a = b) ⇒ a = b. This is so for the domains in some models of synthetic domain theory [29].

(b) A is a continuous poset.

(c) The axiom of foundation holds in the sense of Definition 3.16.

(d) A is a preframe, i.e. it has finite meets and the operation (∧) : A×A → A preserves directed joins, and s : A → A preserves binary meets. For any plump hereditary semilattice X one can then show that f : X → A preserves binary meets as well as successor and arbitrary joins. The advantage over the situation in [15] is that preframe presentations present [14].

Although the Hartogs method is constructive, its application is not. By considering a case where we know where the fixed point is, we see that ℌ(A) is in general much too small.

Proposition 9.8 For plump ordinals,

(a) (α^{+}, ⊴) is a complete lattice and β ↦ (β^{+} ∩ α) is a monotone endofunction whose only fixed point is the top element, α ∈ α^{+}.

(b) Curiously, this is equivalent to β ∩ α ∈ α ⇒ β ∈ α. □

Example 9.9 Let ϕ be any proposition with ⊢ ¬¬ϕ. Then (x = y) ∨ ϕ is an equivalence relation x ∼ y on any object A_{0} with the property that on A = A_{0}/∼, ∀xy. ¬¬(x = y). Since any well founded relation on A must be empty, ℌ(A) = Ω = 0^{++}. Now consider the complete lattice A_{0} = α^{+} ordered by ⊴, for 2 < α. The quotient A carries an order relation and an endofunction induced by those on A_{0}. The least fixed point occurs after α iterations, but the Hartogs construction only offers s(s(⊥)). More precisely, put α = 3; the construction names a point β = 2 which is supposedly fixed, i.e. sβ = β in A; but this means (sβ = β) ∨ ϕ in A_{0} = 4, so (since 3 ≠ 2) ϕ holds. □

Conclusion and Acknowledgements Faced with such a variety of notions of ordinal, how should one choose between them?

If the target structure A is a complete lattice or complete category then other methods of induction are available, using closure conditions or adjunctions. Ordinals are therefore only useful when A just has directed joins, for which the endofunction s : A → A must be monotone and the ordinals must be directed.

The need for plumpness is not so clear. Hereditarily directed plump ordinals certainly approximate the algebraic properties of the classical ordinals most closely. However they don’t look much like the finite numerals, and replacement is needed to construct the rank. Besides, Theorem 6.9d showed that monotonicity in the target structure suffices: it is not needed for the ordinals themselves.

In a sense it doesn’t matter that they don’t look like the finite numerals, because we only use ordinals as labels for recursion: by means of the plump rank we may use transitive ensembles to name their more powerful but unwieldy counterparts. We know this even in the traditional situation: Zermelo’s sequence ∅, {∅}, {{∅}}, {{{∅}}}, ..., which are the numerals from Ens, serve just as well as von Neumann’s more cumbersome 0 = ∅, 1 = {∅}, 2 = {∅, {∅}}, 3 = {∅, {∅}, {∅, {∅}}}, for Peano induction.

The definition {β : β ⊴ α} for the (fat) successor was suggested by my work in synthetic domain theory [29]: I wanted to justify my informal use of the term finite ordinal there. Neither fat nor thin was right, and plumpness is the appropriate compromise.

Anachronistically, we divided Cantor’s definition into well-foundedness and trichotomy, and have examined several refinements of the second clause. The Hartogs construction is sufficiently polymorphic that it seems unlikely that this strategy will ever conquer Tarski’s theorem.

Apart from being replaced by the induction scheme, the idea of well-foundedness has gone unchallenged. This is where the problem with Hartogs’ lemma lies, because the definition forces the relation ≺ to be irreflexive. The induction scheme must be restricted to some class of predicates which does not include equality. I have in mind a generalisation [31] which would include Scottinduction on ^{⋁↑}-closed subsets, as used in denotational semantics.

This has drastic consequences for the development of the theory, beginning with the general recursion theorem. Corollary 2.6, and so the Russell, Burali-Forti and Hartogs arguments, will fail, cf . the possibility of having a type of types in domain theory [12, 28] versus [24]. These generalisations lie within the realm of synthetic domain theory [29].

Partial correctness — the correspondence between the connectives of logic and category theory — is now very well understood. On the other hand, there are numerous techniques of induction (and co-induction [1, 23]), whose relationship to adjunctions remains ad hoc. One of the challenges to categorical logic in future must therefore be to reconcile these: to find, in a systematic way, inductive proof principles corresponding to any given adjunction. Tarski’s fixed point theorem is the first test of that challenge.

I hold an Advanced Research Fellowship (1992–7) and Starter Grant funded by the British Engineering and Physical Sciences Research Council. Previously I was funded by the EPSRC project Foundational Structures in Computer Science and the European Union ESPRIT Basic Research Action Categorical Logic in Computer Science. My visit to Darmstadt in August 1992 was paid for by the Deutsche Akademische Austauschdienst and the British Council and my visit to Warsaw was supported by the Komitet Badan Naukowych.

A preliminary announcement of this work was made in the types electronic forum on 2 December 1991. It was presented at a CLiCS workshop at the University of Århus in March 1992, at the international category theory meeting at the Isle of Thorns (University of Sussex) in July 1992 and at Category Theory and Computer Science V at CWI in Amsterdam in September 1993. I also gave a seminar in Warsaw in November 1994, with a member of the Mostowski family in the audience.

I would like to thank Peter Aczel, Peter Freyd, Wilfrid Hodges, Martin Hyland, Mamuka Jibladze, Peter Johnstone, André Joyal, Achim Jung, Jim Lipton, Bob Lubarsky, Ian Mackie, Adrian Mathias, Ieke Moerdijk, Andy Pitts, Dana Scott and Marek Zawadowski for their comments at various stages in the gestation of this work, and also the anonymous referee who detected an error deeply nested in the proof of Proposition 8.6.

References

[1] Peter Aczel. Non-well-founded sets. CSLI Lecture Notes 14. Center for the Study of Language and Information, 1988.

[2] John Bell. Toposes and local set theories: an introduction. Oxford: Clarendon, 1988.

[3] Cesare Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo matematico di Palermo, 11:154–164, 1897. English translation: A question on tranfinite numbers and on wellordered classes in [32], pages 104–111.

[4] Georg Cantor. Über unendliche, lineare Punktmannigfaltigkeiten. Mathematische Annalen, 21:545– 591, 1883.

[5] John Conway. On Numbers and Games. Academic Press, 1976.

[6] Abraham Fraenkel. Über die Grundlagen der Cantor-Zermeloschen Mengenlehre. Mathematische Annalen, 86:230–7, 1922.

[7] Harvey Friedman and Andre Scedrov. The lack of definable witnesses and provably total functions in intuitionistic set theories. Advances in Mathematics, 57:1–13, 1985.

[8] Jean-Yves Girard. Π_{2}^{1} logic: Part I, dilators. Annals of Mathematical Logic, 21:75–219, 1981.

[9] Kurt Gödel. The consistency of the axiom of choice and the continuum hypothesis. Proceedings of the National Academy of Sciences, 24:556–7, 1938. Re-printed in Annals of Mathematics Studies, vol. 3, Princeton University Press, Princeton, NJ, 1940.

[10] Robin Grayson. Heyting valued models for intuitionistic set theory. In Michael P. Fourman, Chris J. Mulvey, and Dana S. Scott, editors, Applications of Sheaves, Lecture Notes in Mathematics 753. Springer-Verlag, 1977, pages 402–414.

[11] Friedrich Hartogs. Über das Problem der Wohlordnung. Mathematische Annalen, 76:436–443, 1915.

[12] Martin Hyland and Andrew Pitts. The theory of constructions: Categorical semantics and topostheoretic models. In John Gray and Andre Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 137–199. Amer. Math. Soc, Providence RI, 1989.

[13] Peter Johnstone. Topos Theory. Academic Press, London, 1977.

[14] Peter Johnstone and Steven Vickers. Preframe presentations present. In Aurelio Carboni, Cristina Pedicchio, and Giuseppe Rosolini, editors, Category Theory — Proceedings, Como, 1990, Lecture Notes in Mathematics 1488, pages 193–212. Springer Verlag, 1991.

[15] André Joyal and Ieke Moerdijk. Algebraic Set Theory. London Mathematical Society Lecture Notes in Mathematics, number 220. Cambridge University Press, Cambridge, 1995.

[16] Donald E. Knuth. Surreal Numbers. Addison Wesley, Reading, Mass., USA, 1974.

[17] Jim Lambek and Philip Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics Vol. 7. Cambridge University Press, 1986.

[18] William Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the USA, 52:1506–1511, 1964.

[19] Adrian Mathias. The ignorance of Bourbaki. Mathematical Intelligencer, 14(3):4–13, 1992.

[Mir17a] Dimitry Mirimanoff. Les antinomies de Russell et de Burali-Forti, et le problème fondemental de la théorie des ensembles. Enseignement Mathématique, 19:37–52, 1917.

[20] Richard Montague. Well founded relations; generalisations of principles of induction and recursion. Bulletin of the American Mathematical Society, 61, 1955.

[Moo82] Gregory H. Moore. Zermelo’s Axiom of Choice. Number 8. Springer-Verlag, 1982.

[21] Andrzej Mostowski. An undecidable arithmetical statement. Fundamenta Mathematica, 36:143–164, 1949.

[22] Gerhard Osius. Categorical set theory: a characterisation of the category of sets. Journal of Pure and Applied Algebra, 4:79–119, 1974.

[23] Andrew Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[24] Andrew Pitts and Paul Taylor. A note on Russell’s Paradox in locally cartesian closed categories. Studia Logica, 48(3):377–387, 1989.

[25] William Powell. Extending Gödel’s negative interpretation to ZF. Journal of Symbolic Logic, 40:221– 229, 1975.

[26] Thoralf Skolem. Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre, in Matematikerkongressen i Helsingfors den 4–7 Juli 1922, Den femfe skandinaviska matematikenkongressen, Rodogörelse, Akademiska Bokhandeln, Helsinki, 1922, pages 217–232, Enlish translation: Some remarks on axiomatised set theory in [32], pages 290–301.

[27] Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

[28] Paul Taylor. Quantitative domains, groupoids and linear logic. In David Pitt, editor, Category Theory and Computer Science 3, Lecture Notes in Computer Science 389, pages 155–181, Springer Verlag, 1989.

[29] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[30] Paul Taylor. Practical Foundations. Cambridge University Press. (In preparation).

[31] Paul Taylor. Towards a unified theory of induction.

[32] Jan van Heijenoort. From Frege to Gödel: a Source Book in Mathematical Logic, 1879–1931. Harvard University Press, Cambridge, MA, 1967.

[33] Japie Vermeulen. A note on iterative arguments in a topos. Mathematical Proceedings of the Cambridge Philosophical Society, 111:57–62, 1992.

[34] John von Neumann. Zur Einführung der transfiniten Zahlen. Acta litterarum ac scientiarum Regiae Universitatis Hungaricae Franscisco-Josephinae, Section scientiarum mathematicarum, 1:199–208, 1923. English translation: On the introduction of transfinite numbers in [32], pages 346–354.

[35] Ernst Zermelo. Neuer Beweiss für die Möglichkeit einer Wohlordnung, Mathematische Annalen, 65:107–128, 1908. New proof that every set can be well ordered. English translation in [32], pages 183–198.

[36] Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 59:261–281, 1908. English translation: Investigations in the foundations of set theory, I in [32], pages 199–215.