Dusko Pavlovic <dusko@kestrel.edu> writes:

...

I have always considered the statement regarding existence of a unique function f to be the principle of recursion.

the recursion schema, as defined by godel in 1930, is a bit stronger: g is allowed to depend on n, not only on f(n).

Yes, I overlooked that point. But, is that principle any stronger than the principle you called induction? I think it isn't, given products in our category. Let N be the initial successor algebra. Let c be in X and g:N x X -> X. To define a function f such that f(0) = c f(n+1) = g(n,f(n)), I just have to cook up the appropriate structure map for N x X. I think that <s o p_1,g> + <0,c>: (N x X) + 1 -> N x X does it (p_1 is the projection map). Let <k,f>: N -> N x X be the unique function guaranteed by initiality. One can show that f satisfies the equations above. (Along the way, one shows that k is the identity.) (To add other parameters, one needs exponentials. For instance, given h:A -> X g:A x N x X -> X to show that there is a unique f such that f(a,0) = h(a) f(a,n+1) = g(a,n,f(a,n)) requires a structure map for (X x N)^A, if I'm not mistaken.) This shows that Godel's principle of recursion is equivalent to the statement "N is an initial algebra". I.e., it is equivalent to the statement that there is a unique f such that f(0) = c f(n+1) = g(f(n)).

...

The principle of induction is, in my mind, the weaker principle that says that if a property holds of 0 and is closed under successor, then it holds of N.

in a topos, this principle is equivalent with the above schema. and the schema itself, of course, just means that [0,s] : 1+N --> N is initial: any algebra [c,g] : 1+X --> X induces a unique homomorphism f : N-->X. using the exponents, we do recursion.

I am confused by this statement. My principle of induction for successor algebras [0_X,s_X]:1+X -> X is this: For all subsets P of X, if 0_X is in P and P is closed under s_X, then P = X. (Categorically, an algebra satisfies the principle of induction if it contains no proper subalgebras.) Consider the successor algebra X={x}, with the evident structure map [0_X,s_X]:1+X -> X. Surely, for every subset P of X, if 0_X is in P and P is closed under s_X, then P = X. In other words, the algebra X satisfies the principle of induction in the sense that I gave. This seems to contradict the equivalence you mention. What am I overlooking?

as i said last time, induction and recursion have been in heavy use for so long, that they really don't leave much space for redefining, even for the sake of symmetry with coinduction and corecursion.

I quite agree, but I didn't redefine induction, as far as I am concerned. I learned that induction was the proof principle as I stated it and that recursion is the principle regarding the definition of functions many years ago. I think that our disagreement in definitions is a disagreement that one will find elsewhere in the literature. I also suppose that the term coinduction (as I use it) arose from the definition of induction that I offered. Are others unfamiliar with the distinction between induction and recursion as I drew it? I assumed it was a more or less conventional distinction. If my use is really idiosyncratic, then I'd be happy to drop it. -- Jesse Hughes "Such behaviour is exclusively confined to functions invented by mathematicians for the sake of causing trouble." -Albert Eagle's _A Practical Treatise on Fourier's Theorem_