*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] \forall versus \And -- also \exists versus \Or*From*: Makarius <makarius at sketis.net>*Date*: Tue, 7 Apr 2015 11:07:32 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <a062007b6d1485c6fc401@[192.168.1.20]>*References*: <a062007b6d1485c6fc401@[192.168.1.20]>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 \Andis for the statement of a theorem or lemma, and is not supposed to be used ina proof. But what would happen if we used \forall in the statement of alemma, 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

**Follow-Ups**:**Re: [isabelle] \forall versus \And -- also \exists versus \Or***From:*Andrew Gacek

**References**:**[isabelle] \forall versus \And -- also \exists versus \Or***From:*W. Douglas Maurer

- Previous by Date: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Date: Re: [isabelle] Modify theorem with equality assumption
- Previous by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list