but wouldn't it be nice to keep the standard definition of induction, which says that the equations
f(0) = c f(n+1) = g(f(n))
determine a unique f, given c and g? this is the definition that most first year
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).
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. 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. -- dusko