Re: [isabelle] universal quantifiers vs. schematic variables


> if "P" is a previously defined predicate and I want to prove it always
> holds, it seems I can do it in two ways. the first uses the universal
> quantifier as in
>     lemma "!x. P(x)"
>     ....
> and the second uses schematic variables, as in
>     lemma  "P(x)"
>     ...
> if I'm not mistaken each of these can be used to prove the other, so they
> are logically equivalent. the only differences I could find were in the way
> the proved lemmas can be used in proofs, where usually the second
> formulation is easier to use.

first of all, your assessment is correct. Nitpicking: In the second
formulation, you use the free variable 'x', which â after proving the
lemma â gets generalized to a schematic variable. You can recognize
schematic variables by the prefixed question mark (e.g. '?x').

> and if so why does Isabelle offer two different ways to say the same thing.
> comparing to the case of --> and ==>, the different arrows are also
> logically equivalent but they are intended for different situations, but I
> couldn't find such distinction in the universal case.

I don't have an insight into the early history of Isabelle. I have the
understanding that the notion of schematic has been there for a long
time. The only explanation I can offer is that schematic variables can
be easily instantiated. For example, if you have the theorem 'P ?x', you
can substitute '?x' by something arbitrary, without having to know about
the universal quantifier. In the explicitly-quantified case (be it HOL
quantification or Pure quantification), the 'x' would be a bound
variable and you would need to know more. Essentially, schematic
variables allow for easy *outermost* quantification.


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