Re: Definite description and Choice in HOL
Randall Holmes (holmes@diamond.idbsu.edu)
Thu, 16 Jun 94 04:41:11 -0600
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