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

Isabelle/HOL introduces the axiom of choice fairly late in the development (contrast with other HOL implementations, which include it as part of the basic axiomatic set up), but from that point onwards, it gets intertwined with everything. It would be better if you chose a development involving AC, something to do with cardinals perhaps, or simply some of the more obscure consequences of AC.

Larry Paulson

> On 26 Jan 2016, at 20:16, 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.