Signature (model theory)
In mathematical logic , a signature consists of the set of symbols that are added to the usual, purely logical symbols in the language under consideration , and a mapping that uniquely assigns an arity to each symbol of the signature . While the logical symbols are always interpreted as “for all”, “there is a”, “and”, “or”, “follows”, “equivalent to” or “not”, the semantic interpretation of the symbols allows the Signature different structures (in particular models of statements of logic) can be distinguished. The signature is the specific part of an elementary language .
For example, the entire ZermeloFraenkel set theory can be formulated in the language of firstorder predicate logic and the single symbol (in addition to the purely logical symbols); in this case the symbol set of the signature is the same .
motivation
If statements about a certain area are to be formalized, it must first be decided about which objects and which relationships statements are to be made. A constant is introduced for every nameable object and a relation symbol for every relationship . For example, to talk about the arrangement of natural numbers, a constant is introduced for each number and relational symbols (less than) and (greater than).
In most cases you also need functions that you can use to calculate using the constants, e.g. B. a symbol for the addition of natural numbers.
There are thus three types of symbols that can appear in signatures:
 Constant symbols : They stand for exactly one value.
 Function symbols : They each stand for a clear assignment of values to others.
 Relation symbols (predicates) : They each stand for a relationship, i.e. for an assignment of values to one another, which does not have to be unique. A relationship is often expressed as the subset of all tuples for which the predicate applies.
Classification and demarcation
The signature does not include variable symbols , the value of which is not interpreted in the formula, and other symbols that are used to build a statement or formula. All these characters together form the "elementary language" generated by the signature. A language therefore comprises more characters than the associated signature
The characters allowed for the formation of logical statements and formulas can thus be roughly divided into
 Characters that define the structure (composition) of the statement or formula:
 Juncture symbols , for example
 Quantifier symbols , for example
 Terminal signs that stand for values and their relationships:
 Variables , for example

Symbols of the signature
 Constant symbols , for example
 Function symbols, for example
 Relation symbols (predicates), for example
 Technical signs
 Outlines, like the brackets
 others, like (comma)
Some authors do without some of the joiners and quantifiers, e.g. B. can be explained with the help of the other of these signs. Taking advantage of duality can (or vice versa ) be omitted.
Terms do not belong to the signature, but these are built up from the logical symbols, the variables and the function and constant symbols of the signature and from variables according to fixed formation rules.
If terms are used as arguments in the relation symbols, atomic statements of the predicate logic arise . Comparisons of terms are also considered atomic statements in predicate logic. From them, combined statements can be formed through links (connectors and quantifiers), see firstlevel predicate logic §Expressions .
definition
Let and be pairwise disjoint sets of nonlogical signs. Then called each character in a symbol and a symbol set when by mapping each character in the following one arity called number is clearly assigned:
 for all
 for everyone and
 for all
is then called a signature and each is referred to as a constant symbol , each as a function symbol and each as a relation symbol .
A signature is called finite if there is a finite set . If a signature has no relational symbols, it is called an algebraic signature , whereas if it has no constant and no function symbols, it is called a relational signature .
Remarks
 The constant symbols can also be counted among the function symbols, so that results with .
 Occasionally, symbols for zerodigit relationships are also permitted; these correspond to propositional (Boolean) constants (see Relations §Relations and Functions and Brass (2005), p. 19). Mirt the amount of these symbols widens to and the complete set of symbols is then .
 Some authors consider instead of the illustration that assigns its arity to each symbol, its archetype fibers , specifically the sequences and that assign the relational or functional symbols of the arity concerned to each natural number. To identify the signature, it is sufficient to specify these two sequences .
 The same relation symbol can be used for relations of different arity, and the same function symbol can be used for functions of different arity. The symbol is then called overloaded or polymorphic . The sets of relation symbols for the various arithmetic units n on the one hand and the sets of function symbols on the other hand are then no longer necessarily disjoint from one another , but the set of all relation symbols is still disjoint from that of all function symbols . In this case, the arity mapping is a multifunction ( instead of ); however, the restrictions to a certain arity ( ) are clear. An example are the functions max and min, which are each defined for all n tuples with as arguments, i.e. H. ; and LCM , GCD : .
 In the literature, a distinction is often not made between a signature and its set of symbols; the arithmetic mapping is then not specified as such.
Semantics of a signature
Structures
Let be a signature and let the set consist of all constant symbols, the set consist of all function symbols and the set of all relation symbols. Furthermore, denote a nonempty set and . Then is a figure so that
this is what one calls an interpretation function and a structure of the signature or, for short, a structure . One then also finds the ways of naming . if the basic set , the carrier set or, in short, the carrier of If is a finite set, then it is also called finite , otherwise infinite .
Remarks
 A constant can be understood as the zerodigit function such that :
 with functions and with relations
 Every digit function is always a digit relation (with the function value in the last position). Therefore, any structure can be represented as
 with relations
 If a structure only contains functions ( algebraic structure ) or only relations ( relational structure , in particular order structure ), then it often has special properties.
 The definition can be extended to partial functions to e.g. B. to capture partial algebras .
 If the relation and / or function symbols are overloaded, clarity is established by specifying the arity for the respective symbol:
 and
 .
 These are partial mappings, only for arithmetic or there can be assignments of symbols to relations or functions.
Interpretations
The signature is given a certain semantic meaning through a structure and an interpretation or interpretation of variables :
Let be the set of variable symbols. A variable assignment is then a (possibly only partial ) mapping . is called an assignment of the structure . is then called an interpretation of the signature or, for short, an interpretation .
Diverse signatures
For the description of diverse structures , such as B. heterogeneous algebras ( modules , vector spaces , Kalgebras , Liealgebras, etc.) with several carrier sets , one can introduce multisite or multi site signatures . In addition to the function and relation symbols, there are also types and descriptions for the carrier quantities. An nary relation is a subset of the nfold Cartesian product of a sequence of the carrier sets . The argument range of an nplace function is just such a product, plus one of the carrier sets for the value range.
Multivarietal can always be traced back to single varietal by adding the variety affiliation for each variety as a onedigit relation ( variety predicate ). In contrast to the secondorder predicate logic with relation variables, multivariate does not mean an increase in the power of the theory, for example with regard to questions of provability. For this it is sufficient to consider the single species case. Incorrect variety assignments (such as if and belong to different varieties, e.g. scalar and vector) then no longer appear as syntactic errors. Multisort structures form a settheoretical 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.
Among the amounts for the function and for the relation symbols yet another finite, nonempty comes varieties amount not logical character to. The signature of a function or relation symbol is no longer simply a number of arguments , but has to respect their types. The argument sorts therefore form n  tuples with arity n . The image type is also added for functions , so that an ( n + 1) tuple results overall . The tuples can be understood as words above the sort alphabet , i.e. H. as elements of the Kleene shell . They are called type referred to the relations or function icon: . The signature is then composed of the variety amount of the symbol amount and the type mapping together: .
literature
 HeinzDieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic . 3rd, completely revised u. exp. Edition. tape 1 : Fundamentals, Algebra and Geometry . Bibliographisches Institut, Mannheim u. a. 1992, ISBN 3411156031 , Chapter II: Syntax of First Level Languages, Chapter III: Semantics of First Level Languages.
 Walter Gellert, Herbert Küstner, Manfred Hellwich, Herbert Kästner (eds.): Small encyclopedia of mathematics . 10th (completely revised 2nd) edition. Harri Deutsch, Thun / Frankfurt a. M. 1984, ISBN 3871443239 , pp. 361363 .
 Philipp Rothmaler: Introduction to Model Theory . Spektrum Akademischer Verlag, 1995, ISBN 9783860254615 .
 Erich Grädel: Mathematical Logic . Mathematical Foundations of Computer Science, SS 2009. RWTH, Aachen, S. 129 ( flditwww.cs.unidortmund.de [PDF]).
 W. Vogler: Logic for computer scientists . WS 2007/2008. Univ. Augsburg, Institute for Computer Science, Augsburg, p. 49 ( informatik.uniaugsburg.de [PDF]).
 Uwe Kastens: Predicate logic . University of Paderborn, Institute for Computer Science, Paderborn 2008, p. 31 ( cs.unipaderborn.de [PDF]).
 Thomas Worsch: Predicate logic . Unit 18: Logic, WS 2008/2009. University of Karlsruhe, Faculty of Computer Science, Karlsruhe, S. 35 ( cs.unipaderborn.de [PDF]).
 Armin B. Cremers, Ulrike Griefahn, Ralf Hinze: Type systems. In: Deductive Databases. Artificial Intelligence . Vieweg + Teubner, Wiesbaden 1994, ISBN 9783528047009 , Chapter 5: Type systems, p. 147182 , doi : 10.1007 / 9783663095729_5 .
The multisite or multisite case is treated in the following sources:
 Arnold Oberschelp : Investigations into the multivariety quantifier logic . In: Mathematical Annals . tape 145 , no. 4 . Springer, 1962, p. 297333 , doi : 10.1007 / BF01396685 ( eudml.org ).
 Arnold Oberschelp; Ed .: Karl Hans Bläsius, Ulrich Hedtstück, ClausRainer Rollinger: Order Sorted Predicate Logic . Lecture Notes in Computer Science (LNCS), Volume 418 : Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 2426, 1989 Proceedings. SpringerVerlag, Berlin Heidelberg 1990, ISBN 9783540523376 , p. 307 , doi : 10.1007 / 3540523376 .
 François Bry: Excursus: Firstorder multivarietal predicate logic . tape 2.9 . LMU, Institute for Computer Science, pms, Munich 1999 ( en.pms.ifi.lmu.de ).
 Stefan Brass: Mathematical Logic with Database Applications . Martin Luther University HalleWittenberg, Institute for Computer Science, Halle 2005, p. 176 ( users.informatik.unihalle.de [PDF]).
 R. Kruse, C. Borgelt: Basic concepts of predicate logic . Computational Intelligence. Otto von Guericke University, Magdeburg 2008, p. 14 ( fuzzy.cs.ovgu.de [PDF]).
 R. Hartwig: Syntax Semantics Specification  Basics of Computer Science . WS 2009/2010. University of Leipzig, Institute for Computer Science, Leipzig, p. 219 ( informatik.unileipzig.de [PDF]).
 Reinhold Letz: 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]).
 Friedrich Steimann: 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 ( fernunihagen.de  diploma thesis). , at: FernUni Hagen, fernunihagen.de (PDF). Original at: Universität Karlsruhe 1992, Institute for Logic, Complexity and Inference Systems
References and comments
 ↑ The arguments of the relations and functions are positional parameters (also called positional parameters). Logics widely used in information technology, in which names are given to the arguments ( keyword parameters ), are called feature logics , see also: Parameters (computer science) §Different parameter terms and Steimann (1992), p. 4.
 ↑ See E. Grädel (2009) p. 45.
 ↑ see propositional logic §Buildings of propositional language
 ↑ For example Kruse, Borgelt (2008) p. 3
 ↑ See E. Grädel (2009) p. 45 f
 ↑ E. Grädel (2009) p. 46 f
 ↑ In the Englishlanguage literature there is also the designation (from arity , arity ) instead of .
 ↑ The two consequences of defining itself as the archetype fibers limitations of the two symbol sets and : . See W. Vogler (2007/2008) p. 3.
 ↑ Stefan Brass (2005) p. 16. The explanations there for multisort signatures have been simplified here. The set of natural numbers takes the place of the Kleen's covering over the varieties . Constants are understood as zerodigit functions, zerodigit relations are permitted. The author uses the term predicate symbols with designations , and instead of , and .
 ↑ ^{a } ^{b} Stefan Brass (2005), p. 20
 ↑ Cremers et al., (1994), p. 148; see also polymorphism (programming) .
 ↑ See also correspondence
 ↑ The asterisk attached above means the positive envelope .
 ↑ Expressed in set theory, functions are special relations:, where the power set (set of all subsets) denotes.
 ↑ Equivalent in set theory:, in particular, is for singledigit relations (subsets) or equivalent . If zerodigit relations (logical constants) are permitted, for them or .
 ↑ R. Letz (2004) p. 6. The author uses the notation instead of for the interpretation function .
 ↑ is written here as a family . This arises from the disjoint union of the three parts, so that one can define equivalently with the help of the restrictions .
 ↑ See firstorder predicate logic §Semantics
 ↑ Sometimes one speaks of an area ( value or object area ), e.g. B. if it is a number range .

↑ For the interpretation function on the set of constants this means that their image area through the singleton is replaced, the value range whereby to simplified. Sometimes zerodigit relations are allowed. These can be understood as logical constants. then denotes all relation symbols including the zerodigit. In the above relation for the signature is accordingly by replacing; the range of values increases with zerodigit functions and relations
 ↑ A. Oberschelp (1962), p. 298
 ↑ The set of variable symbols can be finite or countably infinite (see Stefan Brass (2005) p. 13), in the second case variable names composed of several characters are used, which are subject to certain rules so that they can be recognized as variable names, in terms of information theory at in this case is a formal language . Partial mappings as occupancy are allowed if is infinite.
 ↑ For more details see A. Oberschelp (1962) p. 297f
 ↑ For example, errors in data type assignments can be recognized quickly (at compile time ) as system errors.
 ↑ Constants are understood here as zerodigit functions, logical constants possibly as zerodigit relations
 ↑ . In the case of the function symbols, where another type is required for the value range, the values of are in the positive envelope . Arity is the word length of the type (minus 1 for function symbols).