[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy
brianh at cs.pdx.edu
Fri Sep 14 20:26:21 CEST 2007
On Friday 14 September 2007, Stefan Berghofer wrote:
> 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.
I agree completely. I am always disappointed to see proofs rely on AC when
they really don't need to.
I put some effort into making HOLCF independent of AC. Probably the most
common unnecessary use of AC was from using SOME where THE or LEAST would do.
Now the entire HOLCF library is built on top of just Finite_Set; Main (along
with Hilbert_Choice) is only imported at the very end.
I have also tried to make the development of the real and complex numbers
independent of AC, as far as possible. The development of nonstandard
analysis uses AC, but I'm OK with it, because in this case it is actually
Right now the only way to be sure that a theorem does not rely on the axiom of
choice is to make sure Hilbert_Choice.thy is not loaded, which currently
isn't that difficult to do (import PreList instead of Main, for example). But
if Hilbert_Choice is moved earlier in the development of HOL, then it will be
nearly impossible to tell which theorems have been contaminated with AC.
I think we need a way for people who care about independence from AC (like me)
to recognize theorems that rely on it. Maybe we could use the theorem tagging
mechanism (now used for proof oracles) to tag those theorems that use AC?
More information about the isabelle-dev