Re: [isabelle] \forall versus \And -- also \exists versus \Or

How do schematic variables relate to \And quantified variables? I know
that sometimes I need to use 'case' and sometimes 'case_tac' for
example, but it's not clear to me why I can't freely move a variable
from being \And quantified to being schematic and vice-versa.


On Tue, Apr 7, 2015 at 4:07 AM, Makarius <makarius at> wrote:
> 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.