# [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.*