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

Larry Paulson wrote:

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

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?

- Gergely

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