Re: topos logic arising nicely

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

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