*To*: dimitri at math.uni-bonn.de*Subject*: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 2 Feb 2016 10:55:23 +0000*Cc*: Cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <6bc8023d679624184fa937c615db0a9e.squirrel@webmail5.math.uni-bonn.de>*References*: <6bc8023d679624184fa937c615db0a9e.squirrel@webmail5.math.uni-bonn.de>

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 math.uni-bonn.de 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 > >

**Follow-Ups**:**Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer***From:*Buday Gergely

- Previous by Date: Re: [isabelle] RC1 - Greyout
- Next by Date: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- Previous by Thread: Re: [isabelle] RC1 - Greyout
- Next by Thread: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- Cl-isabelle-users February 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list