Date: Wed, 14 Aug 91 10:08:39 EDT
From: ian@com.oracorp.cambridge (Ian Sutherland)
Message-Id: <9108141408.AA20473@>
To: info-hol@edu.ucdavis.eecs.iris
Subject: Re: Choice

Rob Arthan writes:

>Re Josh Guttman's observations:
>
>>      Rather, my point is this: Given an ordinary structure, there's no canonical way
>>      to determine the values of epsilon-terms.  That is, it's arbitrarily chosen.
>>      The fact that you have a choice function or universal well-ordering in your
>>      background structure doesn't really make it any the less arbitrary, because of
>>      course there's nothing canonical about its being one choice function rather
>>      than any other.

But isn't this the same as saying there's nothing canonical about the
underlying sets in a first-order structure?  This underlying set is
bound only by the semantics of first-order logic and the axioms you
write about the interpretation of the language you're using.

Your original contention seemed to be that you couldn't even NAME the
choice function, and therefore couldn't write axioms about it the way
you could about other functions.  I THINK this is wrong.  I THINK you
can name the choice function as

        \x:(*->bool).(@y.(x y))

so you could write whatever axioms you like about it.  This is no
different, it seems to me, than writing axioms about "=" in ordinary
first-order logic.

I am not an HOL weenie, so could someone who is please tell me whether
the above really does name the "@" choice function for all intents and
purposes?  It's certainly legal HOL (according to our version of HOL
anyway).

>1) As Roger Jones points out, if you use (i) a fairly reasonable
>formulation of the axiom of choice in HOL, and (ii) the conservative
>extension mechanism called `new_specification' (which certainly is
>conservative), then you can define the choice operator.

As I noted above, it seems to me that you can name the choice operator
without any such machinery.