Re: Definite description and choice

R.B.Jones@win0109.wins.icl.co.uk
Sat, 18 Jun 1994 14:47:25 +0100

Since no-one else has done it I shall have to criticise my contribution on the
above topic myself.

The passage:

>In Cambridge HOL to really avoid the axiom of choice you would also have to
>remove one of the primitive definitional principles, which effectively
>presumes it. This principle, which permits function definitions of the form:
>
> f x = .. x ..
>
>might be considered technically redundant (and in fact is not primitive in
>ProofPower). Most definitions of this form can be reduced to the form:
>
> f = \x. .. x ..
>
>without using the axiom of choice, but not all of them. However even where
>the reduction can be done without using the axoim of choice it is easier if
>one can use choice.

is completely incorrect. There are circumstances in which the axiom of choice
simplifies the existence proofs necessary for using the "new_specification"
facility, but I'm not aware of any relevant problems in the strictly
definitional extensions in HOL.

I'm still puzzled by John Harrison's original claim (echoed by others) that
definite description has the force of the axiom of choice if one is reckless
with free variables.

>I would say that the most important feature neglected in many presentations
>of logic is some sort of description operator: "the x such that ..." or
>"some x such that ...". I believe Bourbaki postulate such a feature in their
>notional logical foundation. Without it, there seems to be a real reliance
>on nontrivial metatheory (introducing Skolem functions or getting rid of
>existential quantifiers in an elaborate way). If you don't like the Axiom of
>Choice you need to be careful about allowing free variables in the "..."s
>in the introduction rule.

I agree that "some x such that .." will be problematic, because that sounds
like a choice operator rather than definite description. I don't see how the
axiom of choice is implied by the use of "the x such that ..." provided that
the axiom which is associated with the construct is the usual one:

(there exists a unique x such that P x) => P (the x such that Px)

Can John (or anyone else) explain more fully how this can ever entail the axiom

of choice and/or give an example of such a use?

Roger Jones
International Computers Limited