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

Marry Christmas,

the short answer to your question is: no, what the Wikipedia article describes is not called "sorts" (but "types") in Isabelle/HOL.

As Larry already said, sorts control polymorphism. More specifically sorts are linked to Isabelle's axiomatic type classes. (See also the fine tutorial on type classes that is part of Isabelle's documentation.)

E.g., you might want to prove something for all "entities" that support some operator, say "plus", that satisfies associativity. This you might encapsulate into a type class

  class plus_assoc =
    fixes plus :: "'a => 'a => 'a"
    assumes assoc: "plus x (plus y z) = plus (plus x y) z"

Now by saying that something "is of sort plus_assoc" we mean that it "is an instance of the class plus_assoc", which in turn means that it "has an operator plus that is associative". For example, we could prove that natural numbers are an instance of class plus_assoc:

  instantiation nat :: plus_assoc

  definition "plus_nat (x::nat) y = x + y"

  instance by (intro_classes) (simp add: plus_nat_def)


Now we can use "plus" on natural numbers

  term "plus 0 (Suc 0)"

hope this helps


On 12/25/2013 01:03 PM, Yannick Duchêne (Hibou57) 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?


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?

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