我THE x. A在Isabelle/HOL标准库的源代码中看到了构造.这个结构表示什么？它似乎与之相似SOME x. A.
THE是一个描述运算符SOME,但具有较弱的公理化.THE x. P x表示满足谓词的唯一值,P前提是存在这样的唯一值.如果没有,THE x. P x则未指定.它也被称为Russell的描述运算符.因此,如果您使用THE,那么无论何时您想要证明任何非平凡的事情THE x. P x,您都必须证明只有一个值令人满意P.
有SOME,可能有几个值满足P; SOME x. P x然后表示其中之一.如果没有,那么SOME x. P x也是未指定的.它被称为希尔伯特的选择算子,基本上为您提供了选择的公理.为了证明一些非平凡的事情SOME x. P x,你必须表明有一些值得满足的P.
一般来说,无论何时使用它都比THE较好SOME,因为它依赖于较弱的公理并表明读者的独特性.