From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1673 Path: news.gmane.org!not-for-mail From: Dusko Pavlovic Newsgroups: gmane.science.mathematics.categories Subject: Re: coinduction Date: Sun, 29 Oct 2000 19:38:08 -0800 Message-ID: <39FCED20.9EC15DBD@kestrel.edu> References: <87itqexbja.fsf@phiwumbda.dyndns.org> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018011 32357 80.91.229.2 (29 Apr 2009 15:13:31 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:13:31 +0000 (UTC) To: "Categories@Mta. Ca" Original-X-From: rrosebru@mta.ca Mon Oct 30 14:26:39 2000 -0400 Return-Path: Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UHljU03310 for categories-list; Mon, 30 Oct 2000 13:47:45 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 31 Original-Lines: 32 Xref: news.gmane.org gmane.science.mathematics.categories:1673 Archived-At: > > 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