伊莎贝尔/HOL : What does the THE construct denote?

Question

我看到了构造 THE x. A在 Isabelle/HOL 标准库的源代码中。这个构造表示什么？好像和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也未指定。它被称为希尔伯特选择算子，本质上为您提供了选择公理。证明一些关于 SOME x. P x 的重要事情，你必须证明有一些值满足 P .

一般来说，THE优于 SOME只要你可以使用它，因为它依赖于一个较弱的公理并向读者表明唯一性。