如何解决在 Isabelle 中量化句子的特定部分
假设我在 Isabelle 中写了一个引理“(∀a. P a ⟹ Q a) ⟹ R b”。 ∀a 只会量化 P a。但是，如果我想对 P a ⟹ Q a 进行量化，将括号放在 ∀a 之后（即“(∀a. (P a ⟹ Q a)) ⟹ R a”）将导致 Isabelle 的解析失败。
如何正确量化句子的特定部分？
注意：我知道引理中的自由变量在 Isabelle 中是隐式通用的。这道题主要针对内部陈述，其中量词不应覆盖整个句子。
解决方法
我认为解析失败的原因是 Isabelle/HOL 有两种不同类型的蕴涵运算符，Pure.imp (⟹) 和 HOL.implies (⟶)。前者是 Isabelle 元逻辑的一部分，而后者是 HOL 逻辑的一部分。您可以在这些邮件列表帖子中找到有关为何存在这种区别以及何时使用每种区别的更多信息：
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-December/msg00031.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00019.html
⟹ 运算符的优先级非常低，低于 ∀，因此无法按预期解析 ∀a. (P a ⟹ Q a)。您可以使用优先级高于 ⟶ 的 ∀ 运算符来修复引理中的解析失败。另一种选择是将 ∀ 更改为元量词 ⋀，使您的句子更符合 Isabelle 的框架。
可以使用运算符优先级表，但我不能保证它是最新的。您可以在 Isabelle 中使用 print_syntax 命令以获得更可靠的最新排序。
表：https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/pdfi7tZP06fqA.pdf
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
