Isabelle/HOL: What does the THE construct denote?

问题:

I saw the construct THE x. A in the source code of the Isabelle/HOL standard library. What does this construct denote? It seems to be similar to SOME x. A.

回答1:

THE is a description operator like SOME, but with a weaker axiomatization. THE x. P x denotes the unique value that satisfies the predicate P provided that such a unique value exists. If not, THE x. P x is unspecified. It is also known as Russell's description operator. So if you use THE, then whenever you want to prove anything non-trivial about THE x. P x, you must prove that there is exactly one value satisfying P.

With SOME, there may be several values that satisfy P; SOME x. P x then denotes one of them. If there are none, then SOME x. P x is also unspecified. It is known as Hilbert's choice operator and essentially gives you the axiom of choice. To prove something non-trivial about SOME x. P x, you must show that there is some value satisfying P.

In general, THE is preferable over SOME whenever you can use it, because it relies on a weaker axiom and indicates the uniqueness to the reader.