[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