Towards a Unified Treatment of Induction (Abstract)

Paul Taylor

26 August 1996

Mathematical induction over the nat-

ural numbers has been familiar since Euclid, Fermat, Dedekind and Peano. It was unified with ∈-induction in Set Theory by generaling the successor n ≺ n + 1 to a well founded relation, i.e. one which satisfies the induction scheme

∀a. (∀x. x ≺ a ⇒ ϕ[x]) ⇒ ϕ[a] ; ∀a. ϕ[a]

(the definitions using minimal counterexamples or descending sequences cannot be used intuitionistically).

In proof theory, type theory and computer science, structural induction on lists, trees, etc. is more important, where ≺ is the immediate subexpression relation. However in both theoretical computer science and software engineering it is also necessary to be able to reason in an inductive idiom for non-terminating processes and ill founded recursion. One technique for doing this, known as Scott induction after the set theorist turned semanticist Dana Scott, is formally the same as well founded induction, except that the predicate ϕ[x] must be ā priori closed under joins of ascending chains in a suitable order structure.

My aim is to unify these methods, apply them to new circumstances and also to understand the role of the axiom of replacement. I would like to express this axiom-scheme, or at least the existence of transfinite iterates of functors, in an elementary way.

Category theory has shown that universal properties or adjunctions provide an extremely powerful unifying principle for constructions throughout mathematics. As a doctoral student in the early 1960s, Bill Lawvere’s avowed aim (in the face of severe skepticism even from the foremost categorists) was to do set theory without elements. Amongst many other major contributions, he identified the quantifiers as adjoints to substitution and the universal property of the natural numbers:

ℕ < s ℕ
1  z >
Θ^{\begin{matrix}p \\ ∨ \end{matrix} . . . . . . . . . . . . . .}< s_{Θ}^{z_{Θ} >}  Θ^{\begin{matrix}p \\ ∨ \end{matrix} . . . . . . . . . . . . . .}

He and Myles Tierney later found the axioms for an elementary topos, which are essentially equivalent to an intuitionistic form of Zermelo’s original set theory. The first order properties of the category of sets relevant to universal algebra had also been identified as stable disjoint sums and stable effective quotients of equivalence relations. These axioms do not however capture replacement at all.

The very general nature of universal properties — the fact that this mode of description applies to so many other mathematical phenomena, including the quantifiers — means that we no longer have a “hands on” appreciation of the parsing and induction properties of term algebras. These two (characteristic) features drive the unification algorithm used in logic programming. Categorists, and also workers in the algebraic methodology of programming, have also almost invariably presupposed the existence of initial algebras, and so have been unable to deal with induction involving functors without rank, such as the powerset.

Many treatments have been given of typetheoretic internal languages in toposes, but Gerhard Osius came closest to a categorical account of set theory. He defined a transitive set object as a carrier (object of the topos) A together with a monomorphism parse : A ↪ P(A), which you should think of as a ↦ {x : x ≺ a}, satisfying the Definition The recursion scheme.

P(A) \overline{\begin{matrix}P(p) \\ > \end{matrix}} P(Θ)

A^{parse∧}  \overline{p >} Θ \begin{matrix}ev \\ ∨ \end{matrix}

For any object Θ and morphism ev : P(Θ) → Θ, there is a unique function p : A → Θ such that

p = parse ; P(p) ; ev

or, for each a ∈ A,

p(a) = ev( {p(x) : x ≺ a} ).

The present work develops Osius’s ideas, but with any functor T (so long as it preserves monos and inverse images) instead of the covariant powerset functor P. Any morphism parse : A → T (A) is called a T -coalgebra, so a P-coalgebra exactly codes a binary relation on A, which is extensional iff parse is mono.

Example Let T take any object X to the disjoint union 1 + X and the morphism p : X → Y to id + p : 1 + X → 1 + Y, i.e. the same function on these objects and the identity on the constant extra component.

1 + ℕ \overline{id + p>} 1 + Θ

ℕ \begin{matrix}[z, s] \\ ∨ \end{matrix} ^{∧parse} \overline{p >} Θ \begin{matrix}[z_{Θ}, s_{Θ}] \\ ∨ \end{matrix}

ℕ is a “fixed point” of this functor in the sense of the isomorphism shown, where the notation [z, s] says what to do on each component of the sum, and Osius’s recursion scheme reduces to Lawvere’s. □

Example Let T (X) = ℕ+X and T (p) = id+p.

ℕ + (ℕ × ℕ) \overline{\begin{matrix}id + p \\ > \end{matrix}} ℕ + ℕ

ℕ × ℕ^{parse∧}  \overline{p >} ℕ \begin{matrix}[id, id] \\ ∨ \end{matrix}

This diagram codes the Euclidean algorithm, where

parse(n, m) = \{ \begin{matrix}m ∈ ℕ & if n = 0 \\ (m mod n, n) ∈ ℕ × ℕ & otherwise \end{matrix} This is typical of tail recursion, but Osius’s diagram expresses a general paradigm for recursive functions: take the argument apart, call the function for each sub-argument, and put the results back together. The functor T marshals the sub-arguments (plural, using terms X^{n}) and makes the recursive calls in parallel.

Using a “polynomial” functor T (X) = ∑_{r} X^{ar(r)}, results from set theory can be applied to structural recursion over (infinitary) term algebras.

Osius’s diagram expresses recursion, but what about induction? In the diagram

\begin{aligned}P(U) & ^{⊂}  P(i) > & P(A) \\ H & ∧ & ^{⊂}  > & U & ^{⊂} i > & A, & ^{∧parse} \end{aligned}

where U = {a ∈ A : ϕ[a]}, the pullback is

H = {(a, V) : a ∈ A, parse(a) = V ⊂ U ⊂ A}
≅ {a ∈ A : ∀x ∈ A. x ≺ a ⇒ ϕ[x]} ,

so the inclusion H ⊂ U ⊂ A says that

∀a ∈ A. (∀x ∈ A. x ≺ a ⇒ ϕ[x]) ⇒ ϕ[a],

which is the premise of the induction scheme.

Definition (mine) For any functor T, we say that parse : A → T (A) is a well founded coalgebra if, in any such pullback diagram, in fact i : U ≅ A.

Lemma (Osius) For transitive set objects U and A, we have U ⊂ A in the set-theoretic sense iff there is a function i : U → A making the square

P(U) ^{⊂} \begin{matrix}P(i) \\ > \end{matrix} P(A)

U^{parse_{U}_{∪} ∧} ^{⊂} i > A^{parse_{A}_{∪} ∧}

commute. Such a map is called a coalgebra homomorphism in category theory and a simulation in process algebra; here it is unique and injective. □

Instead of “transitive set” I use the term ensemble for an extensional well founded T - coalgebra.

Proposition • ∅ → T (∅) is an ensemble;

• if parse_{A} : A ↪ T (A) is an ensemble then so is T (parse_{A}) : T (A) ↪ T^{2}(A);

• if parse_{A} : A ↪ T (A) is an ensemble and i : U ↪ A is a coalgebra monomorphism then parse_{U} : U ↪ T (U) is also an ensemble, and

• unions (with respect to coalgebra monomorphisms) of ensembles are again ensembles.

Moreover any subclass of ensembles with these closure conditions consists of all of them. □

Theorem General recursion. Well-foundedness suffices to solve the recursion equation uniquely. (Conversely, with ⋂ : P^{2}(1) → P(1) for Θ, wellfoundedness is necessary for uniqueness.) Proof The purpose of a generalisation such as this is to allow the objects A and Θ and the associated morphisms to belong to some other category S besides the category of sets and functions (or a topos) from which the ideas came. The proof is the usual one, with attempts (partial solutions), but we must identify what properties of S are needed. In particular it must have a strict initial object (∅), and for any two subobjects U, V ⊂ X, the diagram

\begin{aligned}U & ^{⊂} > & U ∪_{X} V \\ U ∩_{X} V & ^{^{∪} ∧} & ^{⊂} > & V & ^{^{∪} ∧} \end{aligned}

must be a pushout. That is, given functions U → Θ and V → Θ agreeing on U ∩ V, there must be a unique extension to U ∪ V → Θ. □

The test object ev : T (Θ) → Θ is called a T - algebra. If there is a well founded T -coalgebra parse : I ≅ T (I), then parse^{−1} : T (I) → I is the initial T -algebra. In this case the ensembles are exactly the sub-coalgebras of I. Classically this happens if T has rank, but the notion of rank depends on classical set theory. For the powerset, the ensembles form the von Neumann hierarchy, a top-less complete class lattice. Settheoretic intersection and union can be defined for T -ensembles, and we recover most of set theory (apart from the ordered pair formula, which was obfuscation anyway).

Well-foundedness can be considered without extensionality, which may be recovered by the Mostowski collapse

p(a) = {p(x) : x ≺ a} .

This is a surjective coalgebra homomorphism, and is the universal such. It can be constructed as a quotient by a recursively defined equivalence relation, without using the axiom of replacement [12].

The notion of “mono” used both in the induction scheme and in defining extensionality need not be the absolute one in category theory (the cancellation property). Indeed it is already customary in proof theory to confine the predicates ϕ[x] to which the induction scheme applies to some specified class. One undesirable predicate is (x ⊀ x), as induction for this says that well founded relations are always irreflexive. Fewer “monos” means that there are more “epis” than surjective functions in the epi-mono factorisation of morphisms, and then the generalised Mostowski theorem does need replacement.

Example Let S = Pos, the category of posets and monotone functions, and let L be the functor which is like the powerset, except that each U ∈ L(X, ≤) is to be a lower set, i.e. ∀u ∈ U. ∀x ∈ X. x ≤ u ⇒ x ∈ U. Now the function parse : A → L(A) is monotone iff

y ≤ x ≺ a ≤ b ⇒ y ≺ b

where ≺ is the binary relation associated to parse as before. Interesting things happen if we modify the notion of “mono” and hence “extensional”:

• if A carries the restricted order induced by parse : A ↪ L(A) then ≺ is transitive (in the order-theoretic sense), but the converse does not hold;

• if also parse makes A a lower set of L(A) then

C ⊂ parse(b)∧b ≺ a ⇒ ∃!c ∈ A. C = parse(c),

or γ ⊂ β ∈ α ⇒ γ ∈ α in traditional notation.

In a much more symbolic style, I introduced structures with the second property as plump ordinals in my analysis of Intuitionistic sets and ordinals. Whereas the successor α^{+} = α ∪ {α} for transitive well founded relations satisfies

\begin{aligned}β^{+} ≺ α^{+} & ⟹ & β^{+} ⊂ α & ⟺ & β ≺ α \\ β^{+} ⊂ α^{+} & ⟺ & β ≺ α^{+} & ⟹ & β ⊂ α, \end{aligned}

the successor for plump ordinals, given by

α^{+} = {β ⊂ α : β is a plump ordinal} ,

makes all of the implications reversible. It appears that we need replacement to construct plump ω, the Mostowski “collapse” of (ℕ, <).

Considering instead the category of semilattices (in the binary sense only) and homomorphisms, the ensembles are directed ordinals (this is not automatic intuitionistically). Moving on to predomains (posets with joins of directed subsets) and Scott-continuous functions (those which preserve these joins), one can define ordinals which — pace Burali-Forti, whose centenary is almost upon us — have fixed points of the successor function.

There is also a more abstract approach to the ordinals which arises if the functor T is part of a monad; this endows the ensembles with partial successor and “union” operations automatically. Eugenio Moggi has argued for monads as a notion of computation. Roy Crole and Andrew Pitts have constructed “fixed point objects” for them.

Induction proves new theorems about existing terms, but recursion generates new terms of existing types. The next stage is to generate new types by iterating functors. This is to be done transfinitely by forming unions or colimits at limit stages. For example the sequences ℵ_{α} and ℶ_{α} are obtained from ℵ_{0} = ℶ_{0} = ℕ by iterating the Hartogs and powerset functors. This needs replacement.

Another use of replacement is to collect in one place infinitely much data which we already have in our possession, for example to define infinitary colimits. In fact Jean Bénabou has shown how replacement can be avoided for this purpose. Essentially, he says that the data already form a single object anyway.

For example, the family {X_{β} : β ∈ α} is coded by the disjoint union

\begin{matrix}X ≡ ∐_{β∈α} X_{β} & x ∈ X_{β} \\ α & ∨ & β ∈ α & ∨ \end{matrix}

and we are interested in the case X_{β} = T^{β}(∅), where α is an ordinal. In fact X_{(−)} : α → Set is to be a functor or diagram: for each γ ≤ β in α we intend there to be a morphism X_{γ} → X_{β}; then X → α is in fact a discrete fibration of posets.

We regard X → α as an object of a category Pos^{→}, whose morphisms are commutative squares

\begin{matrix}Z & \overline{>} & Y \\ γ & ∨ & \overline{i >} & β & ∨ \end{matrix}

in Pos. The above results apply to this category.

For any lower set U ⊂ α, we want to define

Y_{U} = colim_{β∈U} T (X_{β})

where the colimit is with respect to the subdiagram restricted to U. In the Bénabou style, this colimit is simply the set of order-connected components, without using replacement.

Theorem Let \overline{T} : Pos^{→} → Pos^{→} be the functor which takes the object X → α to the object

\begin{matrix}∐_{U∈L(α)} Y_{U} & y & ∈ Y_{U} = colim_{γ∈U} T (X_{γ}) \\ L(α) & ∨ & U. & ∨ \end{matrix}

Then the square

\begin{matrix}X & \overline{>} & Y \\ α & ∨ & \overline{\begin{matrix}parse \\ > \end{matrix}} & L(α) & ∨ \end{matrix}

is a pullback iff the fibres over each β and parse(β) are isomorphic:

X_{β} ≅ colim_{γ≺β} T (X_{γ}),

i.e. we have the transfinite iteration of T. □ This characterisation is an example of generalised extensionality, since we may call a square (morphism of Pos^{→}) “mono” if it is a pullback and “epi” if the bottom map i is an isomorphism.

Example Well-foundedness of α is necessary:

X \overline{≅ >} P(X) V

\{⋆\} ∨ \overline{\begin{matrix}parse \\ > \end{matrix}} L(\{⋆\}) ∨ \{⋆\} ∨
⋆  > {⋆}

As a test of my theory, as I want to prove the

Conjecture Let Θ be a domain (predomain with least element ⊥) and s : Θ → Θ a monotone (not necessarily continuous) function. Then s has a least fixed point.

This can be proved classically using ordinals and Hartogs’ Lemma, and Tarski proved it intuitionistically for complete lattices. André Joyal and Ieke Moerdijk have recently derived it from an axiom of collection expressed in a categorical way (which is not the same as mine and Osius’s).

Peter Freyd has proposed as an axiom for domain theory that the initial algebra I and final coalgebra F for any functor T exist and I ≅ F. Any category with this property has a zero object, so my technique is not directly applicable, but I would like to find a way of stating the coincidence without presupposing the existence of I and F, i.e. that T has rank.

Other active research in this area is based on the effective topos [4], whose roots lie in Kleene realisability. The wider aim, synthetic domain theory, is to unify topological ideas with recursion theory.

References

[1] Jean Bénabou. Fibred categories and the foundations of naïve category theory. Journal of Symbolic Logic, 50(1):10–37, 1985.

[2] Roy L. Crole and Andrew M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Information and Computation, 98(2):171–210, June 1992.

[3] Peter J. Freyd. Remarks on algebraically compact categories. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science: Proceedings of the LMS Symposium, Durham, 1991, LMS Lecture Notes 177. Cambridge University Press, 1992.

[4] J. Martin E. Hyland. The effective topos. In Anne Sjerp Troelstra and Dirk van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics, 110, pages 165–216. North-Holland, Amsterdam, 1982.

[5] André Joyal and Ieke Moerdijk. Algebraic Set Theory. LMS Lecture Notes 220. Cambridge University Press, 1995.

[6] Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, 7. Cambridge University Press, 1986.

[7] F. William Lawvere. Adjointness in foundations. Dialectica, 23:281–296, 1969.

[8] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[9] Gerhard Osius. Categorical set theory: a characterisation of the category of sets. Journal of Pure and Applied Algebra, 4:79–119, 1974.

[10] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[11] Paul Taylor. Practical Foundations. Cambridge University Press, 1997 (In preparation).

[12] Paul Taylor. Intuitionistic sets and ordinals. Journal of Symbolic Logic, September 1996.