Re: [isabelle] universal quantifiers vs. schematic variables



Schematic variables have been part of Isabelle from the very beginning. The idea has always been that it should be possible to prove something by transitivity, without first knowing what the intermediate term would be. From a strictly logical point of view, schematic variables are simply variables (necessarily free variables, as there is no way of binding them).

Larry Paulson


> On 4 Oct 2015, at 19:24, Lars Hupel <hupel at in.tum.de> wrote:
> 
> 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.