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

My papers — slides — MathOverflow — the Pataraia fixed point theorem.

The purpose of Categorical Set Theory is to study
well-foundedness and extensionality *as a mathematical structure*,
using the tools of category theory, but
*stripped of its ontological pretensions*.

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.

This notion is in principle powerful enough to study quantifier complexity, although I haven’t exploited that yet.

A coalgebra is extensional if its structure map α is mono. Category theory has already contributed here, identifying exactly what is required of the underlying category and endofunctor. Principally, it has replaced “monos” with factorisation systems, to study different systems of constructive ordinals.

In set theory, extensional well founded relations provide partial models for the non-existent free algebra for the covariant powerset functor. Our techniques generalise this to other endofunctors, with or without free algebras.

The case without free algebras suggests a categorical way to approach the axiom-scheme of replacement from ZFC set theory. Transfinite iteration of functors can be expressed using the same techniques as our version of Mostowski’s extensional quotient. The aim is to give a replacement for replacement in the native language of category theory, using adjointness in foundations.

Recent work (since 2019):

Well founded coalgebras and recursion: currently with a journal referee; abstract below.

Ordinals as Coalgebras: coherent draft; abstract below.

Transfinite iteration of functors: work in progress, abstract below.

Older work (1990s):

Intuitionistic Sets and Ordinals:
*Journal of Symbolic Logic*, 61 (1996) 705–744.
Abstract

Towards a Unified Treatment of Induction: An obsolete incomplete manuscript that is only included here for the historical record; all of the material in it is superseded by the recent papers above. Abstract etc

The Fixed Point Property in Synthetic Domain Theory:
Presented at
*Logic in Computer Science* 6, Amsterdam, July 1991.
Abstract

A Fixed Point Theorem for Categories at the British Logic Colloquium in Birmingham, 7 September 2024 (abstract). See also the version of the proof on MathOverflow.

Ordinals as Coalgebras, 27 June 2024, Category Theory 2024, Santiago de Compostela.

Ordinals as Coalgebras, 23 August 2023, Symposium in honour of Andy Pitts, Cambridge.

A novel fixed point theorem, towards a replacement for replacement, 6 July 2023, Category Theory 2023, abstract and YouTube video of the lecture.

Well Founded Coalgebras, slides for a seminar given on 2 March 2023 in person in Birmingham and online at the invitation of the Logic and Semantics and Applied Category Theory research groups in Tallinn University of Technology.

Order-theoretic fixed point theorems, slides for a seminar given on 8 December 2022 in Birmingham, which was is an extended version of one given on 29 September 2022 in Ljubljana.

Free algebras for functors, without an ordinal in sight,
slides for a seminar given onn 26 April 2024
in Birmingham.
This was superseded by the *Fixed Point Theorem for Categories* above,
which has a much much simpler proof.

Miscellaneous slides from several lectures given in the 1990s. NB: This is a 21Mb scanned image of overhead projector slides in no particular order, but some of them are still interesting.

MathOverflow is the only *inter-disciplinary* site that we have for Mathematics.
So it is — or should be — the appropriate place to ask about *history*
and the *inter-relationship* of ideas.
However, whenever I have tried to use it in this way or to advertise
this research programme I have received *abuse* and at least down-votes.

So I ask my colleagues to visit the following pages, *up-vote* them
and make positive comments. Better still, *answer* the historical questions.

Constructive ordinals and Mostowski extensional reflection:

Mostowski collapses and universal extensional relational classes, asked by Martin Brandenburg in 2010 and answered by me in September 2023.

Ordinals in constructive mathematics, asked by Simon Henry in 2015 and answered by me in September 2023.

A categorical characterization of ordinal numbers, asked by Fosco Loregian in May 2014 and then answered by me.

Pataraia and Bourbaki–Witt fixed point theorems:

Bourbaki-Witt in a textbook, other than in logic, asked by me in December 2022.

A new and subtle order-theoretic fixed point theorem, ie my version of Pataraia’s theorem, asked by me in March 2023, together with my proof of the categorical version as an Answer (Seotember 2024).

That was a re-written version of Uses of Zorn’s Lemma when the thing is actually unique, asked by me in June 2020. This gives several non-constructive proofs as well as Pataraia’s constructive one. I was trying to ask whether similar ideas (especially my fifth condition) had arisen elsewhere. Unfortunately, all I got was a lecture on transfinite recursion, but the author of that was eventually persuaded to delete it.

Other history of induction and recursion:

History of well founded relations, asked by me in April 2020.

Well founded induction attributed to Noether, asked by me in 2013.

Foundations without Set Theory:

Categorical foundations without set theory,
an anonymous question with *two* answers by me in 2010.

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⇒ s x≤ 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 ⊤.

The categorical version explains where the “special condition” comes from: see the BLC24 slides and the proof on MathOverflow.

To come, but see my new translations page.

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

Sections 2 and 8 have been re-written since the November 2022 version.

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.

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. Future work will obtain much more powerful results by using this in a categorical form of Mostowski’s theorem that imposes extensionality.

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, 27 June 2024, Category Theory 2024, Santiago de Compostela.

Slides, 23 August 2023, Symposium in honour of Andy Pitts, Cambridge.

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

This yields the “thin” and “plump” ordinals
from *Intuitionistic Sets and Ordinals*
and also another system that we call “slim”,
although this is much less well behaved.

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.

However, the paper is still work in progress, so please don’t distribute or file it. As you can see from the number of declared counterexamples, this is a particularly fiddly subject and likely to be riddled with more than the usual quota of errors.

Seminar slides for Ordinals as Coalgebras, Symposium in honour of Andy Pitts, Cambridge, 23 August 2023.

This is the most common use of Replacement in mainstream mathematics.

The paper will demonstrate how “extensional quotient” *à la*
Mostowski can be used to formulate a characterisation of transfinite iteration
in the native language of category theory,

So it is in accordance with Bill Lawvere’s dictum
of using *Adjointness in Foundations*.

Please contact me if you know of other uses of Replacement that are not instances of transfinite iteration of functors.

Things like “the (2-)category of all categories” are just uses of Universes and so are not interesting.

I want to hear about areas of Mathematics that can be expressed
in its *lingua franca*, namely Category Theory.
I don’t care about problems invented by set theorists
in their obscure notation and ontology in order
to try to claim that category theory is incapable
of serving all of the foundational needs of mathematics.

What interests me about Replacement is that it builds skyscrapers out of plans on the ground. Using Universes to do this is like building them from orbiting satellites.

Based on Section 9.5 of my book Practical Foundations of Mathematics, published by Cambridge University Press in 1999.

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.
The programme that this proposes is carried out
in
*Ordinals as Coalgebras*.) - 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 done fully in
*Transfinite Iteration of Functors*.)

*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 clarifies 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.

This manuscript is obsolete and only included here for the
historical record.
All of the material in it 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.