[isabelle] \forall versus \And -- also \exists versus \Or



(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? (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? Certainly \Or x. P(x) appears to do the same thing as \exists x. P(x) . Further confusing me here is that a number of example Isar proof statements do use \exists instead of \Or, such as lemma assumes Pf: "\exists x. P(f x)" shows "\exists y. P y" (p. 10 of "A Tutorial Introduction To Structured Isar Proofs"). (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 ? (4) Am I understanding correctly that \And applied to the null set is True, while \Or applied to the null set is False?

--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.