Induction, recursion, replacement and the ordinalsPaul Taylor1990s and since 2019 |
This page was called “ordinals” because I hoped to include an intuitionistic categorical account of them in my book Practical Foundations of Mathematics (CUP, 1999). I did a lot of work towards that goal, but have been forced to agree with Kazimierz Kuratowski (1922) that ordinals need to be eliminated from mathematical arguments. Set theory has at many stages impeded progress in these matters: productive insight as come from rejecting it and following the instructions of category theory instead.
See my Review of the well founded coalgebras programme for an introduction to the whole research programme. These are the slides from a lecture at PSSL 112 in Nottingham on 28 March 2026.
Any order-preserving endofunction of a chain- or directed-complete poset with least element has a least fixed point. Associated with this are induction principles. There are three very different proofs of this:
Because of the idée fixe from Georg Cantor of “doing something infinitely often, and then some more” it never occurred to anyone (including me) to compose the functions of which they wanted the fixed point. Until Dito Pararaia did so in 1997. Unfortunately, he died in 2010 without ever writing up his “fixed point theorem”. The account by his closest colleague only says that any dcpo has a greatest inflationary monotone endofunction.
In order to make use of this in my work on well founded coalgebras below, I needed a condition I call maximality of fixed points.
Lemma If s:X→ X is an inflationary monotone endofunction of a dcpo with ⊥ such that ∀ x,y∈ X. s x=x≤ y⇒ x=y then X has a greatest element ⊤, which is the unique fixed point of s.
Corollary If φ is a predicate on such a dcpo, where φ(⊥) holds, ∀ x.φ(x)⇒φ(s x) and φ is closed under directed joins then φ(⊤) holds too.
I tried to ask whether anybody had seen this condition elsewehere, but MathOverflow censored my posting about this new proof (the most important one that I wrote on that site). Fortuitously it was archived just beforehand.
Understanding the new proof is essential background for the categorical work, so please read it first.
I channelled my anger about this bullying into writing a historical paper, called Old and New Proofs of the Order-Theoretic Fixed Point Theorem, that gives the details of all three proofs, fairly closely based on the original papers.
In connection with that study, I have translated various papers in the history of this subject, which is not as you probably believe it to be.
Here are some slides of a seminar about that history, before I had done serious work on it. (It was given on 8 December 2022 in Birmingham, as an extended version of one given on 29 September 2022 in Ljubljana.)
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.
A coalgebra is extensional if its structure map α is mono, but this idea can be made much more powerful by generalising “mono” to the M-class of a factorisation system. The “Mostowski collapse” and “rank” of a well founded relation are examples of the reflection into the subcategory of extensional well founded coalgebras.
The paper, Well founded coalgebras and recursion contains the substance of the theory, including historical material from the 1970s and 1990s.
The axiom-scheme of Replacement enables transfinite iteration of set-theoretic constructions. Other authors have either re-formulated category theory to look like the first-order axiomatisation of set theory or interpreted Replacement using Universes or maps from small objects to large ones.
Giving a new axiom in the native language of category theory (i.e. adjunctions) of comparable strength to Replacement has been open question in categorical logic since the introduction of elementary toposes in 1970.
Transfinite iteration of functors proposes as this axiom that every well founded coalgebra have an extensional reflection. This idea is generalised using fibred category theory and factorisation systems to construct transfinite iteration of functors.
I lectured on Transfinite Iteration of Functors as an Extensional Reflection at Category Theory 2026, 13 July 2026 (abstract, Zulip channel)
Discussion of set theory and Replacement is avoided in that paper, but I have a “discussion document” that I will share privately with selected colleagues who want to take part in a debate about this topic.
It derives a more general adjoint functor theorem than the extensional reflection.
I gave a lecture on an earlier version of this, called A Categorical Replacement for Replacement, at ItaCa, on 18 November 2025, of which there is a Youtube video.
This characterises well founded coalgebras for the down-sets endofunctor of posets that are extensional with respect to regular monos or down-sets. The latter are plump ordinals.
Neither of these coincides with the most commonly found definition, as transitive, extensional, well founded relations, but determined effort is put into including those in the theory.
Slides of lectures:
Ordinals as Coalgebras, 23 August 2023, Symposium in honour of Andy Pitts, Cambridge. See the paper above.
Ordinals as Coalgebras, 27 June 2024, Category Theory 2024, Santiago de Compostela.
The appropriate categorical generalisation of an inflationary monotone endofunctor is is a well pointed endofunctor: S:C→C equipped with a natural transformation σ:id→ C such that Sσ=σ S.
These were popularised in a 1980 paper by Max Kelly that made heavy use of transfinite (ordinal) constructions.
However, ordinals can be eliminated by making a generalisation of Pataraia’s observation for dcpos.
Well Pointed Endofunctors and Recursive constructions in Category Theory at the Birmingham CS Theory Lab Lunch on 19 June 2025.
This gives the proof of the order-theoretic fixed point theorem and its analogue for well pointed endofunctors. It also suggests a way in which polynomial functors could be used to generalise ordinal arithmetic.
My 1996 paper that the work above develops.
Intuitionistic Sets and Ordinals: Journal of Symbolic Logic, 61 (1996) 705–744. Abstract
This document was translated from LATEX by HEVEA.