Message-Id: <9107291038.AA14937@erbert.win.icl.co.uk>
From: Rob Arthan <rda@uk.co.icl.win>
Date: Mon, 29 Jul 91 10:38:27 GMT
To: info-hol@edu.ucdavis.eecs.iris
Original-To: info-hol@clover.ucdavis.edu
Subject: Choice


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.

I'm afraid I'm not really sure what you are getting at here. Are the following
comments relevant:

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. The fact that
there is nothing canonical about the object which must be used to
interpret the operator in a structure is not a special property of
choice, it's a fact of life for the loosely specified constants you can
introduce with `new_specification'.

2) It is also true that most, if not all, of the other operators which
occur in the accepted axioms for HOL are loosely specified (and so not
canonical). For example, the type of individuals is axiomatised as a
type admitting a self-mapping which is one-one but not onto. There is
nothing canonical about the type or the mapping.

3) Loosely specified constants are extremely useful. In our ICL
implementation of a proof development system for HOL, we use
`new_specification' a lot in defining the basic mathematical theories.
For example, we introduce the type of natural numbers in such a way
that the definition of the type is, essentially, the statement that
there exist a zero element and a successor function on the type which
satisfy the Peano postulates. `new_specification' can then be used to
define zero and successor with a defining theorem which is simply the
statement of the Peano postulates. This leads to a development of
arithmetic which is a lot more elegant than one which works directly
with representatives for zero and successor in the type of individuals,
since the theory as seen by a user contains no (or almost no)
extraneous information about how the operators were constructed.

4) Item 3 is an instance of Roger's advice that the best thing to
do with choice in HOL is not to use it, because most computing
applications just don't need such a strong axiom. However, of course,
one does need it for proving results like Zorn's lemma which are
potentially useful hammers for cracking certain walnuts.

Regards,


Rob Arthan. (rda@win.icl.co.uk)                 ICL Secure Systems,
                                                Eskdale Rd.
                                                Winnersh,
                                                Wokingham
                                                Berks. RG11 5TT