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

On Wed, 25 Dec 2013, Yannick Duchêne (Hibou57) wrote:

`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?
`

`In logic literature there is a general shortage of words for things that
``qualify other things. So "type", "class", "sort", "kind", "mode" etc.
``occur with varying meaning, depending on the context and the author.
`

`In Isabelle/Pure, a sort is just a syntactic representation for the
``intersection of finitely many type classes, and the empty intersection {}
``is the "top" or "full" sort (not the empty sort).
`
Makarius

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