Re: coinduction: definable equationally?

[jesse@andrew.cmu.edu (Jesse F. Hughes)]

Vaughan Pratt <pratt@cs.stanford.edu> writes:

> 1.  Is there a variety embedding coinduction?
> 
> Jesse Hughes distinguishes induction from recursion in terms of natural
> numbers.  For him induction is Peano's mathematical induction, while
> recursion is the uniqueness of the map from the (unique up to a unique
> isomorphism) initial algebra to an arbitrary algebra.
> 

This doesn't look like what I had in mind, exactly.  Peano's
mathematical induction was meant as an example of induction, not the
whole meaning of induction.  I stated induction in terms of natural
numbers only to continue Dusko's example.  I'm afraid that I was a bit
vague in what exactly induction is in my previous post.

I say that a G-algebra A satisfies the principle of induction just in
case every mono G-homomorphism into A is an isomorphism.  If our base
category has equalizers, then A satisfies the principle of induction
just in case, for every algebra B, there is at most one homomorphism 
A -> B.  So induction is the uniqueness part of initiality.

What's recursion, then?  As far as I'm concerned, recursion is just
initiality.  I.e., an algebra A satisfies the principle of definition
by recursion just in case it is the initial algebra.  (Why not take
recursion to be just the existence part?  I haven't seen much use for
just the existence part and it also doesn't fit well with conventional
usage.)  Clearly, on this view, the principle of recursion implies the
principle of induction, but the converse is not the case.

I hope that my idea of induction is a bit clearer.  I really must
learn to write more precisely.
-- 
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_