Induction, recursion, replacement and the ordinals

Paul Taylor

My chief contribution to this subject is the notion of "well founded coalgebra", which is described briefly in the "extended abstract" below and also Sections 2.5, 6.3, 6.7 and 9.5 of my book, Practical Foundations of Mathematics. The detailed treatment is in the full paper that is the second item below.

In particular, this proves

the equivalence between my notion of well-foundedness (induction) and the recursion scheme due to Osius, for endofunctors of Set that preserve inverse images,
that, if the functor has an initial algebra, a coalgebra for it is well founded iff it has a coalgebra homomorphism to the initial algebra, and
that extensional well founded coalgebras behave in many ways like sets (of the set-theoretic kind), in particular their coproducts "overlap" in a similar way, and are idempotent like joins in a lattice.

Parametric recursion is covered in the Exercises for Chapter VI of the book.

The earlier JSL paper on Intutionistic Sets and Ordinals treats them in the normal mathematical way, as carriers together with structure (a binary relation called ε), in any elementary topos. Mostowski's theorem, in the form of the extensional quotient of any well founded relation, is proved without replacement.

The classical notion of ordinal splits into several versions when considered intuitionistically. These are characterised in a quasi-set-theoretic fashion in my JSL paper, categorically in Section 6.7 of the book and algebraically by Joyal and Moerdijk in their book Algebraic Set Theory.

Section 9.5 of the book 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.

Towards a Unified Treatment of Induction (Extended Abstract)

PDF (156 kb)
DVI (30 kb)
PostScript (compressed) (54 kb)
A5 PS booklet (compressed) (48 kb)
What are these?
[12 Feb 2009]

Presented at Logical Foundations of Mathematics, Computer Science and Physics - Kurt Gödel's Legacy (Gödel '96), Brno, 26 August 1996. This extended abstract was circulated at the meeting, as the paper did not appear in the printed proceedings.

This work had also been presented at Category Theory 1995 in Cambridge on 8 August 1995.

Here are the slides that I used at these two conferences and other seminars. NB: This file is a 21Mb scanned image of a merged collection of overhead projector slides from several lectures.

Towards a Unified Treatment of Induction~I: the General Recursion Theorem

PDF (349 kb)
DVI (206 kb)
PostScript (compressed) (242 kb)
A5 PS booklet (compressed) (225 kb)
What are these?
[12 Feb 2009]

Written in 1995-6, circulated in Brno and elsewhere and available on my web page 1996-2003 and from 2006.

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.

Intuitionistic Sets and Ordinals

PDF (411 kb)
DVI (175 kb)
PostScript (compressed) (153 kb)
A5 PS booklet (compressed) (141 kb)
What are these?
[12 Feb 2009]

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.

The Fixed Point Property in Synthetic Domain Theory

This paper is not available to download.

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 is www.PaulTaylor.EU/ordinals/index.php and it was derived from ordinals/index.tex which was last modified on 13 February 2009.