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