我在 Isabelle/HOL 标准库的源代码中看到了这个结构 THE x. A。这个结构代表什么意思？它似乎类似于 SOME x. A。
Isabelle/HOL: THE构造表示什么？
5
- Wolfgang Jeltsch
1个回答
6
THE是一个类似于SOME的描述运算符，但其公理化程度较弱。如果存在唯一满足谓词P的值，则THE x. P x表示该唯一值。否则，THE x. P x是未指定的。它也被称为Russell的描述运算符。因此，如果您使用THE，那么每当您想证明任何关于THE x. P x的非平凡内容时，您必须证明恰好有一个值满足P。对于
SOME，可能存在多个满足P的值；然后，SOME x. P x表示其中之一。如果没有这样的值，则SOME x. P x也是未指定的。它被称为Hilbert的选择运算符，基本上提供了选择公理。要证明关于SOME x. P x的任何非平凡内容，您必须证明存在某个值满足P。通常情况下，只要可以使用
THE，就应首选它，因为它依赖于更弱的公理，并向读者指示唯一性。- Andreas Lochbihler
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接