From lusk Thu Jun 16 05:39:14 1994
Received: from diamond.idbsu.edu (diamond.idbsu.edu [132.178.200.127]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id FAA09025; Thu, 16 Jun 1994 05:39:04 -0500
Message-Id: <199406161039.FAA09025@antares.mcs.anl.gov>
Received: by diamond.idbsu.edu
	(1.37.109.4/16.2) id AA02453; Thu, 16 Jun 94 04:41:11 -0600
Date: Thu, 16 Jun 94 04:41:11 -0600
From: Randall Holmes <holmes@diamond.idbsu.edu>
To: lusk@mcs.anl.gov, qed@mcs.anl.gov
Subject: Re:  Definite description and Choice in HOL

One can have the Hilbert epsilon operator (the device which seems to
force choice on HOL in conjunction with abstraction) without the axiom
of choice being mandated, if one has the general capability of
specifying that certain constructions are opaque to abstraction;
variables in such constructions cannot be bound in lambda-terms.  I
have implemented such a general facility in my baby prover.

The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@math.idbsu.edu