我在Isabelle/HOL标准库的源代码中看到THE x. A的结构。这个结构意味着什么？它似乎与SOME x. A相似.
THE是一个描述运算符，类似于SOME，但公理化较弱。THE x. P x表示满足谓词P的唯一值，前提是存在此类唯一值。否则，THE x. P x未指定。它也被称为罗素描述运算符。所以如果你使用THE，那么每当你想证明任何关于THE x. P x的非平凡的事情时，你必须证明正好有一个值满足P。
对于SOME，可能有几个满足P的值; 然后SOME x. P x表示其中之一。如果没有，则SOME x. P x也是未指定的。它被称为希尔伯特选择运算符，本质上为您提供了选择公理。要证明SOME x. P x的一些非平凡的东西，你必须证明有一些价值令人满意P。
一般来说，只要您可以使用THE，它就比SOME更可取，因为它依赖于较弱的公理并向读者指示唯一性。