Induction, recursion, replacement and the ordinals

Paul Taylor

1990s and 2019–23

My papersslidesMathOverflow — 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 α:AT A for a functor T:CC is well founded if, for every mono i:UA 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.

Papers

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

Seminar Slides

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.

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.

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 questions and answers

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.

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.

Pataraia’s fixed point theorem

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:XX be an endofunction of a poset such that

Then


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 ⊤.

History and translations

To come, but see my new translations page.

Well founded coalgebras and recursion

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.

Ordinals as Coalgebras

Draft PDF

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.

Transfinite iteration of functors

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.

Practical Foundations of 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:

Intuitionistic Sets and Ordinals

Full paper (PDF)

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

Towards a Unified Treatment of Induction

Full version, c1996 (PDF)

Abstract, 1996 (PDF)

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.

The Fixed Point Property in Synthetic Domain Theory

Full paper (PDF)

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 LATEX by HEVEA.