Variety logic

Sort logic arises from the intention not to regard the (set theoretical) universe ( basic set , universal class , up to a Grothendieck universe ) as a homogeneous collection of (mathematical) objects , but to divide them into different classes or types, which in this context are sorts (similar to the data types in many programming languages and database systems ). A variety is assigned to each term in a logical formula . Unification of terms is only allowed if both terms are of the same kind; Substitution and transfer of arguments can also only take place under consideration of these varieties. Incorrect type assignments are therefore already shown as syntax errors .

See also : object (programming) , math formula, and substitution (math)

See also : Arguments  and Functional Programming

motivation

From the point of view of predicate logic (without varieties), varieties are single-digit relations ( variety predicates ), but incorrect assignments to varieties no longer appear as syntax errors, but as incorrect after assigning a semantic . Variety logic, on the other hand, provides a special treatment of the form just mentioned for these predicates .

In contrast to the second level predicate logic with relation variables , the variety logic therefore does not offer any increase in power, for example with regard to questions of provability. Since many deduction steps do not have to be taken into account because of the variety incompatibility, the search effort for a proof is considerably reduced in practice.

Multi-sort structures form a set theoretical model for the data types in information technology , especially in databases , which is why they are of considerable practical importance. In addition, multivariate is a possibility to take into account the issues related to type theories on a set theoretical basis.

Classification and demarcation

In principle, there are different ways of realizing this intention. Common to most of the cases

• there are a lot of varieties (in information technology and data t ypes called)  ${\displaystyle T}$
• there is a generalization of the term signature in order to take into account the additional information associated with the varieties.

In the entire universe, as a summary of all objects of a structure, the value ranges for the various types are then delimited.

The algebraization of sort logic is described in an article by Caleiro and Gonçalves and can serve well as an introduction to the matter.

Diverse logic

In the many-sided logic , the pairwise disjointness of the value ranges (also called carrier sets ) for the different types is assumed.

In vielsortigen signatures are compared to ordinary one-sorted signatures to the function and relations and reported constant symbols nor specially possibly names for the varieties , d. H. add the value ranges. Each of the symbols is now no longer identified only by the arity, but by the exact sequence of the types of arguments, and possibly a type of value or image. An n-ary relation is a subset of the n-fold Cartesian product of a sequence of carrier sets . The argument range of an n-place function is just such a product, plus one of the carrier sets for the image (function value).

Examples

• An example is provided by taxa (groups) of biological organisms , including and . While a function makes sense, a similar function would generally not. Sort logic allows terms of the kind , but rejects them as incorrect syntactic constructions. ${\displaystyle {\textit {Pflanze}}}$ ${\displaystyle {\textit {Tier}}}$ ${\displaystyle {\textit {Mutter}}:{\textit {Tier}}\longrightarrow {\textit {Tier}}}$ ${\displaystyle {\textit {Mutter}}:{\textit {Pflanze}}\longrightarrow {\textit {Pflanze}}}$ ${\displaystyle {\textit {Mutter}}(}$ ${\displaystyle {\textit {Rex}}}$ ${\displaystyle )}$ ${\displaystyle {\textit {Mutter}}(}$ ${\displaystyle {\textit {Schaeferbuche}}}$ ${\displaystyle )}$

• Diverse structures of the first level are, for example, the following heterogeneous algebras :
  • Vector spaces over a body (left and right vector spaces in the case of a sloping body, bivector spaces ) - with the types scalar and vector
  • Modules over a commutative ring (left, right modules in any ring, bimodules) - a generalization of the concept (i.e. category ) vector space
  • Algebras over a field or commutative ring - as special vector spaces
  • Lie algebras and commutative algebras over a field - both special algebras over this field
  • Affine spaces are examples of three-order structures with a point space and a vector space with a set of supports over a body , the points are linked to the vectors via an operation called parallel displacement. ${\displaystyle A}$ ${\displaystyle V}$ ${\displaystyle K}$

definition

Let and be disjoint sets of non-logical signs. Let also be another finite and non-empty set of non-logical signs disjoint from it. One then calls ${\displaystyle {\mathcal {F}}_{0}}$ ${\displaystyle {\mathcal {R}}_{0}}$ ${\displaystyle T}$

• each character into a symbol and a set of symbols , ${\displaystyle {\mathcal {S}}:={\mathcal {F}}_{0}\cup {\mathcal {R}}_{0}}$ ${\displaystyle {\mathcal {S}}}$
• each character in a variety , ${\displaystyle T}$

if a sequence ( tuple ) of types is assigned to each symbol as a type by mapping , namely: ${\displaystyle \tau }$

• ${\displaystyle \tau (f)\in T^{k+1}}$for everyone with ardor , and ${\displaystyle f\in {\mathcal {F}}_{0}}$ ${\displaystyle k=\sigma (f)\in \mathbb {N} _{0}}$
• ${\displaystyle \tau (R)\in T^{k}}$for everyone , with ardor . ${\displaystyle R\in {\mathcal {R}}_{0}}$ ${\displaystyle k=\sigma (R)\in \mathbb {N} _{0}}$

${\displaystyle {\boldsymbol {S}}:=(T,{\mathcal {S}},\tau )}$is then called a multiple or multi- site signature .

Remarks

1. As in the single-species case, each is referred to as a function symbol , each as a relation symbol (or predicate symbol ). ${\displaystyle f\in {\mathcal {F}}_{0}}$ ${\displaystyle R\in {\mathcal {R}}_{0}}$
2. The multi-faceted signature is used to assign ${\displaystyle {\boldsymbol {S}}}$
   • the relation symbols of arity a type ( argument type ) consisting of the argument types and ${\displaystyle R}$ ${\displaystyle k=\sigma (R)}$ ${\displaystyle \tau (R)={\boldsymbol {s}}=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k})\in T^{k}}$ ${\displaystyle k}$ ${\displaystyle {\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k}}$
   • the function symbols of arity a type consisting of the argument type (i.e. the types of arguments as in the case of relations) and additionally the type of image . ${\displaystyle f}$ ${\displaystyle k=\sigma (f)}$ ${\displaystyle \tau (f)=({\boldsymbol {s}};s')=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')\in T^{k+1}}$ ${\displaystyle {\boldsymbol {s}}}$ ${\displaystyle k}$ ${\displaystyle s'=\tau (f)_{n+1}}$

The sequences (tuples) of the symbol types (the image values ​​of ) can be interpreted as words (strings) above the sort alphabet . In set theory, these are elements of Kleen's shell . ${\displaystyle \tau }$ ${\displaystyle T}$ ${\displaystyle T^{*}}$

3. The zero-digit function symbols are interpreted as constant symbols of the variety . ${\displaystyle c\in {\mathcal {C}}:=\{f\in {\mathcal {F}}_{0}|\tau (f)\in T\}}$ ${\displaystyle \tau (f)}$
4. Possibly. Existing zero-digit relation symbols are interpreted analogously as - propositional (or Boolean ) constant symbols . ${\displaystyle b\in {\mathcal {B}}:=\{R\in {\mathcal {T}}_{0}|\tau (R)=\epsilon \}}$
5. Similar to the single-species case with arity, instead of the image that assigns each symbol its type , one can look at its original image fibers. Specifically, these are the families and  ; in functional notation: ${\displaystyle \tau }$ ${\displaystyle T^{*}}$ ${\displaystyle {\boldsymbol {\mathcal {R}}}=({\boldsymbol {\mathcal {R}}}_{s})_{s\in {T^{*}}}}$ ${\displaystyle {\boldsymbol {\mathcal {F}}}=({\boldsymbol {\mathcal {F}}}_{s,s'})_{s\in {T^{*}},s'\in {T}}}$
   • ${\displaystyle {\boldsymbol {\mathcal {R}}}:T^{*}\to {\mathcal {R}}_{0}}$assigns the set of relational symbols with this sequence as type to each sequence of sorts (the length of the sequence is the arity); and
   • ${\displaystyle {\boldsymbol {\mathcal {F}}}:T^{+}\to {\mathcal {F}}_{0}}$ assigns the set of function symbols to each non-empty sequence of types, whereby the last type of the sequence in each case designates the image type and the others previously the argument type.

To identify the signature, it is then sufficient to specify the type alphabet together with these two families . ${\displaystyle {\boldsymbol {\mathcal {S}}}=(T,{\boldsymbol {\mathcal {R}}},{\boldsymbol {\mathcal {F}}})}$

6. Instead of identifying the type of function symbol, it is also written. When using the notation, it must always be remembered that descriptions, symbols, types (identifiers) are meant here, not the objects, functions, value ranges (carrier quantities) themselves. The notation is particularly valid when overloaded (the type of image is clearly determined by the argument type ). ${\displaystyle \tau (f)=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')\in T^{k+1}}$ ${\displaystyle f:{\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k}\longrightarrow s'}$
7. The same relation symbol can be used for relations with different argument types. The same applies to function symbols. One then speaks of an overloaded relation symbol (predicate) or function symbol. If one looks at the original image fibers, then the set of relation symbols and the set of function symbols for each fixed image type are no longer necessarily disjoint in pairs when overloaded. For a fixed type of argument , however, the amounts of the action icons are continuing to different image types disjoint: . Consequently, in this case too, the set of all relation symbols and the totality of all function symbols for each image type remain disjoint in pairs. The type assignment is a multifunction ( instead of ) in the event of overload . But even in this case, each symbol has at most one meaning with a fixed argument type: Either it is a relation symbol or a function symbol for a certain type of image . Designates the set of all function symbols with a certain type of argument (i.e. the union across all types of images ), then the restrictions on a certain type of argument ( ) are always clear as images. Even in the case of overloading, the mapping that assigns the image type to each function symbol (as the last coordinate of the multifunction , i.e. with arity ) is unambiguous. A logic without overloads is called strict . ${\displaystyle s'}$ ${\displaystyle {\boldsymbol {s}}\in T^{*}}$ ${\displaystyle s'_{1},s'_{2}\in T}$ ${\displaystyle {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'_{1}}\cap {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'_{2}}=\emptyset }$ ${\displaystyle {\mathcal {R}}_{0}}$ ${\displaystyle {\boldsymbol {\mathcal {F}}}_{*,s}:=\bigcup _{{\boldsymbol {s}}\in {T}^{*}}{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}=\bigcup \{{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}|{\boldsymbol {s}}\in {T}^{*}\}}$ ${\displaystyle s'\in T}$
   ${\displaystyle \tau }$ ${\displaystyle \tau :{\mathcal {S}}\multimap T^{*}}$ ${\displaystyle \tau :{\mathcal {S}}\to T^{*}}$ ${\displaystyle s'}$
   ${\displaystyle {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},*}}$ ${\displaystyle {\boldsymbol {s}}}$ ${\displaystyle \bigcup \{{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}|s'\in T\}}$ ${\displaystyle \tau }$ ${\displaystyle \tau _{t}:=\tau |_{{\boldsymbol {\mathcal {R}}}_{\boldsymbol {s}}\cup {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},*}}}$ ${\displaystyle \tau '}$ ${\displaystyle \tau }$ ${\displaystyle \tau (f)_{n+1}}$ ${\displaystyle n=\sigma (f)}$
   
8. A programming language can, for example, provide integers (int for integer) and character strings (string, with lexicographical order ). The less-than symbol < can to compare two integers or two strings are used: . Again, max and min can serve as examples for multi-sorts overloaded function symbols, which can appear next to each other with the same designation on different total orders. The function symbols min and max can either be applied to n arguments of the data type int or to n arguments of the type string. The type of image is then determined by the type of the arguments, namely the same as the type of each individual argument, int or string. ${\displaystyle <\in {\boldsymbol {\mathcal {R}}}_{\operatorname {int} \operatorname {int} },<\in {\boldsymbol {\mathcal {R}}}_{\operatorname {string} \operatorname {string} }}$
9. The type of logical truth values ​​has a special meaning, if any ; Common names for these are (or ). Relations can be understood as predicates according to their characteristic function , see Relation, § Relations and Functions . Correspondingly, relation symbols can be interpreted as Boolean function symbols with image type . This enables a further simplification to be achieved. An example is the requirement of disjointness of the symbol sets per image type in the event of overloading (elimination of the relations as a special case). In the definition of the terms term and expression (also called formula ) and in their use, the variety has a special role, see below: § Terms in multiple logic and § Expressions in multiple logic . ${\displaystyle \{\operatorname {false} ,\operatorname {true} \}}$ ${\displaystyle \operatorname {logical} }$ ${\displaystyle \operatorname {boolean} }$ ${\displaystyle \operatorname {logical} }$ ${\displaystyle \operatorname {logical} }$

Variable symbols in the case of diversity

A variety must also be specified for the variables. There are essentially two approaches to be found in the literature:

1. A single set of variables is provided. A (possibly only partial) mapping that assigns a variety to variable identifiers is called a variable declaration ; a variable from the domain of the variable declaration is called declared . During the interpretation, this can be replaced in the scope (area of ​​effect) of the respective quantifier by a local variant ( locally modified variable declaration ) with any and ${\displaystyle {\mathcal {V}}}$ ${\displaystyle \nu :{\mathcal {V}}\not \to T}$ ${\displaystyle \nu '=\nu _{\langle x\mapsto s\rangle }}$ ${\displaystyle x\in {\mathcal {V}},s\in T}$

${\displaystyle \nu '(y)=\nu _{\langle x\mapsto s\rangle }(y):={\begin{cases}s&{\text{wenn}}\ y=x,\\\nu (y)&{\text{sonst (auf dem ursprünglichen Definitionsbereich von}}\ \nu {\text{)}};\end{cases}}}$ 

2. Other authors, on the other hand, strictly delimit the sets of symbols for the variables of different types and use a separate set of variable symbols for each type. The variables are z. B. characterized by a variety index. The assignment of a variety to a variable is fixed and is not modified locally. ${\displaystyle \nu }$

The affiliation of a variable to a certain type ( ) is syntactically noted as following the type judgment of type theory . ${\displaystyle \nu (v)=s}$ ${\displaystyle v:s}$

Variable symbols of second level predicate logic

• In the second level predicate logic there are additional relation variables and possibly also function variables . Even in the single-variety case, arity must be ascribed to these; in the case of multivariate, this is expanded to a type, as with the raltion and function symbols. In the literature, fixed assignments (arity) are usually chosen (in single-variety cases). According to the practice in information technology, ( arity or) type declarations with local variants are also possible. The variable declaration must then be expanded accordingly with a value range instead . ${\displaystyle \nu }$ ${\displaystyle T^{*}}$ ${\displaystyle T}$
• The relation variables of the second level predicate logic can be interpreted as function variables with image type . ${\displaystyle \operatorname {logical} }$
• The variables of the variety - if any - are called propositional variables . They correspond to zero-place relation variables. ${\displaystyle \operatorname {logical} }$
• In the second level monadic predicate logic , only single-digit relation variables are permitted. In the multi-faceted case, these are to be identified by the (only) argument type.

Terms in multifaceted logic

definition

With a given signature and variable declaration , the set of terms of the (non-logical) kind is then recursively defined as follows: ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle \nu }$ ${\displaystyle {\mathcal {T}}_{{\boldsymbol {S}},\nu }(s)}$ ${\displaystyle s}$

1. Each variable symbol of a variety is a term of the variety by declaration ${\displaystyle v}$ ${\displaystyle \nu (v)=s}$ ${\displaystyle s}$
2. If a ( -character) function symbol is of the type , and if there is also a term of the kind , a term of the kind , a term of the kind , then a term of the kind is , in particular: ${\displaystyle f}$ ${\displaystyle k}$ ${\displaystyle ({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')}$ ${\displaystyle t_{1}}$ ${\displaystyle {\boldsymbol {s}}_{1}}$ ${\displaystyle t_{2}}$ ${\displaystyle {\boldsymbol {s}}_{2}}$ ${\displaystyle \dots }$ ${\displaystyle t_{k}}$ ${\displaystyle {\boldsymbol {s}}_{k}}$ ${\displaystyle f({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k})}$ ${\displaystyle s'}$
   • Each constant of the variety is a term of the variety by signature ${\displaystyle c}$ ${\displaystyle \tau (c)=s}$ ${\displaystyle s}$

The set of all terms is given by the disjoint union of all non-logical sorts . With an empty variable declaration, the index may relate to: . The function symbols induce links of different types between the elements of the different types or types , with which these sets of different types of character strings themselves become a heterogeneous algebra as term algebra or basic termgebra. ${\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }}$ ${\displaystyle T_{{\boldsymbol {S}},\nu }(s)}$ ${\displaystyle s\in T\setminus \{\operatorname {logical} \}}$ ${\displaystyle \nu }$ ${\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s),\ {\boldsymbol {\mathcal {T}}}_{\boldsymbol {S}}}$
${\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }}$ ${\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s)}$ ${\displaystyle s}$

Remarks

• Infix notation for two-digit functions: instead of , as above. Prefix form: Polish notation without brackets, also as above. Less common: Postfix notation. ${\displaystyle x+1}$ ${\displaystyle +(x,1)}$
• Dot notation instead , instead (as in object-oriented programming). ${\displaystyle x.\operatorname {farbe} }$ ${\displaystyle \operatorname {farbe} (x)}$ ${\displaystyle x.\operatorname {plus} (y)}$ ${\displaystyle x\operatorname {plus} y}$
• Recently, the tree representation of terms has become increasingly important.

Expressions in versatile logic

definition

Given a signature and a variable declaration . An atomic formula (also atomic expression ) is ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle \nu }$

• ${\displaystyle t_{1}=t_{2}}$for all terms of the same sort . ${\displaystyle t_{1},t_{2}}$ ${\displaystyle s\in T}$
• All proposition variables, provided this variety is allowed.
• ${\displaystyle Rt_{1},\dots t_{k}}$for all -digit relation symbols of the type , if term is variety , term is variety , term is variety . ${\displaystyle k}$ ${\displaystyle (s_{1},\dots s_{k})}$ ${\displaystyle t_{1}}$ ${\displaystyle s_{1}\in T}$ ${\displaystyle t_{2}}$ ${\displaystyle t_{2}\in T}$ ${\displaystyle \dots }$ ${\displaystyle t_{k}}$ ${\displaystyle t_{k}\in T}$
• Zero-place relation symbols (logical constants), if permitted.

Expressions (or formulas) in general are defined recursively in multisort logic as follows:

• Every atomic expression is an expression.
• Are and expressions, so too are , , , expressions. ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle (\varphi \land \psi )}$ ${\displaystyle (\varphi \lor \psi )}$ ${\displaystyle (\varphi \rightarrow \psi )}$ ${\displaystyle (\varphi \leftrightarrow \psi )}$
• ${\displaystyle (\exists x:s\ \varphi )}$and are expressions if there is a species, a variable symbol, and an expression in which the local variable of the species occurs. ${\displaystyle (\forall x:s\ \varphi )}$ ${\displaystyle s\in T}$ ${\displaystyle x\in {\mathcal {V}}}$ ${\displaystyle \varphi }$ ${\displaystyle x}$ ${\displaystyle s}$

annotation

Relations can be understood as predicates, ie as (Boolean) functions with the same arity and argument type as well as the value range , i. H. the type of image (see relation, § relations and functions ). If the joiners are understood as symbols for one- and two-digit Boolean functions (in prefix or infix notation), then expressions - apart from those with quantifiers - are quasi 'terms of the kind '. ${\displaystyle \{\operatorname {falsch} ,\operatorname {wahr} \}}$ ${\displaystyle \operatorname {logical} }$ ${\displaystyle \operatorname {logical} }$

interpretation

Semantics of a versatile signature

${\displaystyle {\boldsymbol {S}}:=(T,{\mathcal {S}},\tau )}$be a multi-faceted signature with the set of function symbols (constants as zero-digit functions) and the set of relational symbols (possibly also zero-digit, i.e. logical constants). Be  and a figure with the following stipulations: ${\displaystyle {\mathcal {F}}_{0}}$ ${\displaystyle {\mathcal {R}}_{0}}$
${\displaystyle {\boldsymbol {A}}:=\{A_{s}|s\in T\}\cup \textstyle \bigcup _{t\in T^{*}}{\mathcal {P}}(\textstyle \prod A\circ t)}$ ${\displaystyle \alpha }$

• ${\displaystyle \alpha (s)=A_{s}}$be a range of values for each variety ( basic set ) ${\displaystyle s\in T}$
• ${\displaystyle \alpha (R)\subseteq A_{\tau (R)_{1}}\times \cdots A_{\tau (R)_{\sigma (R)}}}$a relation for each , and ${\displaystyle R\in {\mathcal {R}}_{0}}$
• ${\displaystyle \alpha (f):A_{\tau (f)_{1}}\times \cdots A_{\tau (f)_{\sigma (f)}}\to A_{\tau (f)_{\sigma (f)+1}}}$a function (link) for each . ${\displaystyle f\in {\mathcal {F}}_{0}}$

Then one calls an interpretation function and a multifaceted structure of the signature or structure . ${\displaystyle \alpha }$ ${\displaystyle {\mathcal {A}}:=((A_{s})_{s\in T},\alpha |_{{\mathcal {F}}_{0}}\cup \alpha |_{{\mathcal {R}}_{0}})=(\alpha |_{T},\alpha |_{{\mathcal {F}}_{0}}\cup \alpha |_{{\mathcal {R}}_{0}})}$ ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle {\boldsymbol {S}}}$

Overload

In the case of overload, uniqueness is established by specifying the argument type for the relation or function symbol:

${\displaystyle \alpha _{\boldsymbol {s}}(R)\subseteq A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}}$,

${\displaystyle \alpha _{\boldsymbol {s}}(f):A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}\to A_{s'}}$.

The arity here is given by the (word) length of the argument type , and is the type of image clearly determined by the argument type. It is a question of partial mappings, only for types with or can there be any assignment of symbols to relations or functions given. ${\displaystyle n}$ ${\displaystyle n=|{\boldsymbol {s}}|}$ ${\displaystyle {\boldsymbol {s}}}$ ${\displaystyle s'}$ ${\displaystyle s'=\tau (f)_{n+1}.}$
${\displaystyle {\boldsymbol {s}}}$ ${\displaystyle {\boldsymbol {\mathcal {R}}}_{t}\neq \emptyset }$ ${\displaystyle {\boldsymbol {\mathcal {F}}}_{t}\neq \emptyset }$

interpretation

A (possibly only partial) image on the variables declared out to elements of the associated species (i. E. From the value range ) mapping, i.e. a occupancy of vielsortigen structure . ${\displaystyle \beta }$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle x}$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle \nu _{x}=\nu (x)}$ ${\displaystyle A_{\nu _{x}}}$ ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle {\mathcal {A}}}$

The components are now required to interpret the signature . ${\displaystyle {\boldsymbol {I}}}$ ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle T,{\mathcal {A}},\nu ,\beta }$

With an existing interpretation and variable allocation (which may require a variable declaration ), the type and value of the terms can then be determined (see term, § Term Evaluation ), and the validity of logical expressions can be assessed (see Term, § Validity of expressions ).

Term evaluation and validity of expressions (formulas)

• For the evaluation of non-logical terms see main article Term, § Term evaluation ,
• for the validity of logical expressions (formulas) see main article Term, § Validity of expressions .

Ordered logic

In order sorted logic (English: order-sorted logic ) are the varieties associated value ranges as opposed to vielsortigen logic not necessarily disjoint . Instead, the set of sorts is given a partial order so that the following applies to all sorts : if , then . This declares the variety to be a sub-variety of the variety ( upper variety ). This logic is the basis of the inheritance of classes ( class hierarchy ) in object-oriented programming. ${\displaystyle s\in T}$ ${\displaystyle A_{s}}$ ${\displaystyle T}$ ${\displaystyle \preceq }$ ${\displaystyle s_{1},s_{2}}$ ${\displaystyle s_{1}\preceq s_{2}}$ ${\displaystyle A_{s_{1}}\subseteq A_{s_{2}}}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{2}}$

Ordered logic can be converted into ordinary single-order logic like multi-layered logic. The variety is again translated into a single-digit predicate , and an axiom is added for each sub-variety relationship . ${\displaystyle t:s}$ ${\displaystyle P_{s}(t)}$ ${\displaystyle s\preceq s'}$ ${\displaystyle \forall x:(P_{s}(t)\to P_{s'}(t))}$

The opposite approach was successful in an automated theorem proof: in 1985 Christoph Walther was able to solve a benchmark problem by formulating it in orderly logic and thereby reducing the effort by orders of magnitude, since many single-digit predicates became sorting.

Examples

• In the example above it would be about

${\displaystyle {\textit {Hund}}\ \preceq \ {\textit {Fleischfresser}}}$,

${\displaystyle {\textit {Hund}}\ \preceq \ {\textit {Wirbeltier}}}$,

${\displaystyle {\textit {Raubtier}}\ \preceq \ {\textit {Tier}}}$,

${\displaystyle {\textit {Wirbeltier}}\ \preceq \ {\textit {Tier}}}$,

${\displaystyle {\textit {Tier}}\ \preceq \ {\textit {Organismus}}}$,

${\displaystyle {\textit {Buche}}\ \preceq \ {\textit {Pflanze}}}$,

${\displaystyle {\textit {Pflanze}}\ \preceq \ {\textit {Organismus}}}$,

and so on.

• Modeling the relationships in the number ranges:

${\displaystyle \mathbb {Z} }$( whole numbers ) ( rational numbers ) ( real numbers ) ( complex numbers ) ( quaternions ) ( octonions ) ( sedenions ), ${\displaystyle \subseteq \mathbb {Q} }$ ${\displaystyle \subseteq \mathbb {R} }$ ${\displaystyle \subseteq \mathbb {C} }$ ${\displaystyle \subseteq \mathbb {H} }$ ${\displaystyle \subseteq \mathbb {O} }$ ${\displaystyle \subseteq \mathbb {S} }$

${\displaystyle \mathbb {Q} \subseteq \mathbb {A} }$( algebraic numbers ) . ${\displaystyle \subseteq \mathbb {C} }$

• In some programming languages ​​(such as Pascal and Modula-2 ), integer intervals are used as data types: Be with , then applies to the interval data type The (unchecked) assignment of any integer values ​​to this data type can be classified as syntactically incorrect. ${\displaystyle m,n\in \mathbb {Z} }$ ${\displaystyle m\leq n}$ ${\displaystyle m.\!.n\preceq \operatorname {int} }$

• A special situation arises when the variety overlaps with other varieties. The truth values and can be interpreted as 0 to 1. Then these are available for relations like and functions (links) like and . One example of this in information technology is C-Language . In an extension, the logical values ​​of a three-valued logic or simple fuzzy logic could be equated with numbers from the real interval , so that the following applies in all cases: ${\displaystyle \operatorname {logical} }$ ${\displaystyle \operatorname {false} }$ ${\displaystyle \operatorname {true} }$ ${\displaystyle \leq }$ ${\displaystyle +,-,\cdot }$ ${\displaystyle /}$ ${\displaystyle [0,1]}$ ${\displaystyle \operatorname {logical} \preceq \operatorname {real} }$

method

A sort structure is then generated with an order- oriented signature that has been expanded again , for example examples of order-sorted structures in mathematics ${\displaystyle (T,\preceq )}$ ${\displaystyle (T,\preceq ,\tau |_{{\mathcal {F}}_{0}},\tau |_{{\mathcal {R}}_{0}})}$

• ${\displaystyle \mathbb {Q} }$, , And as a commutative and associative algebras over the ring of integers (d. H as special. - modules ), as subset of these number ranges, ${\displaystyle \mathbb {A} }$ ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {C} }$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle \mathbb {Z} }$
• ${\displaystyle \mathbb {R} }$as infinite-dimensional associative and commutative algebra over the field of rational numbers (i.e. as a special vector space with a Hamel basis ), since , ${\displaystyle \mathbb {Q} }$ ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {Q} \subseteq \mathbb {R} }$
• ${\displaystyle \mathbb {C} }$as two-dimensional associative and commutative algebra over the field (i.e. as a special vector space), since ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {R} \subseteq \mathbb {C} }$
• Another example is the different areas of hyper- complex numbers , such as the quaternions (or octonions or sedenions ), for example as four-dimensional associative non-commutative algebra (or eight- or 16-dimensional non-associative non-commutative algebra) over the body , which, as with, is a subset. ${\displaystyle \mathbb {H} }$ ${\displaystyle \mathbb {O} }$ ${\displaystyle \mathbb {S} }$ ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {C} }$

The partial order is canonically continued as follows: ${\displaystyle \preceq }$ ${\displaystyle T^{*}}$

${\displaystyle {\boldsymbol {s}}_{1}{\boldsymbol {\preceq }}{\boldsymbol {s}}_{2}}$ exactly when

• ${\displaystyle {\boldsymbol {s}}_{1}}$and have the same arity (i.e. tuple or word length), here denoted by ${\displaystyle {\boldsymbol {s}}_{2}}$ ${\displaystyle k}$
• for all true ${\displaystyle i=1\dots {k}}$ ${\displaystyle {\boldsymbol {s}}_{1_{i}}\preceq {\boldsymbol {s}}_{2_{i}}}$

Regular signature

An order-oriented signature is called regular if and only if for each function symbol and each the set ${\displaystyle f\in {\mathcal {F}}_{0}}$ ${\displaystyle {\boldsymbol {w}}\in T^{*}}$

${\displaystyle \{s'\in T|\exists {\boldsymbol {s}}\in T^{*}\ \textstyle {mit}\ {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}:\tau (f)=({\boldsymbol {s}},s')\}=\{s\in T|\exists {\boldsymbol {s}}\in T^{*}\ \textstyle {mit}\ {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}:\ \;f:{\boldsymbol {s}}\longrightarrow s'\}}$

is empty or has a clearly defined smallest element.

Acceptable signature

A regular signature is allowed if the following conditions are met:

• If for and with applies , then also applies ${\displaystyle f:{\boldsymbol {s}}\longrightarrow s'}$ ${\displaystyle f:{\boldsymbol {w}}\longrightarrow w'}$ ${\displaystyle {\boldsymbol {s}},{\boldsymbol {w}}\in T^{*},s',w'\in T}$ ${\displaystyle {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}}$ ${\displaystyle w\preceq s}$
• There cannot be infinite chains . If the types and symbols are finite ( finite signature ), this is always guaranteed. ${\displaystyle \dots s_{3}\preceq s_{2}\preceq s_{1}}$
• Down completeness : When two varieties common sub-types have, then there is a greatest common sub-locations (GGU, Eng .: greatest common subset ) in character . If necessary, however, a suitable new variety can be added to the variety alphabet so that it is then fulfilled. At the object level, the condition says nothing else than that the intersection of two value ranges and (as the largest common subset) is either empty or must be a value range of a suitable type . In order to integrate ordered logic into a sentence-based automatic theorem prover, a corresponding ordered unification algorithm is necessary. This requires that for two declared varieties whose GGU except Disjointness also stated member of the Variety amount is ${\displaystyle s_{1},s_{2}\in T}$ ${\displaystyle \operatorname {gcs} (s_{1},s_{2})}$ ${\displaystyle r}$ ${\displaystyle T}$ ${\displaystyle r=\operatorname {gcs} (s_{1},s_{2})}$ ${\displaystyle A_{s_{1}}}$ ${\displaystyle A_{s_{2}}}$ ${\displaystyle r\in T}$
  ${\displaystyle s_{1},s_{2}\in T}$ ${\displaystyle \operatorname {gcs} (s_{1},s_{2})}$ ${\displaystyle T}$
• For all of the amount is ${\displaystyle s\in T,{\boldsymbol {w}}\in T^{*},f\in {\mathcal {F}}_{0}}$ ${\displaystyle f:{\boldsymbol {w}}'\longrightarrow s'}$

  ${\displaystyle \{{\boldsymbol {v}}\in T^{*}|\exists {\boldsymbol {v}}'\in T^{*},r\in T:f:{\boldsymbol {v}}'\longrightarrow r,r\preceq s,{\boldsymbol {v}},{\boldsymbol {\preceq }}w,{\boldsymbol {v}}{\boldsymbol {\preceq }}{\boldsymbol {v}}'\}}$

either empty or has a largest element. The combination of this requirement with downward completeness is called downward uniqueness .

For practical reasons, overloading is the norm. Otherwise, all function and relation symbols would have to be different for each number range . B. keep it as an index. The numerical ranges by the complex-algebraic numbers and the chains and also constitute an example of (lack of) downward completeness: two As intersection varieties value ranges are the real-algrbraischen numbers a lot with missing variety characters, which the entirety would nachzutragen sake. ${\displaystyle +,-,\cdot ,/,\leq ,\dots }$ ${\displaystyle \mathbb {N} ,\mathbb {Z} ,\mathbb {Q} ,\mathbb {R} \mathbb {A} ,\mathbb {C} }$ ${\displaystyle \mathbb {C} ,\mathbb {A} ,\mathbb {R} ,\mathbb {Q} }$ ${\displaystyle \mathbb {A} }$ ${\displaystyle \mathbb {Q} \subseteq \mathbb {R} \subseteq \mathbb {C} }$ ${\displaystyle \mathbb {Q} \subseteq \mathbb {A} \subseteq \mathbb {C} }$ ${\displaystyle \mathbb {A} \cap \mathbb {R} }$

Variables in orderly logic

As with the multi-faceted logic, there is the option of assigning the variables in quantities with a fixed variety, or of subsequently defining the variety by means of a declaration that can be modified locally . ${\displaystyle \nu :{\mathcal {V}}\to T}$

Term evaluation in orderly logic

The term analysis based on the variable declaration and type of functions (including the constants) assigns the terms depending on the signature and the variable declaration recursively as far as possible a variety quantity (overloading!) And a value to. ${\displaystyle t}$ ${\displaystyle {\mathcal {S}}(t)}$ ${\displaystyle [\![t]\!]}$

• for variables : (above set of ) ${\displaystyle v\in {\mathcal {V}}}$ ${\displaystyle {\mathcal {S}}(v)=\{r\in T|\nu (v)\preceq r\}}$ ${\displaystyle \nu (v)}$
• for constants : ${\displaystyle c}$ ${\displaystyle {\mathcal {S}}(c)=\{r\in T|\tau (c)\preceq r\}}$
• for functions : ${\displaystyle f}$ ${\displaystyle {\mathcal {S}}(f)=\{({\boldsymbol {r}},r')\in T^{+}|\exists {\boldsymbol {s}}\in T^{*},s'\in T:f:{\boldsymbol {s}}\longrightarrow s'\land {\boldsymbol {s}}{\boldsymbol {\preceq }}{\boldsymbol {r}}\land s'\preceq r'\}}$

example

If and are variables of type or , then the equation has the solution , where holds. ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{2}}$ ${\displaystyle x_{1}=x_{2}}$ ${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$ ${\displaystyle x:\operatorname {gcs} (s_{1},s_{2})}$

Extensions

Gert Smolka generalized the ordered logic to allow parametric polymorphism (English parametric polymorphism ). In his work, sub-species relationships are further developed into complex type expressions. In a programming example, a parameterized type can be declared (where > is a type parameter like in a C ++ template ). The relation can be derived automatically from the subtype relation , which means that every list of integers is also a list of floating point numbers ( ). ${\displaystyle {\textit {list}}(X)}$ ${\displaystyle X}$ ${\displaystyle {\textit {int}}\subseteq {\textit {float}}}$ ${\displaystyle {\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})}$ ${\displaystyle {\textit {float}}}$

Schmidt-Schauß generalized the ordered logic to allow term declarations. For example, the sub-sort relationships and allow a term declaration to be explained as a property of integer addition that cannot be expressed with ordinary overload. ${\displaystyle {\textit {even}}\preceq {\textit {int}}}$ ${\displaystyle {\textit {odd}}\preceq {\textit {int}}}$ ${\displaystyle \forall i:{\textit {int}}.\;(i+i):{\textit {even}}}$

Finally, the ordered logic can be expanded in the direction of feature logic . The arguments of functions and relations are given names (instead of or in addition to the position number). This allows keyword parameters to be used in addition to or instead of the usual positional parameters. On the one hand, the method is widespread in information technology, but on the other hand it opens up theoretical connections with dependency grammars .

See also

• Signature (model theory)
• Term evaluation and validity of expressions (formulas)

literature

• Wolfgang Bible, Steffen Hölldobler, Torsten Schaub: Knowledge representation and inference. A basic introduction . Springer-Verlag, 2013, ISBN 3-322-86814-1 , p. 99-100 ( books.google.de ).
• François Bry: Excursus: First-order multi-varietal predicate logic . tape 2.9 . LMU, Institute for Computer Science, teaching and research unit for programming and modeling languages ​​(pms), Munich 1999 ( en.pms.ifi.lmu.de ).
• François Bry: Excursus: Second order predicate logic . tape 2.10 . LMU, Institute for Computer Science, teaching and research unit for programming and modeling languages ​​(pms), Munich 1999 ( en.pms.ifi.lmu.de ).
• PC Gilmore: An addition to “Logic of many-sorted theories” . (PDF) In: Compositio Mathematica . 13, 1958, pp. 277-281.
• Klaus Gloede: Script for the lecture set theory . SS 2004. University of Heidelberg, Mathematical Institute, p. 181 . PDF , At DOCZZ , At Yumpu
• Hartwig, R .: Syntax Semantics Specification. Basics of computer science . WS 2009/2010. University of Leipzig, Institute for Computer Science, Leipzig, p. 219 ( informatik.uni-leipzig.de [PDF]).
• M. Huber, I. Varšek: Extended Prolog with Order-Sorted Resolution.4th IEEE Symposium of Logic Programming . San Francisco 1987, p. 34-45 .
• H. Kleine Büning ,: sorts and terms. Winter semester 2015 . Mod. 05 part 1. University of Paderborn, 2015, p. 15 .
• Letz, Reinhold: Predicate logic . WS 2004/2005. Technical University of Munich, Faculty of Computer Science, Chair of Computer Science IV, Munich, p. 47 ( tcs.ifi.lmu.de [PDF]).
• Lutz, Carsten: Logic part 4: Second level predicate logic . University of Bremen, AG Theory of Artificial Intelligence, 2010, p. 65 ( informatik.uni-bremen.de [PDF] lecture in the winter semester 2010).
• Arnold Oberschelp : Investigations into multi-varietal quantifier logic, number 4 . In: Mathematical Annals . 145, 1962, pp. 297-333. ISSN  0025-5831 ; 1432-1807 / e. doi : 10.1007 / bf01396685 .
• Oberschelp, Arnold: Order Sorted Predicate Logic. Lecture Notes in Computer Science (LNCS) . Ed .: Bläsius, Karl Hans; Hedtstück, Ulrich; Rollinger, Claus-Rainer. tape 418 : Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24-26, 1989 Proceedings . Springer-Verlag, Berlin / Heidelberg 1990, ISBN 978-3-540-52337-6 , p. 307 , doi : 10.1007 / 3-540-52337-6 .
• Pelletier, F. Jeffry: Sortal Quantification and Restricted Quantification . (PDF) In: Philosophical Studies . 23, 1972, pp. 400-404. doi : 10.1007 / bf00355532 .
• Esther Ramharter, Günther Eder: Second level predicate logic . In: Memo Seki-85-11-KL . University of Kaiserslautern, Department of Computer Science, 1985 ( homepage.univie.ac.at [PDF]).
• Schmidt-Schauß, Manfred: A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. SE modal logic and other philosophically relevant logics . WS 2015/2016. University of Vienna, S. 22 .
• Walther, Christoph: A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution . In: Artif. Intelligent . 26 (2), 1985, pp. 217-224. doi : 10.1016 / 0004-3702 (85) 90029-3 .
• Walther, Christoph: A Many-Sorted Calculus Based on Resolution and Paramodulation . In: Research Notes in Artificial Intelligence . Pitman, London 1987.
• Wang, Hao: Logic of many-sorted theories . In: Journal of Symbolic Logic . 17, 1952, pp. 105-116. doi : 10.2307 / 2266241 . , Part of the Computation, Logic, Philosophy collection. A Collection of Essays , Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.

References and comments

1. ↑ For more details see A. Oberschelp (1962) p. 297f
2. ↑ For example, errors in data type assignments can be recognized quickly (at compile time ) as system errors.
3. ↑ is interpreted as an alphabet of variety designators, see alphabet (computer science) and alphabet (mathematics) ${\displaystyle T}$
4. ↑ Carlos Caleiro, Ricardo Gonçalves: On the algebraization of many-sorted logics . In: Proc. 18th int. Conf. on Recent trends in algebraic development techniques (WADT) . Springer, 2006, ISBN 978-3-540-71997-7 , pp. 21-36.
5. ↑ In this context, sorting is understood to mean the assignment to varieties, see Steimann (1991) p. 3
6. ↑ with the special case of Euclidean space
7. ↑ Note: Kruse, Borgelt (2008) p. 3 and p. 9 denote
   • the set of varieties with and the varieties themselves with , ${\displaystyle T}$ ${\displaystyle \Theta }$ ${\displaystyle A,B,\dots }$
   • the restriction of to the function symbols with (a set of ordered pairs), ${\displaystyle \tau |_{{\mathcal {F}}_{0}}}$ ${\displaystyle \tau }$ ${\displaystyle \Delta }$
   • the restriction of to the relation symbols with , ${\displaystyle \tau |_{{\mathcal {R}}_{0}}}$ ${\displaystyle \tau }$ ${\displaystyle \Pi }$
   • the variable declaration with (more precisely, the authors use a dot notation , with the dot as an additional technical character. The variables are only used in the form with the actual variable name x and a variety s . Variables in the sense used in the article here with quantity designation then the combinations, ie strings with an implicit variable declaration are used. This means that the raw name x can be used for several types), ${\displaystyle \nu }$ ${\displaystyle \Omega }$ ${\displaystyle x.s}$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle x.s}$ ${\displaystyle \beta (x.s)=s}$
   • the signature with what corresponds to the text above , ${\displaystyle \Sigma =(\Theta ,\Delta ,\Pi )}$ ${\displaystyle (T,\tau |_{{\mathcal {F}}_{0}},\tau |_{{\mathcal {R}}_{0}})}$
   • the figure (characteristic of the structure) with , and ${\displaystyle \alpha }$ ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle I}$
   • the variable assignment with . ${\displaystyle \nu }$ ${\displaystyle \beta }$
8. ↑ . In the case of the function symbols, where at least one type is required for the range of values, the values ​​of lie in the positive envelope . Arity is the word length of the type (minus 1 for function symbols). ${\displaystyle T^{*}=\bigcup \{T^{n}|n\in \mathbb {N} _{0}\}}$ ${\displaystyle \tau }$ ${\displaystyle T^{+}=T^{*}\setminus \{\emptyset \}=T^{*}\setminus \epsilon }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$
9. ↑ with the empty Cartesian set product consisting of the empty word (set-theoretically identical to the empty set ): ${\displaystyle T^{0}=\{\emptyset \}=\{\epsilon \}}$
10. ^ ^{A b c d e f g} Brass, Stefan: Mathematical logic with database applications . Martin Luther University Halle-Wittenberg, Institute for Computer Science, Halle 2005, p. 176 ( informatik.uni-halle.de [PDF]).
11. ↑ The two families are defined analogous to the one-sorted case as the archetype of fibers of the limitations of the two symbol sets and : ${\displaystyle \alpha }$ ${\displaystyle {\mathcal {R}}_{0}}$ ${\displaystyle {\mathcal {F}}_{0}}$ ${\displaystyle {\boldsymbol {\mathcal {R}}}_{s}=(\alpha |_{{\mathcal {R}}_{0}})^{-1}(\{s\}),\;{\boldsymbol {\mathcal {F}}}_{s,s'}=(\alpha |_{{\mathcal {F}}_{0}})^{-1}(\{(s,s')\})}$
12. ↑ Stefan Brass 2005 pp. 16-19. The author uses bundles of fibers and sometimes slightly different designations to identify the signature, in particular the variety alphabet is designated with instead . ${\displaystyle {\mathcal {S}}}$ ${\displaystyle T}$
13. ↑ ^{a b c d e f g h} Steimann, Friedrich: Ordered feature logic and dependency grammars in computational linguistics . Monographs. FernUni, Faculty of Mathematics and Computer Science, LG Programming Systems, Hagen January 31, 2011, p. 104 ( fernuni-hagen.de - diploma thesis). , at: fernuni-hagen.de (PDF). Original at: Universität Karlsruhe 1992, Institute for Logic, Complexity and Inference Systems. Over and above the topic, the author describes a first-level feature logic in order , i.e. H. Arguments have names and can be referenced as keyword parameters.
14. ↑ see also correspondence
15. ↑ A. Oberschelp (1989/1990) page 10
16. ↑ that is then also the kind of logical constants as zero-digit relations.
17. ↑ Relations can therefore be understood as special functions, conversely, functions are special (left-total-right-unambiguous) relations .
18. ↑ For used here Maplet notation (instead of the slash used by Stefan Brass or ) see Klaus Grue (1995) p. 11 ${\displaystyle \nu _{\langle x\mapsto s\rangle }}$ ${\displaystyle \nu \langle {x/s}\rangle }$ ${\displaystyle \nu {\frac {s}{x}}}$
19. ↑ A. Oberschelp (1989/1990) page 9ff
20. ↑ F. Bry (1999 / 2.10) Def. 2.10.1
21. ↑ C. Lutz (2010) pp. 6 and 8
22. ↑ Ramharter, Eder (2015/16) p. 17. The authors mark the arity of the relation variables with an index.
23. ↑ ^{a b} Grädel, Erich: Mathematical logic . Mathematical basics of computer science. SS 2009. RWTH, Aachen, S. 129 ( cs.uni-dortmund.de [PDF]).
24. ↑ ^{a b} Kruse, Stefan; Borgelt, C .: Basic Concepts of Predicate Logic . Computational Intelligence. Otto von Guericke University, Magdeburg 2008, p. 14 ( fuzzy.cs.ovgu.de [PDF]).
25. ↑ Kleine Büning (2015), p. 5 ff
26. ↑ Detailed description: Kleine Büning (2015), pp. 8–15.
27. ↑ D. h. In the scope (scope) of the respective quantifier, a locally modified variable declaration (also called ( -) variant ${\displaystyle x}$ ) applies with any and ${\displaystyle \nu '=\nu _{\langle x\mapsto s\rangle }}$ ${\displaystyle x\in {\mathcal {V}},s\in T}$

    ${\displaystyle \nu '(y)=\nu _{\langle x\mapsto s\rangle }(y):={\begin{cases}s&{\text{wenn}}\ y=x,\\\nu (y)&{\text{sonst (auf dem ursprünglichen Definitionsbereich von}}\ \nu {\text{)}};\end{cases}}}$

    See Stefan Brass (2005) p. 56, as well as Ramharter, Eder (2015/16) p. 17. In the event that it is already declared outside of the quantifiers, i. H. if the declaration is already in the original definition area , it is overwritten locally. A variable in the scope of a quantifier (like here ) is called a bound variable. ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle \nu }$ ${\displaystyle x}$
28. ↑ with ( family notation ), wherein (word or tuple's length of ). ${\displaystyle A\circ t=(A_{t_{i}})_{i\in \{1\dots n\}}}$ ${\displaystyle \textstyle \prod A\circ t=\textstyle \prod _{i\in \{1\dots n\}}A_{t_{i}}}$ ${\displaystyle n:=|t|}$ ${\displaystyle t}$
29. ↑ See Stefan Brass (2005), p. 29; the author uses the notation instead . as in the single-variety case, denotes the arity of , here given by the (word) length of the type . Simplified: without overloading. ${\displaystyle {\mathcal {I}}}$ ${\displaystyle \alpha }$ ${\displaystyle \sigma (R)}$ ${\displaystyle R}$ ${\displaystyle \tau (R)}$
30. ↑ Constants are understood here as zero-digit functions. Otherwise, another part would be added to the range of values (this corresponds to the single-variety case). ${\displaystyle {\boldsymbol {A}}}$ ${\displaystyle \alpha }$ ${\displaystyle \textstyle \bigcup _{s\in T}A_{s}}$ ${\displaystyle A}$
31. ↑ In fact, because of the disjointness of , and is irrelevant whether you separate the individual sections with commas or . A tuple of families with disjoint index sets is isomorphic to a family with the united index set. In this sense the structure is identical to the interpretation function (family) or with, except for isomorphism . See also restriction, § compatibility rules . ${\displaystyle T}$ ${\displaystyle {\mathcal {F}}_{0}}$ ${\displaystyle {\mathcal {R}}_{0}}$ ${\displaystyle \cup }$ ${\displaystyle {\boldsymbol {S}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle \alpha }$ ${\displaystyle (\alpha |_{T},\alpha |_{{\mathcal {F}}_{0}},\alpha |_{{\mathcal {R}}_{0}})}$
32. ↑ If the variables that are assigned to a variety according to the declaration are designated with (= original fiber from below ), then the restriction of the assignment to these variables is a (possibly partial) mapping ${\displaystyle \nu }$ ${\displaystyle s\in T}$ ${\displaystyle {\mathcal {V}}_{\nu ,s}}$ ${\displaystyle s}$ ${\displaystyle \nu }$ ${\displaystyle \beta }$ ${\displaystyle {\mathcal {V}}_{\nu ,s}\not \to A_{s}}$
33. ↑ alternative names: , ${\displaystyle \subseteq }$ ${\displaystyle \sqsubseteq }$
34. ↑ A. Oberschelp (1989) page 11ff .
35. ↑ Christoph Walter (1985)
36. ↑ int stands for integer, value range is for simple . See sequence, § Formal definition : finite sequences. ${\displaystyle \langle m,n\rangle =\{m,m+1,\dots n-1,n\}}$ ${\displaystyle n=m}$ ${\displaystyle \{m\}}$
37. ↑ Conversely, in the if query in C, every argument not equal to 0 is evaluated as true, and only 0 as false.
38. ↑ A. Oberschelp (1989/1990) page 11ff
39. ↑ Steimann 1992, p. 5. The author describes the sort alphabet as with partial order , the set of symbols with and the ordered signature with accordingly ${\displaystyle \operatorname {S} }$ ${\displaystyle \leq }$ ${\displaystyle \Sigma }$ ${\displaystyle (\operatorname {S} ,\leq ,\Sigma ).}$
40. ↑ Gloede, Set Theory, 2004
41. ↑ or , ${\displaystyle s_{1}\cap s_{2}}$ ${\displaystyle s_{1}\sqcap s_{2}}$
42. ↑ d. H. if there is no overload ${\displaystyle ({\boldsymbol {w}}',s'):=\tau (f)}$
43. ↑ Oberschelp 1989/90 p. 14 f
44. ↑ Smolka, Gert: Logic Programming over Polymorphically Order-Sorted Types . University of Kaiserslautern, May 1989.
45. ^ Schmidt-Schauß, Manfred: Computational Aspects of an Order-Sorted Logic with Term Declarations  (= LNAI), Volume 395.Springer, April 1988.
46. ↑ See parameters, § Different parameter terms