Date: Sat, 27 Jul 91 07:28:42 EDT
From: ian@com.oracorp.cambridge (Ian Sutherland)
Message-Id: <9107271128.AA19999@>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: More on the choice function

>I believe what Josh meant to say is that the value of
>
>       @x. P x
>
>is not determined by P because it depends on some "hidden"
>well-ordering that can't be referred to in the language.

Actually, if the value of the @ function was always picked out by a
well-ordering, you could at least refer to the restriction of this
well ordering to a given type by

        \x:T.\y:T.((@z.((z = x) \/ (z = y))) = x)

Forgetting about well-orderings, there's a choice function generated
in SOME way being used to pick the values of "@" expressions, and it's
nameable as

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

This doesn't change Josh's original point about the value of "@"
expressions not being determined by their contents, but you can talk
about the function being used to determine these values IN HOL, and
could even state axioms or hypotheses about it (although why you'd
want to I don't know).