Re: coinduction

[Charles Wells <cfw2@po.cwru.edu>]

In brief:  If a structure has no nontrivial substructures, you can prove a
property P is true of everything in the structure by proving that the elements
with property P form a nonempty substructure.  Take the structure to be N with
the unary operation of successor and you get induction.  Now say that in the
opposite category:  If a structure has no nontrivial congruences, you can prove
that two objects are equal if they are equivalent under any congruence.  (You
can define "definition by coinduction" by a similar dualization.)  This has
found many applications in computer science (where the congruence is
bisimulation).  See J.J.M.M. Rutten, Universal coalgebra: a theory of systems.
Theoretical Computer Science 249(1), 2000, pp. 3-80 and other papers by him on
his website:  http://www.cwi.nl/~janr/papers/ 

--Charles Wells

>can anyone explain coinduction?
>in what sense it dual to induction?
>does it relate to the basic picture for a NNO?
>is there a (meaningful) concept of co-recursion?
>what would be the appropriate internal language?
>how is it used to prove theorems?
>
>Al Vilcius
>al.r@vilcius.com
>
>
>



Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, USA.
email: charles@freude.com. 
home phone: 440 774 1926.  
professional website: http://www.cwru.edu/artsci/math/wells/home.html
personal website: http://www.oberlin.net/~cwells/index.html
NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm