Yannick Duchêne (Hibou57)

2013-12-25 12:10:17 UTC

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

list, is that what Isabelle names arities?

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 theformed 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.

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

“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