From lusk Sat Jun 18 08:52:24 1994
Received: from relay1.pipex.net (relay1.pipex.net [158.43.128.4]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id IAA11689 for <qed@mcs.anl.gov>; Sat, 18 Jun 1994 08:50:53 -0500
From: R.B.Jones@win0109.wins.icl.co.uk
X400-Received: by mta relay1.pipex.net in /PRMD=pipex/ADMD=pipex/C=gb/; Relayed;
               Sat, 18 Jun 1994 14:50:47 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Sat, 18 Jun 1994 14:47:25 +0100
Date: Sat, 18 Jun 1994 14:47:25 +0100
X400-Originator: R.B.Jones@win0109.wins.icl.co.uk
X400-Recipients: qed@mcs.anl.gov
X400-MTS-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600003614]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 3614
Message-ID: <"3614*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: qed@mcs.anl.gov
Subject: Re: Definite description and choice







 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