[FOM] 618: Adventures in Formalization 4

[Larry Paulson]

> A term being defined is not a syntactic matter. However, we will want
> to have facilities for dealing with compound terms being obviously
> defined, just as mathematicians do. E.g., in an environment with the
> field operations, we have undefined terms. However, we know that if we
> avoid division, the terms are always defined. We need a way of dealing
> with this formally. I haven't quite decided how I want to deal with
> this.

This topic has been endlessly rehearsed by researchers into interactive theorem
proving. 20 years ago, John Harrison wrote a note on this topic which has even
been cited by others, but the original link no longer works. As a contribution
to the discussion, I shall post John's note subsequently. Another highly
relevant paper includes the following:

http://link.springer.com/chapter/10.1007%2FBFb0061839
Dana Scott. Identity and existence in intuitionistic logic.
In: Fourman et al., Applications of Sheaves.
Springer LNM Volume 753 (1977), 660-696.

William Farmer has written extensively on this topic, and his publications can be found here:
	http://imps.mcmaster.ca/wmfarmer/publications.html

Somebody's attitude to the idea of partial functions can be judged by their 
answers to the following questions:

Is 1/0 a ZF set?

Is 1/0 = 1/0 true?

Is the formula 1/x > 0 well defined, if we only know that x is a real number?

Is the formula x > 0 ==> 1/x > 0 well defined and true for all real x, including x=0?

And also the formula 1/x > 0 | x <= 0 ? 

Solutions include logics where you can write statements like Defined(1/x) | x=0.
Three-valued logics have also been proposed; in my opinion that approach is
complicated and unnecessary. And then we have the type theories, where partial
functions take an additional argument a proof p stating that the function is
being applied within its domain; a complication here is the question of whether
the result can depend upon p. But this approach is hugely popular anyway.

In simply-typed systems such as Isabelle/HOL and HOL Light, every term must
denote some value (of the expected type). And therefore 1/0 - 1/0 definitely
equals zero. Whether we choose to extend the domain of a partial function
explicitly depends on the circumstances. As a college student, I remember being
shocked at Donald Knuth's willingness to extend the domains of many operations
on the grounds that they made manipulations easier.

I wish I could claim the credit for being the first to postulate x/0 = 0, but I
have no proof of precedence. Certainly it is widely adopted now. The point is
that it makes many obvious manipulations, such as x(y/z) = (xy)/z,
unconditional.

Larry Paulson