Re: topos logic arising nicely

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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