[1] Resolutely give each partial function a convenient value on points
outside its domain. For example, set:
|- inverse(0) = 0
This has the advantage that you can state many theorems more elegantly:
|- inverse(inverse(x)) = x
|- 0 < x <=> 0 < inverse(x)
|- inverse(-x) = -inverse(x)
|- inverse(x * y) = inverse(x) * inverse(y)
But it also gives you strange "accidental" theorems like
|- inverse(0) = 0
itself.
[2] Give each partial function some arbitrary value outside its domain. This
gives fewer convenient theorems, but also fewer accidental ones.
Nevertheless you still get some, e.g. assuming we define
|- x / y = x * inverse(y)
then we have
|- 0 / 0 = 0 * something = 0
[3] Encode the domain of the partial function in its type and make its
application to arguments outside that domain a type error. This works well
in situations where definedness is implicit, like differential equations
where
|- d f(x) / dx = H[f,x]
includes (I think) an implicit assertion that f is differentiable iff
H[f,x] is defined. On the other hand in complicated situations in
analysis, one could imagine the types becoming staggeringly complicated,
and this approach disallows routine manipulations like:
|- inverse(-x) = -inverse(x)
|- inverse(x * y) = inverse(x) * inverse(y)
without incurring additional typechecking obligations (which might be
nontrivial if x is complicated).
[4] Have a true logic of partial terms. This is the most flexible, since one
can define multiple notions of equality; e.g. "both sides are defined and
equal" or "if one side is defined so is the other and they are equal".
The downside is that the logic becomes more complicated. I don't know how
troublesome this is in practice. Anyway, I think there's a strong argument
that this is how mathematicians normally think informally.
As far as I know, HOL takes approaches [1] and [2] according to the whim of the
user, Nuprl and PVS normally take approach [3], while IMPS takes approach [4].
Old LCF has (used to have?) something analogous to approach [4], and Lambda did
too, though I think it was abandoned in the face of user pressure for a simpler
logic. I'm not sure about other systems. For generic provers like Isabelle, I
suppose you have a free choice.
There's a good discussion of these issues in Farmer's paper "A Partial
Functions Version of Church's Simple Theory of Types" (JSL vol. 55, 1990; pp.
1269-1291). There's also an interesting-looking paper by Feferman on this topic
which I've just received a copy of (it's at home now so I can't give a
reference).
John.