Hi Cris,
I'm not sure about the original motivation for using the axiom of choice in
the HOL logic, and would be interested to know. But given that the HOL
logic has this, and given that excluded middle is provable from this, we may
as well not have excluded middle as an axiom. The philosophy
Hi Cris,
To chime in on this:
I don't have any problems with a system that doesn't allow
you to disable the axiom of choice. In other words:
hardwire choice all you like as far as I'm concerned.
Without AC you get weirdnesses as that a union of countably
many countable sets doesn't need to be
On Sun, 5 Aug 2012, Konrad Slind wrote:
My opinion is that Peter Homeier's HOL-Omega is the right setting to
properly implement something locale-like, since it provides
quantification over type variables in the logic. In plain old HOL the
implementation of locales as essentially
Freek, Mark, Bill,
Thanks very much for the stimulating and I think helpful responses,
including Mark's historical sketch. I'm glad to learn that inclusion of an
axiom of choice is considered unsurprising, perhaps leading to less weird
consequences than if it is left out. Freek's example of the
