问对伊莎贝尔句子的某一特定部分进行量化
EN

Stack Overflow用户

提问于 2021-04-11 00:45:23

回答 1查看 55关注 0票数 2

假设我在伊莎贝尔中写了一个引理"(∀a. P a ⟹ Q a) ⟹ R b“。∀a只会对P a进行量化。但是，如果我想对P a ⟹ Q a进行量化，在∀a (即"(∀a. (P a ⟹ Q a)) ⟹ R a")后面加上括号将导致伊莎贝尔的解析失败。

我怎样才能对句子的特定部分进行适当的量化？

注:我知道在伊莎贝尔中，引理中的自由变量是隐式通用的。这个问题主要是针对内部语句的，在这些语句中，量词不应该涵盖整个句子。

回答已采纳

发布于 2021-04-11 02:15:03

我认为，解析失败是由于伊莎贝尔/霍尔有两种不同类型的蕴涵运算符，即Pure.imp (⟹)和HOL.implies (⟶)。前者是伊莎贝尔metalogic的一部分，后者是HOL逻辑的一部分。您可以找到更多关于为什么存在这种区别以及何时在这些邮件列表中使用这些信息的更多信息：

⟹运算符的优先级很低，低于∀，因此不能像您预期的那样解析∀a. (P a ⟹ Q a)。您可以使用⟶操作符来修复您的引理中的解析失败，后者的优先级高于∀。另一种选择是将∀改为元量词⋀，使您的句子更符合伊莎贝尔的框架。

运算符优先级表是可用的，但我不能保证它是最新的。您可以使用Isabelle中的print_syntax命令进行更可靠的最新排序。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/67040505

复制

相似问题

问对伊莎贝尔句子的某一特定部分进行量化EN