Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id PAA11772 for qed-out; Mon, 22 May 1995 15:24:57 -0500
Received: from pythagoras.ma.utexas.edu (pythagoras.ma.utexas.edu [128.83.133.41]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id PAA11766 for ; Mon, 22 May 1995 15:24:49 -0500
Received: (from bshults@localhost) by pythagoras.ma.utexas.edu (8.6.10/8.6.10) id PAA14051; Mon, 22 May 1995 15:23:53 -0500
Date: Mon, 22 May 1995 15:23:53 -0500
From: Benjamin Price Shults
Message-Id: <199505222023.PAA14051@pythagoras.ma.utexas.edu>
To: kaufmann@CLI.COM
CC: holmes@catseye.idbsu.edu, moore@CLI.COM, qed@mcs.anl.gov
In-reply-to: <9505221831.AA04663@thunder.cli.com> (kaufmann@CLI.COM)
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.064
I think this problem is addressed in a slightly different way (from
the four suggestions given by Harrison) in the popular classical
axiomatizations of set theory (Goedel-Bernays, Morse-Kelley). Of
course, this is in the context of a first-order theory with some
additional axiom schemata, which may be far from what most of you are
thinking of. But perhaps it's worthy of inclusion in the discussion.
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 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