[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy
makarius at sketis.net
Fri Sep 14 19:03:26 CEST 2007
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.
More information about the isabelle-dev