Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer



Hi Chris,

> Correct me if I am wrong, but my impression is that sledgehammer (via
> metis) has (at least a variant of) the "Axiom of Choice" built-in. And I
> think the same holds true for any tool that employs Skolemization.
> 
> E.g.
> 
> lemma "ALL x. EX y. P x y ==> EX f. ALL x. P x (f x)" by metis

This is true, but only if you have loaded "Hilbert_Choice". Before that, "metis" will fail to prove the above, because it has to rely on a weaker skolemizer. And Sledgehammer is simply not available.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.