## Induction, recursion, replacement and the ordinals## Paul Taylor## 1990s and 2019–23 |

A coalgebra α:A → T A for a functor T:C→C is well founded if, for every mono i:U ↪ A such that the pullback H factors through U in the diagram on the left, the map i must be an isomorphism.

Under conditions that are discussed in the papers below, any well founded coalgebra satisfies the recursion scheme that, for any algebra θ:T θ→Θ, there is a unique map f:A→Θ making the square on the right commute.

Thursday, 2 March 2023 at 14:00 UTC: “Well Founded Coalgebras”: Birmingham abstract and slides. In fact this is held at the invitation of the Logic and Semantics and Applied Category Theory research groups in Tallinn University of Technology.

8 December 2022: “Order-theoretic fixed point theorems”: abstract and slides for a seminar in Birmingham. This is an extended version of a seminar in Ljubljana on 29 September 2022.

1990s: miscellaneous slides from several lectures in that period. NB: This is a 21Mb scanned image of overhead projector slides in no particular order, but still contains some interesting ideas.

2019–22 paper currently with a journal referee (PDF).

We define well founded coalgebras and prove the recursion theorem for them: that there is a unique coalgebra-to-algebra homomorphism to any algebra for the same functor. The functor must preserve monos, whereas earlier work also required it to preserve their pullbacks. The argument is based on von Neumann’s recursion theorem for ordinals. Extensional well founded coalgebras are seen as initial segments of the free algebra, even when that does not exist. We have a categorical form of Mostowski’s theorem that imposes extensionality.

The assumptions about the underlying category, originally sets, are examined thoroughly, with a view to ambitious generalisation. In particular, the “monos” used for predicates and extensionality are replaced by a factorisation system.

These proofs exploit Pataraia’s fixed point theorem for dcpos, which Section 2 advocates (independently of the rest of the paper) for much wider deployment as a much prettier (as well as constructive) replacement for the use of the ordinals, the Bourbaki–Witt theorem and Zorn’s Lemma.

See below for my 1990s work that this supersedes.

Slides of my seminar on 9 December 2022

For the central induction results in
*Well founded coalgebras and recursion*
I needed to use the following novel principle:

Let s:X→ X be an endofunction of a poset such that

- X has a least element ⊥;
- X has joins of directed subsets (or chains, classically),
- s is monotone: ∀ x y.x≤ y⇒ sx≤ s y;
- s is inflationary: ∀ x.x≤ s x;
- the
*special condition*, ∀ x y.x=s x≤ y=s y⇒ x=y.

Then

- X has a greatest element ⊤;
- ⊤ is the unique fixed point of s;
- if ⊥ satisfies some predicate and it is preserved by s and directed joins then it holds for ⊤.

The constructive proof for the related fixed point theorem was found by Dito Pataraia in 1996 but he never published it and died in 2011. His proof was dramatically simplified by Alex Simpson and the above is a further simplification of that. The induction principle was apparently first identified by Martín Escardó.

The *special condition* above seems to be new with me;
it is what is needed to force X to have ⊤.

There are also several non-constructive proofs and further discussion on MathOverflow, where I was trying to ask whether similar ideas (especially my fifth condition) had arisen elsewhere. Unfortunately, all I got was a lecture on the ancient history of this subject.

This is nowhere near ready for distribution, although I’m willing to provide the current draft for private discussion.

It works out the theory from *Well Founded Coalgebras and Recursion*
in the category of posets (maybe others) using both
general subsets with the restricted order and lower subsets
as the class of “monos”.

These appear to yield the “thin” and “plump” ordinals
from *Intuitionistic Sets and Ordinals*.

The first few plump ordinals are calculated in the topos of presheaves on a single arrow over classical sets, showing that this requires Replacement for ω· 2.

It is also demonstrated how “extensional quotient” *à la*
Mostowski can be used to formulate the definition of transfinite
iteration of a functor.
That is the most common use of Replacement in mainstream
mathematics.

My work on this topic in the 1990s is described briefly in my book Practical Foundations of Mathematics, published by Cambridge University Press in 1999:

- Section 2.5: Induction and Recursion.
- Section 6.3:
The General Recursion Theorem:
the main result, for endofunctors of a topos that preserve inverse images.
(This is substantially generalised in
*Well founded coalgebras and recursion*.) - Section 6.7: The Ordinals:
with a brief account of how different kinds of ordinals
are the extensional well founded coalgebras for endofunctors.
(This will be covered thoroughly in
*Ordinals in Categories*.) - Exercises for Chapter VI: including parametric recursion.
- Section 9.5: Universes: this
concludes with a sketch of how extensional well founded coalgebras
may be used to characterise ordinal iteration of functors in an
elementary way, and thereby formulate a version of the axiom-scheme
of replacement.
(This will be covered in
*Ordinals in Categories*.)

*Journal of Symbolic Logic*, 61 (1996) 705–744

Presented at Category Theory and Computer Science 5, Amsterdam, September 1993.

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≤ s x, monotonicity or s(x∨ y)≤ s x∨ s y.

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.

slides (scanned PDF) NB: This file is a 21Mb scanned image of a merged collection of overhead projector slides from several lectures.

All of the material in this paper is superseded by
*Well founded coalgebras and recursion* above.

Presented at
*Logic in Computer Science* 6, Amsterdam, July 1991.

We present an elementary axiomatisation of synthetic domain theory
and show that it is sufficient to deduce the fixed point property
and solve domain equations. Models of these axioms based on partial
equivalence relations have received much attention, but there are
also very simple sheaf models based on classical domain theory. In
any case the aim of this paper is to show that an important theorem
can be derived from an *abstract axiomatisation,* rather than
from a particular model. Also, by providing a common framework in
which both PER and classical models can be expressed, this work
builds a bridge between the two.

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.