From lusk Thu Jun 16 04:42:52 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 EAA07939 for ; Thu, 16 Jun 1994 04:40:06 -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; Thu, 16 Jun 1994 10:39:12 +0100 X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2)); Relayed; Thu, 16 Jun 1994 10:11:52 +0100 Date: Thu, 16 Jun 1994 10:11:52 +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 0000012600003611] Original-Encoded-Information-Types: undefined (0) X400-Content-Type: P2-1984 (2) Content-Identifier: 3611 Message-ID: <"3611*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS> To: qed@mcs.anl.gov Subject: Definite description and Choice in HOL I endorse John Harrisons comments about the generality of the simple lambda abstraction available in HOL. Our work on embedding Z into HOL is one example showing how much more elaborate variable binding constructs can be interpreted (not only in theory but in practice) in terms of simple lambda abstraction. I also endorse his view on the importance of a definite description operator. >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. The Cambridge HOL system has unnecessarily confused the relationship between definite description and choice. In Church's paper on "the theory of simple types" he uses a operator for definite description which does not prejudice the principle of choice. The principle of choice can then be introduced if required, as an axiom. In Cambridge HOL there is only a choice operator, and you really can't do much without the axiom of choice. A minor alteration to the primitive axioms and definitions would restore the separation. 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. Roger Jones International Computers Limited