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



Hey all.

It's nice to be able to avoid the Hilbert_Choice theory, and use only
the definite description operator (The/THE) as opposed to the strong
Hilbert choice operator (Eps/SOME).

I played around with this about a year ago, and discovered that this
doesn't buy you much in modern Isabelle. The lifting and transfer
packages seem to make extensive use of Eps, and pretty much everything
that isn't a natural seems to now use lifting/transfer in the definition
of some primitive functions. Even proofs about naturals seem to depend
on the axiom about Eps because the simprocs about naturals sometimes
coerce to integers, and int/of_nat is defined by lifting/transfer.

At least, that's the impression I got. I might have misunderstood what
was going on.

Cheers,
    Thomas.

On 03/02/16 01:01, Jasmin Blanchette wrote:
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




________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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