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

[Makarius]

On Fri, 14 Sep 2007, Stefan Berghofer wrote:

> 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.

I agree with this.


	Makarius