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