Induction, recursion, replacement and the ordinalsPaul Taylor1990s and 2019–25 |
These pages are about my work on recursive constructions in category theory. They were called “ordinals” because I hoped to include an account of them in my book Practical Foundations of Mathematics (CUP, 1999) that would be intuitionistic and naturally expressed in terms of category theory. I did a lot of work towards that goal, but have been forced to agree with Kazimierz Kuratowski (1922) that they need to be eliminated from mathematical arguments.
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:
October 2025: There is now a draft 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. (This paper incorporates an earlier webpage about the new proof.)
So this is like Galileo’s Dialogue on the Two Great Systems of the World, which led to his condemnation by the Vatican.
Likewise, MathOverflow has censored my posting about this new proof (the most important one that I wrote on that site), but fortuitously it was archived just beforehand.
Understanding the new proof is essential background for the categorical work, so please read it first.
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. This is also included in the draft paper.
Old and New Proofs of the Order-Theoretic Fixed Point Theorem
Well founded coalgebras and recursion. Abstract
Ordinals as Coalgebras — a worked example, in particular explaining plump ordinals. Abstract
Intuitionistic Sets and Ordinals: Journal of Symbolic Logic, 61 (1996) 705–744. Abstract
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.
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. However, the 19 June 2025 version is much simpler.
Ordinals as Coalgebras, 27 June 2024, Category Theory 2024, Santiago de Compostela. See the paper above.
Free algebras for functors, without an ordinal in sight, slides for a seminar given on 26 April 2024 in Birmingham. This earlier proof was much more complicated than those above.
Ordinals as Coalgebras, 23 August 2023, Symposium in honour of Andy Pitts, Cambridge. See the paper above.
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.
Miscellaneous slides from several lectures given in the 1990s, in no particular order.
This document was translated from LATEX by HEVEA.