unique - 在 Isabelle 中证明关于 THE 的直观陈述

Question

我想在 Isabelle 中证明这样的引理

lemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"

我想这个假设意味着 THE x. P x存在并且是明确定义的。所以这个引理也应该是真的

lemma assumes "y = (THE x. P x)" shows "∃! x. P x"

我不确定如何证明这一点，因为当我在 Isabelle 的查询框中键入“name: the”时，我已经查看了所有出现的定理，但它们似乎没有用。我找不到 THE 的定义要么，我不知道如何定义它，尽管我对它的含义有一个直观的了解。我试过这样的事情虽然我确定这是错误的

"(∃!x. P x) ⟹ THE x. P x = (SOME x. P x)"

甚至可能没用，因为我不知道如何定义 SOME任何一个!

Answer 1

不幸的是，该假设并不意味着 THE x. P x “存在”，至少在某种意义上不是您会感到满意的。由于 HOL 是一个整体逻辑，因此逻辑中没有“明确定义”的概念。

如果你写 THE x. P x当没有唯一x满足P ，然后 THE x. P x仍然是 HOL 中“存在”的值，但是您无法证明其有任何意义(很像 undefined 常量)，当然也不是 P 的值。持有。 SOME也是如此, 与 THE 基本相同与 THE 的区别，必须有属性(property)和SOME的唯一见证人。不需要唯一性。

展示有关 SOME x. P x 的典型方法是您首先证明存在见证人(即 ∃x. P x )，然后将其插入规则中，例如 someI_ex然后告诉你 P (SOME x. P x)确实成立。
THE也是一样的，除了在那里你必须证明只有一个见证人——这就是 ∃!意味着(参见定理 Ex1_def)。可以显示这种独特的存在，例如与规则 ex_ex1I或 ex1I .然后你可以将该事实插入 theI'和 the1_equality以获得您想要的结果。

顺便说一下，SOME 的常数被称为 Eps (如“希尔伯特的 ε 算子”)和其他是 The和 Ex1 .如果你输入例如term Eps ，您可以按住 ctrl 键单击 Eps它带你到它的定义(或者，在 Eps 和 The 的情况下，而不是它们的公理化)。

还有一个LEAST与 SOME 非常相似的自然数组合子并且有时非常有用(它被称为“最少”，引理是 LeastI_ex 和 Least_le )。

另一个旁注:这种想法，仅仅因为你可以写下一个术语，它不一定在直觉意义上是“明确定义的”在 Isabelle 中很常见:你可以除以零，你可以写下非- 可微函数、不可测集的度量、不可积函数的积分等。然后你会得到某种虚拟值(例如 0 表示除以零或完全荒谬的东西，如 THE x. False )，但大多数许多讨论导数、积分等实际性质的定理确实明确要求事物实际上是明确定义的。