Re: topos logic arising nicely

I don't know Isabelle too well BUT in Higher Order Logic one may well assume inhabitedness of all types when these are built up from N (and 1) via x,-> and P(-). In higher order logic one cannot form subtypes in the logical sense and that's the only way how one can build types that aren't inhabited. Of course, even if type sigma is inhabited from (1) \forall x:\sigma. A(x)->B one must not conclude (2) \exists x:\sigma. A(x) /\ B BUT only (3) \exists x:\sigma. A(x) -> B BTW concluding (2) from (1) is false also classically. Thomas