many-sorted language

A many-sorted language is a variation of the classical first-order language. Whereas structuresMathworldPlanetmath of a first-order language consist of a single universePlanetmathPlanetmath, structures of a many-sorted language may contain many “universes”, where each universe is “named” by a symbol called “sort”, hence the name “many-sorted”.

To formalize the notion of a many-sorted language, we start with a non-empty set S whose elements we call sorts. Let S+ be the set of all (finite) non-empty words over S. Elements of S+ are called sort types and are written as tuples. So instead of writing s1s2snS+, it is written (s1,s2,,sn)S+.

The next item to be defined is the underlying signaturePlanetmathPlanetmathPlanetmath of a many-sorted language. A signature Σ consists of

  • a non-empty set S of sorts,

  • a set F of function symbols, and

  • a set R of (non-logical) relation symbols,

such that each element in FR corresponds to a sort type. In other words, there is a function t:FRS+, and for every rFR, t(r) is its sort type. An element cF such that t(c)S is called a constant symbol (of sort t(c)).

In additionPlanetmathPlanetmath to the signature Σ, we introduce additional symbols:

  • the set V of variablesMathworldPlanetmath, such that each sort sS corresponds to a countably infiniteMathworldPlanetmath subset VsV of variables. In other words, there is a function v:VS, such that for each sS, v-1(s) is countably infinite. For each variable xV, its sort is defined to be v(x).

  • logical predicatesMathworldPlanetmathPlanetmath: ,¬,

  • the equality relation symbol: =, and

  • the left and right parentheses: (,)

Using Σ and the additional symbols above, we can build terms inductively as follows:

  • each variable xV is a term of sort v(x)

  • if fF is a function symbol of sort type (s1,,sn), and for each i=1,,n-1, ti is a term of sort si, then f(t1,,tn-1) is a term of sort sn.

  • all the terms are built this way.

Finally, from the terms, we inductively define formulasMathworldPlanetmath:

  • if t1 and t2 are terms of the same sort, then (t1=t2) is a formula

  • if rR is a relation symbol of sort type (s1,,sn), and for each i=1,,n, ti is a term of sort si, then r(t1,,tn) is a formula

  • if α is a formula, then so is (¬α)

  • if α,β are formulas, then so is (αβ)

  • if α is a formula and xV is a variable, then so is (x(α))

  • all the formulas are formed this way.

The signature Σ, additional symbols, and terms and formulas subsequently defined constitute what is known as the many-sorted language L=L(Σ) on Σ.

As in first order language, the outer most parentheses may be eliminated without causing much harm, so that (¬α) becomes ¬α. In addition, we may introduce other familiar logical symbols ,,, and in terms of ,¬, and . The specifics of how this is done can be found in the entry on first order language.

From this definition, we see at once that the classical first order language is a one-sorted languagePlanetmathPlanetmath (S=1). Sort types are identified with their lengths. Thus, the sort type of a function or a relation symbol is its arity.

Remark. It is not hard to show that a many-sorted language is not much different from a first-order language. Provided that V is countably infinite, a many-sorted language L can be “converted” into a first-ordered language L1. Basically, all the function and relation symbols in L are in L, as well as the additional symbols such as variables and logical symbols. For each sort sS, we introduce a new unary relation symbol Ps in L1. For any formula that contains a subformula of the form xϕ(x), we replace each occurrence of such a subformula by a formula of the form x(Ps(x)ϕ(x)), where x is a variable of sort s and ϕ is some formula in which x occurs as a free variableMathworldPlanetmathPlanetmath. The result is that L1 becomes a one-sorted language.

Title many-sorted language
Canonical name ManysortedLanguage
Date of creation 2013-03-22 17:44:40
Last modified on 2013-03-22 17:44:40
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 12
Author CWoo (3771)
Entry type Definition
Classification msc 03B70
Classification msc 03C07
Classification msc 03B10
Synonym many sorted language
Synonym many-sorted logic
Defines sort
Defines sort type