5. Resolutely give all partial functions the same value on points
outside of their domain. (This comes as a consequence of the basic
underlying language and definitions.)
Bernays uses the definite descriptor term $\iota_x (A)$ to represent
the object which is the unique $x$ such that $A$. In order that this
term be well-defined when there is no unique such object, Bernays says
that when there is no such object then $\iota_x (A)$ always represents
the empty set. He uses two axiom schemata to accomplish this.
So in Bernays' language we might say
1/x=\iota_y(x is real and x<>0 and x*y=1).
So we do get that 1/0={} (and 1/a-foo = {}) but we don't really care.
In Morse-Kelley's set theory they get around the use of the definite
descriptor by defining {x}={z: if x\in V, then z=x} where V is the
universe class.
In this system we might say (I'm skipping a lot of intermediate but
fairly standard definitions):
the-reciprocal-function = {<x, y>: x is real and x<>0 and x*y=1}
Thus, the-reciprocal-function(0) = V, the universe class. But then
again, we don't care.
This turns out to be very convenient for these authors in many ways.
My Ipr system implements an axiom schema for dealing with the definite
descriptor but also allows the user to construct his set theory so
that there is no need for it (as in MK's set theory). Thus the user
may select his favorite way of dealing with undefined terms, or not
worry about it (which is hopefully what most USERS of qed will do).
However, I would not expect that QED will be flexible enough to allow
the user to make such choices at so basic a level.
Benji
-- Benjamin Shults Email: bshults@math.utexas.edu Department of Mathematics Phone: (512) 471-7711 ext. 208 University of Texas at Austin WWW: http://www.ma.utexas.edu/users/bshults Austin, TX 78712 USA Office: RLM 10.142