[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

[Stefan Berghofer]

Lawrence Paulson wrote:
> We previously put some effort into making  
> virtually all of HOL independent of the axiom of choice, so this  
> would be a reversal. [...] Can anybody comment?

For those members of the list who have not followed the discussion
about this issue a few years ago, let me cite what Larry wrote about it:

   I think it would be quite easy to do, and sensible (ZF has always been that way).

   [...]

   If the necessary effort is reasonable, it would be nice to remove AC from the
   core.  It has a corrupting influence.  For example, somebody generalized Least
   to LeastM, which at first sight is a natural generalization, but LeastM
   requires AC while Least does not.

In my opinion, a theory that does not depend on any unnecessarily strong axioms
also seems to be more appealing from a foundational point of view.

Greetings,
Stefan


-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe