Re: Topos logic arises naturally

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