*To*: Ioanna Dimitriou <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 15:11:13 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <56B0BCC5.1090306@math.uni-bonn.de>*References*: <6bc8023d679624184fa937c615db0a9e.squirrel@webmail5.math.uni-bonn.de> <350141C1-74B7-48DC-8865-B87D49C77D1E@cam.ac.uk> <C32D3449D568C445AB18C60817FABFE10144E5188654@ingrid.foiskola.krf> <56B0BCC5.1090306@math.uni-bonn.de>

I'm suspicious of this suggestion. Something tells me that AC (which is available for all types) will contaminate the new types that you introduce. This raises the question however of solving your problem using type classes, whether we could allow types that do not assume AC to coexist beside the others. Larry Paulson > On 2 Feb 2016, at 14:27, Ioanna Dimitriou <dimitri at math.uni-bonn.de> wrote: > > 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.

**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

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

- Previous by Date: Re: [isabelle] Isabelle2016-RC0: cvc4 crashing
- Next by Date: Re: [isabelle] Datatype: Sort constraint and nested datatypes
- 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