伊莎贝尔/霍尔:这个结构意味着什么？

Question

我在Isabelle/HOL标准库的源代码中看到了构造THE x. A。这个结构意味着什么？它似乎与SOME x. A类似。

Answer 1

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也未指定。它被称为Hilbert的选择算子，本质上给出了选择的公理。要证明关于SOME x. P x的一些非平凡的东西，您必须证明有一些满足P的值。

通常，无论何时您可以使用THE，它都比SOME更可取，因为它依赖于一个较弱的公理，并向读者表明其唯一性。