Re: Topos logic arises naturally

Re: Topos logic arises naturally

[Lawrence Paulson]

> -----Original Message-----
> From: Elwood Wilkins [mailto:elwood@essex.ac.uk]
> Sent: Friday, May 30, 2003 4:35 AM
> To: Categories
> Subject: categories: Re: Topos logic arises naturally
>
> 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.

Isabelle's internal logic comes from Lambek and Scott.  It is an
instance of Example 1.1 on page 132, where all types are assumed to be
non-empty.  However, even their full system is unacceptable to many
constructivists because it is impredicative.  Constructive theories,
like a certain commuting diagrams package, have a surprising tendency
to "time out".

Larry Paulson

Re: Topos logic arises naturally

[Todd Wilson]

On Tue, 3 Jun 2003, Lawrence Paulson wrote:
> Isabelle's internal logic comes from Lambek and Scott.  It is an
> instance of Example 1.1 on page 132, where all types are assumed to be
> non-empty.

But this is the heart of the matter.  There is a certain precise sense
in which what happens in a topos between the empty set and a singleton
set governs the behavior of the rest of the topos.  Instead, why not
factor out the topos logic and add whatever nonemptiness assumptions
that are perceived necessary from a practical standpoint as an
additional theory?  This factoring shouldn't affect those that rely on
the non-emptiness assumptions, but it would make a big difference to
those who want to work in the topos logic.

-- 
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh

Re: Topos logic arises naturally

[Lawrence Paulson]

On Tuesday, June 3, 2003, at 05:04  pm, Todd Wilson wrote:

> But this is the heart of the matter.  There is a certain precise sense
> in which what happens in a topos between the empty set and a singleton
> set governs the behavior of the rest of the topos.

The point of my message is merely to counter suggestions on this
mailing list that Isabelle's underlying logic was cooked up in some
ad-hoc way and is incoherent.  The basic logic comes from a standard
source.  Extensions (type classes especially) were thought through very
carefully.  We have never claimed allegiance to any school of
constructivity.

Larry Paulson

Re: Topos logic arises naturally

[Valeria.dePaiva]

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

Re: Topos logic arises naturally

[Toby Bartels]

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.

Is this a failure of constructivism as such, or just a bug?
No doubt that a coherent philosophy of mathematics
helps to avoid such mistakes, but would anybody ever claim
that it's *not* a mistake?


-- Toby

Re: Topos logic arises naturally

[Till Mossakowski]

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

Re: Topos logic arises naturally

[Elwood Wilkins]

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.
>
>
>
>

Topos logic arises naturally

[Till Mossakowski]

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.