I wonder whether anyone has done an investigation (in either a journal paper or web-accessible lecture notes) of the way in which the natural numbers object has to be re-defined in categories with weak logic. It is well known, for example, that in a category that (has finite products but) is not cartesian closed, parameters have to be added explicitly to the definition, yielding a diagram of the form zero succ Gamma --------> N x Gamma <-------- N x Gamma || . . || . . || . rec . <left, rec> || . . || base V step V Gamma -----------> X <------------- N x X (where, as in proof & type theory, I use Gamma for an arbitrary object, or context of parameters). If the category is cartesian closed then this diagram may be rewritten with the exponential X^Gamma in place of X, the object Gamma itself being removed from the top line. The corresponding recursion scheme is written symbolically as Gamma |- base : X Gamma, n:N, x:X |- step (n,x) : X -------------------------------------------------------------- Gamma, n:N |- rec (n, base, step) : X with beta-rules Gamma |- rec (zero, base, step) = base : X Gamma, n:N |- rec (succ(n), base, step) = step (n, rec (n, base, step)) By the way, we call this "recursion at type X", the point being that as the class of types at which the recursion scheme is asserted grows, so considerably does the power of the logic. A similar generalisation is needed when we want to argue about equations: - I have terms Gamma, n:N, x:X |- a_n, b_n : X, - I prove a base case Gamma |- a_0 = b_0 : X - and an induction step that Gamma, n:N, x:X, a_n = b_n : X |- a_n+1 = b_n+1 : X - From these I want to deduce that Gamma, n:N, x:X |- a_n = b_n : X without assumption. Notice that I said nothing about how a_n and b_n themselves were defined. Indeed, if they had been defined by the same base and step maps on X, they would be equal by the uniqueness hypothesis of the universal property - otherwise known as the eta rule for recursion. To give a simple example to show that we need more than this uniqueness, let b_n=b be constant and a_0 = f u, a_1 = f(s u), a_2 = f(s(s(u)), etc where f: X---> Y and s : Y ---> Y so that the sequence a_n itself is not defined by an endofunction. We can apply the ordinary recursion scheme to this example by considering the subtype or equaliser f ------> Z = { y:Y | f y = b } >------> Y X ------> b since the endofunction s : Y --> Y restricts to Z. In fact, the general equational recursion scheme can be derived from a different equaliser: a_n ------> E = { n:N | a_n = b_n : X} >------> Gamma x N X ------> b_n The base case says that zero : Gamma x N -> N factors through E, whilst the induction step says that succ restricts to a map E -> E. Then the above parametric recursion scheme provides an inverse rec_E : Gamma x N ---> E to the inclusion, one equation being given by uniqueness of rec_N : Gamma x N ---> Gamma x N and the other by the fact that E >---> Gamma x N is mono. As you may have guessed, I became concerned by this issue because I am interested in a certain category that does not have general equalisers, so I will need to assert a more complicated recursion scheme in my case. These two generalisations of the beautifully simple Dedekind -- Peano -- Lawvere definition of the natural numbers are beginning to feel like the thin end of a wedge. Presumably be have to make a further alteration to the definition for every propositional and type connective in our logic. Alternatively, we can consider the situation in set theory or an elementary topos. The equational recursion scheme is valid there because we have equalisers, and we may consider in particular the case where X = Omega is the subobject classifier and b_n=true. This gives Peano induction straight away. We get from a given category to the topos situation by means of a Yoneda embedding, though unfortunately not simply into a presheaf topos or functor category. There has to be a Grothendieck topology to make the representable object N from our category coincide with the constant sheaf whose value is N from Set. Actually, we can unwind this situation and re-express it in terms of elementary category theory or type theory. Let Gamma, n:N |- phi(n) be the predicate that we want to prove generally true by induction. This predicate, like any term, may be shifted from one context Gamma to another one Delta by a multiple substitution of a term using variables from Gamma for each typed variable in Delta. Categorically, this just means the composite u x id phi Delta x N --------> Gamma x N -----> Omega Now phi may actually be true in some particular context Gamma, but not in another one Delta. Those contexts in which it is true form a category, or alternatively a sheaf or sieve on the original category. This sieve is the truth-value of phi in the sheaf topos. I think symbolic logic has language for this situation, possibly involving the word "realises", but I'm not sure at the moment what this is. Let S be this sieve. Like E above, it has a map (natural transformation) E ---> N. If the sieve S is representable by an actual subobject of N in the original category, the same argument as above provides an inverse N ---> S, whence S is the whole of N. (A sieve S is representable by an object U if S consists of all of the maps into U). We can see parametric and equational recursion in terms of this sieve. In the equational case, S consists of all maps to Gamma x N that have equal composites with a_n and b_n. The sieve is representable iff it has a terminal object, which is called the equaliser. In the parametric case, the terminal object of the sieve is the exponential X^Gamma. The general form of the recursion scheme in a category with weak logic that we do not want to embed in a topos therefore appears to be this: N admits recursion at the sieve (cf type) S for whatever generality of sieves we care to choose. Since a sieve is the external manifestation of a subset in the topos, what we have said is that any sieve (of the chosen generality) that contains zero and is closed under successor is the whole of N. In other words, N admits induction or is well founded with respect to such sieves as predicates. Maybe I've just answered my own question, but if someone else has worked on this and written it up more fully then I would like to know. Paul Taylor www.cs.man.ac.uk/~pt