Re: Topos logic arises naturally

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

I did not want to deny the need of mathematical thought, but I found
this example of topos theory emerging unexpectedly quite pleasing.

Note that the mail is *not* about Isabelle. Admittedly, I do not
know anything about the quoted system HOL light, so I have not
verified Slind's claim.

Till

Elwood Wilkins wrote:
> Isabelle's internal logic is not constructive. The existential clause of the
> BHK-interpretation is violated so that a consquence of "all unicorns have
> horns" is that "some unicorn has a horn". The moral (biased towards
> theorists): software engineering considerations are not enough, a coherant
> philosophy of mathematics is also needed.
>
> Elwood
>
> ----- Original Message -----
> From: Till Mossakowski <till@Informatik.Uni-Bremen.DE>
> To: Categories <categories@mta.ca>
> Sent: Tuesday, May 27, 2003 11:44 AM
> Subject: categories: Topos logic arises naturally
>
>
>
>>You see: even with just aesthetic and software engineering
>>considerations you are eventually lead to topos logic...
>>
>>--
>>Till Mossakowski               Phone +49-421-218-4683
>>Dept. of Computer Science      Fax +49-421-218-3054
>>University of Bremen           till@tzi.de
>>P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
>>
>>Message-Id: <200305270616.h4R6G3w8008134@plxc2089.pdx.intel.com>
>>To: Randy Pollack <rap@inf.ed.ac.uk>
>>cc: John Harrison <johnh@ichips.intel.com>, isabelle-users@cl.cam.ac.uk
>>Subject: Re: HOL without description operators
>>Date: Mon, 26 May 2003 23:16:03 -0700
>>From: John R Harrison <johnh@ichips.intel.com>
>>Sender: Larry Paulson <Larry.Paulson@cl.cam.ac.uk>
>>
>>Hi Randy,
>>
>>| Perhaps more usefully, how do you suggest I do this task of developing
>
> HOL
>
>>| without description operators.
>>
>>You might find it interesting to look at HOL Light. This gives a
>>different axiomatization of the HOL logic, developed precisely because I
>>was dissatisfied with the one in the original HOL system, on which I
>>believe the Isabelle/HOL logic is based.
>>
>>Although I do eventually introduce the description operator, quite a lot
>>of the basic logic --- including the automation of inductive definitions
>>--- is developed without it (and indeed without excluded middle or
>>extensionality). You may find it a more congenial starting-point.
>>
>>As Konrad Slind later pointed out, what I settled on is remarkably close
>>to the internal logic of a topos, as presented for example in Lambek and
>>Scott's book. This was a surprise to me since at that time I knew next to
>>nothing about toposes and was motivated by a mixture of aesthetic and
>>software engineering considerations.
>>
>>Cheers,
>>
>>John.
>>
>>
>>
>>


-- 
Till Mossakowski               Phone +49-421-218-4683
Dept. of Computer Science      Fax +49-421-218-3054
University of Bremen           till@tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till