Re: [isabelle] \forall versus \And -- also \exists versus \Or
On Mon, 6 Apr 2015, 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?
You should not think of !! as the same as ALL, and ==> as the same as
Just a few notes on this, to overcome common misunderstandings.
* Isabelle/Pure is minimal higher-order logic with connectives !! and ==>
used to describe natural deduction rules declaratively. The
Isabelle/Isar proof languages uses the same rule format to produce
structured proofs. These concepts are integral to Isabelle, and big
assets of its approach; schematic variables also belong here.
* Isabelle/HOL is full higher-order logic with the whole zoo of
connectives (ALL, EX, -->, <-->, ~ etc.) and much more, to work with
applications. HOL statements may occur in Pure rules naturally.
* The view of Pure as "meta-logic" and HOL as "object-logic" is OK in the
historical understanding of Isabelle as "logical framework" to declare
other logics, but it has little practical relevance today.
* The view of Pure as "rule framework for structured reasoning" is very
relevant today. It is the canonical way how I usually explain that to
This archive was generated by a fusion of
Pipermail (Mailman edition) and