From lusk Sat Jun 18 11:45:26 1994 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id LAA13970 for ; Sat, 18 Jun 1994 11:44:39 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 18 Jun 1994 17:44:23 +0100 To: qed@mcs.anl.gov Subject: Re: Definite description and choice In-reply-to: Your message of "Sat, 18 Jun 94 14:47:25 BST." <"3614*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS> Date: Sat, 18 Jun 94 17:44:17 +0100 From: John Harrison Message-ID: <"swan.cl.cam.:230310:940618164428"@cl.cam.ac.uk> Roger Jones writes: | 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? I think you are right: the above axiom won't yield choice. However it might prove too weak in a number of situations. In particular, if P does not contain any variables other than x, then the addition of the stronger axiom (there exists an x such that P x) => P (some x such that Px) does not, I believe, extend the logic nonconservatively, in that any use of the above axiom could be eliminated using exists-elimination in a rather tedious but completely straightforward way. Thus the stronger axiom might be the most natural way of embodying the fact that one can make finitely many arbitrary choices without AC. It is this stronger axiom which is liable to yield AC if additional free variables are allowed, since then one is effectively sanctioning a uniform choice scheme. Since this is the form of the actual HOL axiom (SELECT_AX), I was thinking in terms of that. There is an interesting discussion of this near the start of Potter's book "Sets: An Introduction" (such discussions seem to be few and far between in the logical literature). John.