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.
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.
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
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
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
My two cents worth: 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
-----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
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
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
participants (6)
-
Elwood Wilkins -
Lawrence Paulson -
Till Mossakowski -
Toby Bartels -
Todd Wilson -
Valeria.dePaiva＠parc.com