Re: Topos logic arises naturally

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