Re: Topos logic arises naturally

[Valeria.dePaiva@parc.com]

My two cents worth:
>The moral (biased towards
> theorists): software engineering considerations are not enough, a coherent
> philosophy of mathematics is also needed.
John Harrison (the creator of HOL Light) has a very coherent, but
pragmatic philosophy of mathematics. Let us see how much can we do with
constructive logic, without getting rid of the classical principles: Add
them at the end, so that if someone really needs it, they can use it. This
is a philosophy quite widespread in Cambridge, with Peter Johnstone's
books being the paradigmatic example. If classical reasoning is needed,
it's used, but flagged.

I also agree with Till that it's a cute example.

Best,
Valeria


-----Original Message-----
From: Till Mossakowski [mailto:till@Informatik.Uni-Bremen.DE]
Sent: Friday, May 30, 2003 7:37 AM
To: Categories
Subject: categories: Re: Topos logic arises naturally


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