Thomas Streicher wrote:
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.
That may be the only way that one can *construct* such a type, hence the only way that one can *prove* that such a type exists, but how do you know that some unspecified type variable \sigma doesn't refer to an uninhabited type to begin with? The answer will depend on the interpretation, I suppose; some logics simply aren't applicable to some semantics.
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
Of course. Only with \exists x:\sigma. A(x) will (2) follow. -- Toby