*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer*From*: Ioanna Dimitriou <dimitri at math.uni-bonn.de>*Date*: Tue, 2 Feb 2016 15:27:17 +0100*In-reply-to*: <C32D3449D568C445AB18C60817FABFE10144E5188654@ingrid.foiskola.krf>*References*: <6bc8023d679624184fa937c615db0a9e.squirrel@webmail5.math.uni-bonn.de> <350141C1-74B7-48DC-8865-B87D49C77D1E@cam.ac.uk> <C32D3449D568C445AB18C60817FABFE10144E5188654@ingrid.foiskola.krf>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Icedove/38.5.0

Thank you all for your answers. > 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. > 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. I think that if we have a primitive type "Class" of classes with a subtype "Set" of sets, and some axioms for them, say NBG without choice, then we can still work in a theory that involves the axiom of choice without deducing that certain choice functions and Skolem functions (which exist in HOL) have type "Class". This is similar to constructing a "model" of (ZF+notAC ) while working in (ZF+AC), which is not problematic at all. So, unless I'm mistaken, I don't think that working with HOL is problematic in itself, though we now have to put some work in defining FOL-formulas with class parameters in order to get Class Separation in our theory NGB, and then somehow carefully "connect" these formulas to formulas in HOL. If we didn't have AC at all, then we could be more flexible with rules that deduce that certain metafunctions ("Set => bool") have representations of type Class. > Her research page tells me that her research goal is especially discovering how far one can get without the axiom of choice. > > Might it be that Isabelle/ZF is better for her aim? Though I personally enjoy working without AC, or between AC and notAC, the research goal for the project I mentioned in the last post is to formalise ZF(C) (or NBG(C)) in a way that appears natural to a working mathematician (like in a textbook). Paulson's proof of AC in L is particularly interesting because of the metamathematical arguments which are so commonplace in set theory. In the Bonn logic group we think that HOL is more suitable for this task, because of the shorter proof steps, the meta-arguments that become easier when one can talk about classes, because of the large HOL-libraries we can learn from, and because of Sledgehammer. Having said that, I would also like to compare the two logics (HOL vs ZF) with respect to formalising ZF(C) in a "natural" way. For this, I would really like to be able to use Sledgehammer. That's why I also asked for some pointers in the direction of writing a Sledgehammer for FOL. Perhaps this has been done already, or there is a detailed explanation of Sledgehammer somewhere? Otherwise, do I just have to understand the code in Sledgehammer.thy? Best wishes, Ioanna

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

**References**:**Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer***From:*Lawrence Paulson

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

- Previous by Date: [isabelle] Datatype: Sort constraint and nested datatypes
- Next by Date: Re: [isabelle] Isabelle2016-RC0: cvc4 crashing
- Previous by Thread: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- 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