假设我在 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
关于isabelle - 量化伊莎贝尔句子的特定部分，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/67040505/