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 is
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 pr
On 5 Aug 2012, at 22:32, Cris Perdue wrote:
> In the end I'm quite curious to know: is there some philosophical or
> engineering reason not to introduce the law of the excluded middle separately
> from an axiom of choice in HOL logics?
There are good practical reasons for having AC wired in. I
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 assumpt
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 un