*To*: "Lawrence Paulson" <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?*From*: Yannick <yannick_duchene at yahoo.fr>*Date*: Thu, 26 Dec 2013 20:42:07 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <67E9B945-5E49-44F1-9222-3464C0D9CE20@cam.ac.uk>*References*: <op.w8nc4f05ule2fv@cardamome> <67E9B945-5E49-44F1-9222-3464C0D9CE20@cam.ac.uk>*Reply-to*: yannick_duchene at yahoo.fr*User-agent*: Opera Mail/12.16 (Linux)

Indeed, a short answer is on page 2:

However, in their system it is impossible to express that a type belongs to more than one class. To overcome this difficulty we introduce sorts as finite sets of classes.

Christmas greetings to you too!Sorts regulate polymorphism, which is necessary in the case of Isabelle,since unconstrained polymorphism would break the logical framework. Moredetails here:http://www21.in.tum.de/~nipkow/pubs/jfp95.html Larry PaulsonOn 25 Dec 2013, at 12:03, Yannick Duchêne (Hibou57)<yannick_duchene at yahoo.fr> wrote:Hi people, and Merry Christmas to all of you for whom that matters,I know I should know, but I don't know, so the question: Isabelledocumentation often refers to sorts, something I've never botheredabout so far. Is this the same as what Wikipedia describes as beingsorts in the context of second order logic?http://en.wikipedia.org/wiki/Second-order_logic

-- Yannick Duchêne

**References**:**[isabelle] Are sorts of Isabelle the same as what's described for second order logic?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Previous by Thread: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Next by Thread: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list