isabelle - 量化 Isabelle 中句子的特定部分

Question

(∀a. P a ⟹ Q a) ⟹ R b假设我在 Isabelle 中写了一个引理“ ”。∀a只会量化过来P a。但是，如果我想量化，在（即“ ”）P a ⟹ Q a之后加上括号将导致 Isabelle 的解析失败。∀a(∀a. (P a ⟹ Q a)) ⟹ R a

如何正确量化句子的特定部分？

注意：我知道引理中的自由变量在 Isabelle 中是隐式通用的。这个问题主要针对内部陈述，其中量词不应覆盖整个句子。

标签： isabelle

Answer 1