Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA18941 for qed-out; Tue, 23 May 1995 06:25:53 -0500
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP
id GAA18936 for ; Tue, 23 May 1995 06:25:27 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP-6.5) to cl; Tue, 23 May 1995 12:24:29 +0100
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
In-reply-to: Your message of "Mon, 22 May 1995 16:32:16 CDT." <199505222132.QAA14234@pythagoras.ma.utexas.edu>
Date: Tue, 23 May 1995 12:24:16 +0100
From: John Harrison
Message-ID: <"swan.cl.cam.:158810:950523112446"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.077
You are right: in [2] I meant to allow various arbitrary values in different
situations. This makes the proposal [5] genuinely different. In HOL these
"arbitrary values" arise in two ways:
(1) Explicitly via the choice operator @ (an indefinite descriptor, so "@x.
P[x]" means "some x such that P[x]"). For example, one could define
inv = \x. @y. x * y = 1
(2) Via the principle of constant specification, which allows the
introduction of constants when a witness can be shown to exist.
For example:
|- !x. ~(x = 0) ==> ?y. x * y = 1
so
|- !x. ?y. ~(x = 0) ==> (x * y = 1)
Skolemizing
|- ?f. !x. ~(x = 0) ==> (x * f(x) = 1)
and introducing a constant "inv":
|- !x. ~(x = 0) ==> (x * inv(x) = 1)
Sometimes (1) results in more accidental theorems. We can't say much about
inv(0), but we do at least know that it's "@y. F" (F = falsum). This means that
any other constant of the same type defined in a similar way will also be equal
to "@y. F" when the body is false. Method (2) does not have this weakness. In
fact one could define two constants "inv" and "inv'" based on the same theorem,
without any relationship between inv(0) and inv'(0) being deducible. Some
HOL users considered this sufficiently important to justify the principle of
constant specification (in the old days, HOL only allowed definitions of the
direct form "c = ", or so I'm told). On the other hand, we are not
explicit about the value of "@y. F" in a model. In the standard HOL semantics,
we just assume a single choice function from the start. You can read this
semantics (due to Andy Pitts) in the HOL book from CUP, or in machine-readable
form in the standard HOL distribution.
John.