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



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.