我想证明伊莎贝尔中类似的引理
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 either!
不幸的是，这个假设确实not暗示THE x. P x“存在”，至少在某种意义上你不会感到满意。由于 HOL 是一个整体逻辑，因此逻辑中不存在“明确定义”的概念。
如果你写THE x. P x当没有唯一的时候x满足P, then THE x. P x is仍然是 HOL 中“存在”的一个值，但是你无法证明它有任何意义（就像undefined常数），当然不是一个P成立。对于SOME，这基本上与THE区别在于THE，必须有一个unique财产和财产的见证人SOME不要求唯一性。
展示某事的典型方法SOME x. P x是你首先证明证人存在（即∃x. P x），然后将其插入到类似的规则中someI_ex然后告诉你P (SOME x. P x)确实成立。
对于THE，除了你必须证明确实存在one证人——这就是∃!意味着（参见定理Ex1_def）。可以通过以下方式展示这种独特的存在：有规则ex_ex1I or ex1I。然后你可以将该事实插入theI' and the1_equality得到你想要的结果。
顺便说一句，常数SOME叫做Eps（如“希尔伯特 ε 算子”），其他的是The and Ex1。如果您输入例如term Eps，您可以按住 Ctrl 键单击Eps它会带你到它的定义（或者，如果是Eps and The而是他们的公理化）。
还有一个LEAST自然数的组合器非常类似于SOME有时非常有用（它被称为“最少”，引理是LeastI_ex and Least_le).
另一个旁注：仅仅因为你可以写下一个术语，它不一定是直观意义上“明确定义”的想法在伊莎贝尔中很常见：你可以除以零，你可以写下一个非的导数-可微函数、不可测集的度量、不可积函数的积分等。然后你会得到某种虚拟值（例如 0 表示除以零或完全荒谬的东西，例如THE x. False），但大多数讨论导数、积分等实际属性的定理确实明确要求该事物实际上是明确定义的。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
