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



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





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