Toby Bartels wrote
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.
Certainly, if you allow type variables then the problem crops up. I don't really see the point why one would like to have type variables unless one can perform constructions with types in a uniform way, e.g. when considering logic on top of system F, system F\omega or even on top of a dependent type theory (possibly with an impredicative universe). I guess that in case of HOL type variables were rather motivated by the analogy to functional languages with their "shallow" polymorphism. The point of my mail rather was that so-called topos logic admits subtype formation, i.e. that {x:A|phi(x)} is a type whenever \phi is a predicate on A. This, of course, allows one to introduce types with undecided inhabitedness. See W.Phoa's Edinburgh lecture notes for a calculus extending HOL with subtypes (or Bart Jacob's book). But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. Thomas