Isabelle/HOL 中的对象级含义

Question

我看到 Isabelle/HOL 中的许多定理更喜欢元级蕴涵：

==>

而不是

-->

对象逻辑层次，即高阶逻辑蕴涵。

Isabelle wiki说粗略地说，应该使用元级蕴涵来将规则语句中的假设与结论分开。

除此之外，关于对象和元级蕴涵的使用，我还应该知道些什么？我看到后者主要被使用。我应该何时以及为何使用 HOL 蕴涵？

Answer 1

我认为简短的回答是：尽可能使用 ==>，因为它比 --> 更容易使用。

话虽如此，您不应该在您编写的代码中经常看到 ==>。

1. 写引理时，通常使用 assumes 和 shows 语法会更好。
2. 对于 have 的中间步骤，有 if 的语法： have "B" if "A" 而不是 have "B ==> A"
3. 元蕴涵只能在顶层使用，因此如果您将谓词作为函数的参数，则不能在该谓词中使用 ==>。