terru (Sep 23 2025 at 15:06): terru (Sep 23 2025 at 15:06):I've recently looked into how HOL is built up, and seem to have hit a roadblock in my understanding: Isabelle/HOL provides two description operators (THE and SOME, for definite and indefinite description). I had always assumed SOME (i.e. choice) was the more fundamental of the two — e.g. Mike Gordon introduces it as one of the axioms, and uses it to define ; the old logics.pdf that is (while deprecated) still part of the Isabelle distribution does the same.
The NEWS file seems to imply this used (?) to also be the definition in Isabelle/HOL, but that it was changed with Isabelle 2002. Current HOL.thy instead defines ∃x. P x ≡ ∀Q. (∀x. P x ⟶ Q) ⟶ Q, and uses (definite) description only to define if-then-else, and SOME is no longer in it at all (its axiomatisation still exists, but is only in the separate Hilbert_Choice.thy).
So my question: why this change? The NEWS file unfortunately does not give a reason; perhaps there's literature elsewhere that I missed, or someone here knows?
Mathias Fleury (Sep 23 2025 at 15:25):Using hg blame I found the commit:
changeset: 11451:8abfb4f7bd02
user: paulson
date: Wed Jul 25 13:13:01 2001 +0200
summary: partial restructuring to reduce dependence on Axiom of Choice
This gives at least a partial information on why
terru (Sep 23 2025 at 17:48):fair, then my rough guess wasn't too far off.
(I'd mentally discarded this as possible motivation since I felt that one could probably reconstruct indefinite choice using definite choice & the axiom for undefined, which remains in HOL.thy. But turns out one can't; the closest is that, if one has a concrete P and needs Eps P, one can do typedef P_helper :: {x. P x} and then use undefined :: P_helper in place of Eps P — but while this construction can be done for any P, it can't be done for a general ?P, and in either case undefined was only added with Isabelle 2007, so its presence has no bearing on any motivations of chances done in 2002)
Last updated: Oct 09 2025 at 01:37 UTC