Re: [isabelle] universal quantifiers vs. schematic variables



The answer to this question is simple: induction rules are formulated in this way in Isabelle because Martin-LÃf used the same approach in his constructive type theory. He arrived at this formulation by following the idea of natural deduction consistently. In natural deduction, every inference rule introduces or eliminates a distinguished symbol, and Martin-LÃf recognised that in the case of induction rules, the symbol being eliminated was the premise ân is a natural numberâ. He used a similar approach with the elimination rules for finite sums and products, generalised sums, etc.

One does not have to be a constructivist to to recognise that his was the right approach, and that attaching a universal quantifier to the conclusion is superfluous.

Larry Paulson


> On 5 Oct 2015, at 03:51, Alfio Martini <alfio.martini at acm.org> wrote:
> 
> This for me is a very good explanation for something that has always
> puzzled me, i.e., the way induction rules are formalized
> in Isabelle. For instance, the rule nat_induct0 is formalized as follows:
> 
> lemma nat_induct0:
>  fixes n
>  assumes "P 0" and "ân. P n â P (Suc n)"
>  shows "P n"
> 
> If I would formulate this rule, I would (unnecessarily I see), write the
> conclusion as "!n. P n", since this is what the rule allows me
> to infer if the premises are satisfied. From the logical point of view, it
> would have a clearer and more natural reading.





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