Induction, recursion, replacement and the ordinalsPaul Taylor1990s and 2019–22 |
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.
Slides of my seminar on 9 December 2022
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
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 ⊤.
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:
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 LATEX by HEVEA.