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.