Re: topos logic arising nicely

On Tue, 3 Jun 2003, Thomas Streicher wrote:

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.

"The neglect of sum types is the root of all evil." Paul