Email Gateway (Mar 02 2022 at 10:55): Email Gateway (Mar 02 2022 at 10:55):From: FRANCISCO JESUS MARTIN MATEOS <fjesus@us.es>
Hello
I teach Mathematical Logic at University of Seville and I use Isabelle to explain natural deduction rules.
I have found a situation difficult to explain to my students. It happens when we use 'frule' with 'impI', for example, in order to prove
"(P ⟹ Q) ⟹ P ⟶ Q" (this is a simplified situation):
A typical proof could be:
lemma
"(P ⟹ Q) ⟹ P ⟶ Q"
apply (drule impI)
apply assumption
done
But if I use 'frule' instead of 'drule' the new goal generated is:
(P ⟹ Q) ⟹ ?P ⟶ ?P ⟹ P ⟶ Q
I consider that 'drule' is the same as 'frule' but dropping the assumption used to unify the premise, as is indicated in https://svhol.pbmichel.com/reference/frule, so I don't understand why the new hypotesis included by 'frule' is '?P ⟶ ?P'.
Moreover, (frule_tac P="P" and Q="Q" in impI) does not work.
Could you explain me this?
Thanks in advance.
Regards
Francisco J. Martín Mateos
Computational Logic Group
University of Seville
Email Gateway (Mar 02 2022 at 11:35):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Francisco,
These low-level natural deduction proof methods need to be used with the correct sort of natural deduction inference rule. These are classified as
Introduction rules, indicated by the suffix I
For these, including impI, the appropriate proof method is “rule”.
Elimination rules, indicated by the suffix E
(these should have a fully general conclusion such as ?P that’s also in all the minor premises)
For these, say conjE, disjE, impCE or exE, the appropriate proof method is “erule”.
Destruction rules, sometimes indicated by the suffix D
(my own terminology, for elimination rules not of the form above)
For these, say conjunct1, mp or spec, the appropriate proof methods are “drule” and “frule”.
To me the mystery is not that frule exhibits the behaviour you show, but that either drule or frule succeed at all. They are intended to operate on a formula of the object logic (i.e., first-order or higher-order logic) and not on anything of the form P ==> Q, which is a formula of the logical framework itself.
Try your examples using the appropriate proof method and see how that goes.
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC