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

[John Matthews]

I'm a little surprised to hear Sledgehammer needs a general axiom of  
choice. After all, first order logic doesn't. Could the uses of  
Hilbert's choice in Sledgehammer be replaced with dynamic calls to  
ax_specification? That gives you a lot of the power of Hilbert  
choice, but is a conservative extension.

I guess it would be nice to have a way to remove the constants from  
the theory afterward, since they're only being used for  
skolemization. Even better would be a local version of  
ax_specification, because then you could just throw away the  
enclosing locale after exporting the theorem generated by metis.

-john

On Sep 14, 2007, at 3:32 AM, Lawrence Paulson wrote:

> Florian has suggested making sledgehammer available earlier in the
> construction of Main, before PreList at least. This could be useful
> to developers. However, it requires Hilbert_Choice, which must also
> be introduced earlier. We previously put some effort into making
> virtually all of HOL independent of the axiom of choice, so this
> would be a reversal. However, I don't know of anybody who has
> actually taken advantage of the AC-free part; in particular, I don't
> think that the use of nominal methods requires this any more. Can
> anybody comment?
>
> Larry
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/ 
> isabelle-dev