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 <qed@mcs.anl.gov>; 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