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



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.


On Wed, 25 Dec 2013 13:18:18 +0100, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

Christmas greetings to you too!

Sorts regulate polymorphism, which is necessary in the case of Isabelle, since unconstrained polymorphism would break the logical framework. More details here:

http://www21.in.tum.de/~nipkow/pubs/jfp95.html

Larry Paulson


On 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: Isabelle documentation often refers to sorts, something I've never bothered about so far. Is this the same as what Wikipedia describes as being sorts in the context of second order logic?

http://en.wikipedia.org/wiki/Second-order_logic


--
Yannick Duchêne




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