You are here
Homemanysorted language
Primary tabs
manysorted language
A manysorted language is a variation of the classical firstorder language. Whereas structures of a firstorder language consist of a single universe, structures of a manysorted language may contain many “universes”, where each universe is “named” by a symbol called “sort”, hence the name “manysorted”.
To formalize the notion of a manysorted language, we start with a nonempty set $S$ whose elements we call sorts. Let $S^{+}$ be the set of all (finite) nonempty words over $S$. Elements of $S^{+}$ are called sort types and are written as tuples. So instead of writing $s_{1}s_{2}\cdots s_{n}\in S^{+}$, it is written $(s_{1},s_{2},\cdots,s_{n})\in S^{+}$.
The next item to be defined is the underlying signature of a manysorted language. A signature $\Sigma$ consists of

a nonempty set $S$ of sorts,

a set $F$ of function symbols, and

a set $R$ of (nonlogical) relation symbols,
such that each element in $F\cup R$ corresponds to a sort type. In other words, there is a function $t:F\cup R\to S^{+}$, and for every $r\in F\cup R$, $t(r)$ is its sort type. An element $c\in F$ such that $t(c)\in S$ is called a constant symbol (of sort $t(c)$).
In addition to the signature $\Sigma$, we introduce additional symbols:

the set $V$ of variables, such that each sort $s\in S$ corresponds to a countably infinite subset $V_{s}\subseteq V$ of variables. In other words, there is a function $v:V\to S$, such that for each $s\in S$, $v^{{1}}(s)$ is countably infinite. For each variable $x\in V$, its sort is defined to be $v(x)$.

logical predicates: $\vee,\neg,\forall$

the equality relation symbol: $=$, and

the left and right parentheses: $(,)$
Using $\Sigma$ and the additional symbols above, we can build terms inductively as follows:

each variable $x\in V$ is a term of sort $v(x)$

if $f\in F$ is a function symbol of sort type $(s_{1},\ldots,s_{n})$, and for each $i=1,\ldots,n1$, $t_{i}$ is a term of sort $s_{i}$, then $f(t_{1},\ldots,t_{{n1}})$ is a term of sort $s_{n}$.

all the terms are built this way.
Finally, from the terms, we inductively define formulas:

if $t_{1}$ and $t_{2}$ are terms of the same sort, then $(t_{1}=t_{2})$ is a formula

if $r\in R$ is a relation symbol of sort type $(s_{1},\ldots,s_{n})$, and for each $i=1,\ldots,n$, $t_{i}$ is a term of sort $s_{i}$, then $r(t_{1},\ldots,t_{n})$ is a formula

if $\alpha$ is a formula, then so is $(\neg\alpha)$

if $\alpha,\beta$ are formulas, then so is $(\alpha\vee\beta)$

if $\alpha$ is a formula and $x\in V$ is a variable, then so is $(\forall x(\alpha))$

all the formulas are formed this way.
The signature $\Sigma$, additional symbols, and terms and formulas subsequently defined constitute what is known as the manysorted language $L=L(\Sigma)$ on $\Sigma$.
As in first order language, the outer most parentheses may be eliminated without causing much harm, so that $(\neg\alpha)$ becomes $\neg\alpha$. In addition, we may introduce other familiar logical symbols $\wedge,\to,\leftrightarrow$, and $\exists$ in terms of $\vee,\neg$, and $\forall$. 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 onesorted language ($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 manysorted language is not much different from a firstorder language. Provided that $V$ is countably infinite, a manysorted language $L$ can be “converted” into a firstordered language $L_{1}$. Basically, all the function and relation symbols in $L$ are in $L^{{\prime}}$, as well as the additional symbols such as variables and logical symbols. For each sort $s\in S$, we introduce a new unary relation symbol $P_{s}$ in $L_{1}$. For any formula that contains a subformula of the form $\forall x\phi(x)$, we replace each occurrence of such a subformula by a formula of the form $\forall x(P_{s}(x)\to\phi(x))$, where $x$ is a variable of sort $s$ and $\phi$ is some formula in which $x$ occurs as a free variable. The result is that $L_{1}$ becomes a onesorted language.
Mathematics Subject Classification
03B70 no label found03C07 no label found03B10 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections