Email Gateway (Aug 19 2022 at 17:12): Email Gateway (Aug 19 2022 at 17:12):From: mahmoud abdelazim <m.abdelazim@icloud.com>
What is the difference in Isabelle between Universal Quantification /\ and ∀ ?
What is the difference in Isabelle between the implications => and -> ?
Email Gateway (Aug 19 2022 at 17:13):From: Larry Paulson <lp15@cam.ac.uk>
This is a fundamental question about Isabelle as a logical framework. Isabelle provides general inference mechanisms for combining proofs and for proving not just simple statements, but what are essentially inference rules. This requires a form of universal quantification and a form of implication that operate outside the level of logical assertions.
The advantage of having separate symbols can be seen when comparing Isabelle proofs with those done in other implementations of higher-order logic. Let suppose that you have proved the theorem
P(x,y) ==> Q(y) ==> P (x, f x).
With Isabelle, the quantification over x and y and the implications for P and Q are dealt with automatically, whether you use this “forwards” or “backwards”. But in a traditional HOL system, you’ll devote effort to removing the quantifiers and reasoning with the implications. And the difference is even greater when you use or derive specialist induction rules.
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC