*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] \forall versus \And -- also \exists versus \Or*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Tue, 07 Apr 2015 09:07:47 +0200*In-reply-to*: <a062007b6d1485c6fc401@[192.168.1.20]>*References*: <a062007b6d1485c6fc401@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.2.0

On 07.04.2015 05:27, W. Douglas Maurer wrote: > (1) I am having trouble understanding why Isar permits both \forall and > \And, seeing that they appear to do exactly the same thing. I understand > that \And is for the statement of a theorem or lemma, and is not > supposed to be used in a proof. But what would happen if we used \forall > in the statement of a lemma, rather than \And? How would this affect the > rest of the proof? The short answer is: Isabelle cannot reason about the HOL quantifiers (and boolean connectives) directly, only by referring to their characterisation in terms of the Pure (ore meta) counterparts <\And> and \<Longrightarrow>. So for lemmas you want to use into a proof (as opposed to maybe the final theorem of a large development, which should just read nice), you express it in terms of the meta operations as much as possible. Otherwise, you can expect a lot of manual fiddling around, bringing the theorem into a useful shape everytime you use it (although this depends on the tools you use: metis for example doesn't care at all). Some background: In a way, \<And> is an artifact of Isabelle's Design. Isabelle was designed as a generic theorem prover which one can use to formalise and reason in various logics. As such, Isabelle's kernel knows how to reason about a few primitive constants, namely: Pure.all :: ('a => prop) => prop (written as \<And>) Pure.imp :: prop => prop => prop (written as \<Longrightarrow>) We can use this logical framework (also refered to as Isabelle/Pure) to formalise a logic (e.g. HOL) by declaring new constants and adding rules (made from the primitive constants) as axioms (this is called an "object logic" in Isabelle's notation). So implementing a new logic in Isabelle does not involve writing code or changing the kernel, but just writing a few rules in the logical framework. Now, Isabelle/HOL has its own variants of the above operators, HOL.All :: ('a => bool) => bool (written as \<forall>) HOL.implies :: bool => bool => bool (written as \<longrightarrow>) Note the different types and that bool and prop are not isomorphic (as Isabelle/Pure does not have the law of the exluced middle). > (2) Am I to understand that, just as \And is the universal quantifier at > the meta-level, \Or is the existential quantifier at the meta-level? There is no existential quantifier at the meta level. I'm not sure, where \<Or> comes from (I don't have a current Isabelle at hand, at the moment), but \<exists> is the common way to write an existential in Isabell/HOL. > (3) In Whats In Main, under Orderings, under Syntax, there is given some > syntax for \forall and for \exists, such as \forall x \leq y. P \equiv > \forall x. x \leq y --> P . There are eight rules given here, four for > \forall and four for \exists . Do these rules also work for \And and \Or ? There is no such syntax for \<And>. > (4) Am I understanding correctly that \And applied to the null set is > True, while \Or applied to the null set is False? As HOL types are never empty, \<And> can never be applied "to the null set". If you talk about "\<forall> x \<in> S. P x", yes, this is true if S is empty. -- Lars

**References**:**[isabelle] \forall versus \And -- also \exists versus \Or***From:*W. Douglas Maurer

- Previous by Date: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Date: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Previous by Thread: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list