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



On 07.04.2015 05:27, 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?

The short answer is: Isabelle cannot reason about the HOL quantifiers
(and boolean connectives) directly, only by referring to their
characterisation in terms of the Pure (ore meta) counterparts <\And> and
\<Longrightarrow>.

So for lemmas you want to use into a proof (as opposed to maybe the
final theorem of a large development, which should just read nice),
you express it in terms of the meta operations as much as possible.
Otherwise, you can expect a lot of manual fiddling around, bringing the
theorem into a useful shape everytime you use it (although this depends
on the tools you use: metis for example doesn't care at all).

Some background:

In a way, \<And> is an artifact of Isabelle's Design. Isabelle was
designed as a generic theorem prover which one can use to formalise and
reason in various logics.

As such, Isabelle's kernel knows how to reason about a few primitive
constants, namely:

  Pure.all :: ('a => prop) => prop (written as \<And>)
  Pure.imp :: prop => prop => prop (written as \<Longrightarrow>)

We can use this logical framework (also refered to as Isabelle/Pure)
to formalise a logic (e.g. HOL) by declaring new constants and adding
rules (made from the primitive constants) as axioms (this is called an
"object logic" in Isabelle's notation). So implementing a new logic in
Isabelle does not involve writing code or changing the kernel, but just
writing a few rules in the logical framework.

Now, Isabelle/HOL has its own variants of the above operators,

  HOL.All :: ('a => bool) => bool (written as \<forall>)
  HOL.implies :: bool => bool => bool (written as \<longrightarrow>)

Note the different types and that bool and prop are not isomorphic (as
Isabelle/Pure does not have the law of the exluced middle).

> (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?

There is no existential quantifier at the meta level. I'm not sure,
where \<Or> comes from (I don't have a current Isabelle at hand, at the
moment), but \<exists> is the common way to write an existential in
Isabell/HOL.

> (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 ?

There is no such syntax for \<And>.

> (4) Am I understanding correctly that \And applied to the null set is
> True, while \Or applied to the null set is False?

As HOL types are never empty, \<And> can never be applied "to the null
set". If you talk about "\<forall> x \<in> S. P x", yes, this is true if
S is empty.

  -- Lars




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