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

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.


lemma "ALL x. EX y. P x y ==> EX f. ALL x. P x (f x)" by metis



On 01/26/2016 09:16 PM, dimitri at wrote:
> Hello all,
> since this is my first post in this mailing list, I will shortly introduce
> myself. My name is Ioanna Matilde Dimitriou, and I work with the
> mathematical logic group of Bonn, on formalising ZF/NBG-Set Theory in
> Isabelle/HOL, in a "natural" style, i.e., as in a standard textbook.
> We do this to understand the interplay between Isabelle's, ZF's, and NBG's
> logics, to be able to use Sledgehammer (which to our knowledge is only
> written for HOL), and to explore the controlled natural language parsing
> possibilities in such a setting. For the first goal we chose to revisit
> Lawrence Paulson's "/ZF/Constructible/AC_in_L.thy", which is a large and
> challenging metamathematical formal proof, and which states that the Axiom
> of Choice (AC) is true in L, the universe of constructible sets.
> We quickly realised that AC holds in Isabelle/HOL, in fact it is a lemma
> in "A Proof Assistant for Higher Order Logic" by Nikpow, Paulson, and
> Wenzel (page 87 of the 2015 version).
> Is there any way to completely "turn off" AC in Isabelle/HOL? If not,
> could you please give me some pointers to the direction of writing a
> Sledgehammer for Isabelle/Pure, Isabelle/FOL, or Isabelle/ZF?
> Thank you in advance,
> Ioanna

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