Quantifying over a specific part of the sentence in Isabelle

user_14656198 0
Viewed 55

Suppose I write a lemma "(∀a. P a ⟹ Q a) ⟹ R b" in Isabelle. ∀a will only quantify over P a. If I want to quantify over P a ⟹ Q a however, putting parenthesis after ∀a (i.e "(∀a. (P a ⟹ Q a)) ⟹ R a") will cause Isabelle's parsing to fail.

How can I properly quantify over a specific part of the sentence?

Note: I know that free variables in lemmas are implicitly universal in Isabelle. This question is mostly for inner statements, in which the quantifier should not range over the whole sentence.

isabelle
1 Answers

I believe that the parse failure stems from the fact that Isabelle/HOL has two distinct types of implication operators, Pure.imp (⟹) and HOL.implies (⟶). The former is part of the Isabelle metalogic while the latter is part of the HOL logic. You can find more information about why this distinction exists and when to use each in these mailing list posts:

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

The ⟹ operator has very low precedence, lower than ∀ and as a result ∀a. (P a ⟹ Q a) cannot be parsed as you would expect. You may fix the parse failure in your lemma by using the ⟶ operator instead which has higher precedence than ∀. Another option is to change ∀ to the meta quantifier ⋀, making your sentence more in line with Isabelle's framework.

A table of operator precedence is available but I cannot guarantee that it is up to date. You can use the print_syntax command in Isabelle for a more reliably up-to-date ordering.

Table: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/pdfi7tZP06fqA.pdf

user_134306160
Related