Dear Hendrik,
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.
I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes).
I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove
hd [] = last []
(saying that the head of the empy list equals its last element)
thanks for the interesting information; you really pinpoint why subtypes are used in practice, namely for avoiding partial functions; if one wants to avoid subtypes and treat partial functions directly one might use the Fourman/Scott variant of the interpretation of topos logic; an alternative and actually the one common in mathematical practice is to introduce subtypes; however, to do this constructively one is forced to either treat partial functions as single-valued realtions OR to explicitly introduce proof objects as in Martin-Loef type theory; I am pretty certain that in systems like HA_\omega one cannot quantify over partial functions as these subsume prediacte types; but if one has Higher Order Logic already it seems more natural to treat partial functions as single valued relations; quantification over subtypes can then be reduced to pure Higher Order Logic via a straightforward translation (which, however, needs some care as one sees from HOL) Thomas