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



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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.