*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Wed, 25 Dec 2013 13:03:41 +0100*Organization*: Ada @ Home*User-agent*: Opera Mail/12.16 (Linux)

Hi people, and Merry Christmas to all of you for whom that matters,

http://en.wikipedia.org/wiki/Second-order_logic Quote:

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 Sis a variable of this sort and t is a first-order term then theexpression t ∈ S (also written S(t), or St to save parentheses)is an atomic formula. Sets of individuals can also be viewed asunary relations on the domain.* For each natural number k there is a sort of variables that rangesover all k-ary relations on the individuals. If R is such a k-aryrelation variable and t1,..., tk are first-order terms then theexpression R(t1,...,tk) is an atomic formula.* For each natural number k there is a sort of variables that rangesover all functions taking k elements of the domain and returning asingle element of the domain. If f is such a k-ary function variableand t1,...,tk are first-order terms then the expression f(t1,...,tk)is a first-order term.

-- “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

**Follow-Ups**:**Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?***From:*Lawrence Paulson

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

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

- Previous by Date: Re: [isabelle] My unforgivable soundness issue with a locale
- Next by Date: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Previous by Thread: [isabelle] TYPES Meeting 2014 in Paris, 12 - 15 May: first call for contributions
- Next by Thread: Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic?
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list