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

Stefan Berghofer berghofe at in.tum.de
Fri Sep 14 16:43:51 CEST 2007

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.


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

More information about the isabelle-dev mailing list