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

[Brian Huffman]

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

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?

- Brian