[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy
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