*To*: "Yannick Duchêne (Hibou57)" <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 25 Dec 2013 12:18:18 +0000*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.w8nc4f05ule2fv@cardamome>*References*: <op.w8nc4f05ule2fv@cardamome>

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 > > Quote: > >> The syntax of second-order logic tells which expressions are well >> formed formulas. In addition to the syntax of first-order logic, >> second-order logic includes many new sorts (sometimes called types) >> of variables. These are: >> >> * A sort of variables that range over sets of individuals. If S >> is a variable of this sort and t is a first-order term then the expression t ∈ S (also written S(t), or St to save parentheses) is an atomic formula. Sets of individuals can also be viewed as unary relations on the domain. >> * For each natural number k there is a sort of variables that ranges over all k-ary relations on the individuals. If R is such a k-ary relation variable and t1,..., tk are first-order terms then the expression R(t1,...,tk) is an atomic formula. >> * For each natural number k there is a sort of variables that ranges over all functions taking k elements of the domain and returning a single element of the domain. If f is such a k-ary function variable and t1,...,tk are first-order terms then the expression f(t1,...,tk) is a first-order term. > > Is that the relevant definition of sorts? And the second point in the list, is that what Isabelle names arities? > > > > -- > “Syntactic sugar causes cancer of the semi-colons.” [1] > “Structured Programming supports the law of the excluded muddle.” [1] > [1]: Epigrams on Programming — Alan J. — P. Yale University > >

**Follow-Ups**:

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

- Previous by Date: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Next by Date: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Previous by Thread: [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