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

[Yannick Duchêne (Hibou57)]

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

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)
* 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?

[Lawrence Paulson]

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

Post by Yannick Duchêne (Hibou57)
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

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)
* 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

[Yannick]

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.
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
http://www21.in.tum.de/~nipkow/pubs/jfp95.html
Larry Paulson
On 25 Dec 2013, at 12:03, Yannick Duchêne (Hibou57)

Post by Yannick Duchêne (Hibou57)
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

[Christian Sternagel]

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
begin

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

instance by (intro_classes) (simp add: plus_nat_def)

end

Now we can use "plus" on natural numbers

term "plus 0 (Suc 0)"

hope this helps

chris

Post by Yannick Duchêne (Hibou57)
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

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)
* 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?

[Makarius]

Post by Yannick Duchêne (Hibou57)
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