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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and