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
--> etc.

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
  beginners.


	Makarius




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