Induction, recursion, replacement and the ordinalsPaul Taylor1990s and 2019–21 |
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.
Work in progress 2019–21 (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 required it to preserve inverse images.
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 Boubaki–Witt theorem and Zorn’s Lemma.
Abridged version, February 2020, way out of date (PDF)
See below for my 1990s work that this supersedes.
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. The many versions of this proof that are in circulation have been improved by other people and it seems to be impossible to find Pataraia’s original work.
The induction principle was apparently first identified by Martín Escardó.
The fifth 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
The recursive construction of a function f:A→Θ consists, paradigmatically, of finding a functor T and maps α:A→ T A and θ:TΘ→Θ such that f=α;T f;θ. The role of the functor T is to marshall the recursive sub-arguments, and apply the function f to them in parallel. This equation is called partial correctness of the recursive program, because we have also to show that it terminates, i.e. that the recursion (coded by α) is well founded. This may be done by finding another map g:A→ N, called a loop variant, where N is some standard well founded srtucture such as the natural numbers or ordinals. In set theory the functor T is the covariant powerset; in the study of the free algebra for a free theory Ω (such as in proof theory) it is the polynomial Σr∈Ω(−)ar(r), and it is often something very crude.
We identify the properties of the category of sets needed to prove the general recursion theorem, that these data suffice to define f uniquely. For any pullback-preserving functor T, a structure similar to the von Neumann hierarchy is developed which analyses the free T-algebra if it exists, or deputises for it otherwise. There is considerable latitude in the choice of ambient category, the functor T and the class of predicates admissible in the induction scheme. Free algebras, set theory, the familiar ordinals and novel forms of them which have arisen in theoretical computer science are treated in a uniform fashion.
The central idea in the paper is a categorical definition of well founded coalgebra α:A→ T A [as at the top of this webpage]
In particular, this proves
Parametric recursion is covered in the Exercises for Chapter VI of the book.
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.