PlanetMath: many-sorted structure

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (198)
Orphanage
Unclass'd
Unproven (490)
Corrections (7)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

many-sorted structure

(Definition)

Let be a many-sorted language and the set of sorts. A many-sorted structure for , or simply an -structure consists of the following:

for each sort $s\in S$ , a non-empty set ,
for each function symbol of sort type $(s_1,\ldots, s_n)$ :
- if , a function $f_M: A_{s_1}\times \cdots \times A_{s_{n-1}} \to A_{s_n}$
- if (constant symbol), an element $f_M\in A_{s_1}$
for each relation symbol of sort type $(s_1,\ldots,s_n)$ , a relation (or subset)
$\displaystyle r_M\subseteq A_{s_1}\times \cdots \times A_{s_n}.$

Remark. A many-sorted structure is a special case of a more general concept called a many-sorted interpretation, which consists all of items 1-3 above, as well as the following:

4.: an element $x_M\in A_s$ for each variable of sort .

Example. a left module over a ring can be thought of as a two-sorted structure (say, with sorts $\lbrace s_1,s_2\rbrace$ ), for there are

there are two non-empty sets (corresponding to sort ) and (corresponding to sort ), where
has the structure of an abelian group (equipped with three operations: , corresponding to function symbols of sort types , and )
has the structure of a ring (equipped with at least four operations: $0,-,+,\times$ , corresponding to function symbols of sort types and for and $\times$ , and possibly a fifth operation of sort type )
a function $\cdot: R\times M\to M$ , which corresponds to a function symbol of sort type . Clearly, $\cdot$ is the scalar multiplication on the module .

For a right module over a ring, one merely replaces the sort type of the last function symbol by the sort type

More to come...

"many-sorted structure" is owned by CWoo.

(view preamble)

Other names:

many sorted structure

Also defines:

many-sorted interpretation

This object's parent.

Log in to rate this entry.
(view current ratings)

Cross-references: scalar, operations, abelian group, structure, ring, left module, variable, subset, relation, relation symbol, constant symbol, function, sort type, function symbol, sorts, many-sorted language

This is version 3 of many-sorted structure, born on 2008-01-22, modified 2008-01-25.
Object id is 10206, canonical name is ManySortedStructure.
Accessed 408 times total.

Classification:

AMS MSC:	03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic)
	03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)
	03B70 (Mathematical logic and foundations :: General logic :: Logic in computer science)

Pending Errata and Addenda

None.

Discussion

forum policy

No messages.

Interact