Signature (model theory)

from Wikipedia, the free encyclopedia

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 Zermelo-Fraenkel set theory can be formulated in the language of first-order 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 first-level predicate logic §Expressions .

definition

Let and be pairwise disjoint sets of non-logical 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

  1. The constant symbols can also be counted among the function symbols, so that results with .
  2. Occasionally, symbols for zero-digit 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 .
  3. 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 .
  4. 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 : .

  5. 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 non-empty set and . Then is a figure so that  

  • is a constant for each
  • a function is for each   and
  • there is a relation for each

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

  1. A constant can be understood as the zero-digit function such that :
    with functions and with relations
  2. 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
  3. If a structure only contains functions ( algebraic structure ) or only relations ( relational structure , in particular order structure ), then it often has special properties.
  4. The definition can be extended to partial functions to e.g. B. to capture partial algebras .
  5. 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 , K-algebras , Lie-algebras, etc.) with several carrier sets , one can introduce multi-site or multi- site signatures . In addition to the function and relation symbols, there are also types and descriptions for the carrier quantities. An n-ary relation is a subset of the n-fold Cartesian product of a sequence of the carrier sets . The argument range of an n-place function is just such a product, plus one of the carrier sets for the value range.

Multi-varietal can always be traced back to single- varietal by adding the variety affiliation for each variety as a one-digit relation ( variety predicate ). In contrast to the second-order 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. 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.

Among the amounts for the function and for the relation symbols yet another finite, non-empty 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

  • Heinz-Dieter 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 3-411-15603-1 , 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 3-87144-323-9 , pp. 361-363 .
  • Philipp Rothmaler: Introduction to Model Theory . Spektrum Akademischer Verlag, 1995, ISBN 978-3-86025-461-5 .
  • Erich Grädel: Mathematical Logic . Mathematical Foundations of Computer Science, SS 2009. RWTH, Aachen, S. 129 ( fldit-www.cs.uni-dortmund.de [PDF]).
  • W. Vogler: Logic for computer scientists . WS 2007/2008. Univ. Augsburg, Institute for Computer Science, Augsburg, p. 49 ( informatik.uni-augsburg.de [PDF]).
  • Uwe Kastens: Predicate logic . University of Paderborn, Institute for Computer Science, Paderborn 2008, p. 31 ( cs.uni-paderborn.de [PDF]).
  • Thomas Worsch: Predicate logic . Unit 18: Logic, WS 2008/2009. University of Karlsruhe, Faculty of Computer Science, Karlsruhe, S. 35 ( cs.uni-paderborn.de [PDF]).
  • Armin B. Cremers, Ulrike Griefahn, Ralf Hinze: Type systems. In: Deductive Databases. Artificial Intelligence . Vieweg + Teubner, Wiesbaden 1994, ISBN 978-3-528-04700-9 , Chapter 5: Type systems, p. 147-182 , doi : 10.1007 / 978-3-663-09572-9_5 .

The multi-site or multi-site case is treated in the following sources:

  • Arnold Oberschelp : Investigations into the multi-variety quantifier logic . In: Mathematical Annals . tape 145 , no. 4 . Springer, 1962, p. 297-333 , doi : 10.1007 / BF01396685 ( eudml.org ).
  • Arnold Oberschelp; Ed .: Karl Hans Bläsius, Ulrich Hedtstück, Claus-Rainer Rollinger: Order Sorted Predicate Logic . Lecture Notes in Computer Science (LNCS), Volume 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 .
  • François Bry: Excursus: First-order multi-varietal 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 Halle-Wittenberg, Institute for Computer Science, Halle 2005, p. 176 ( users.informatik.uni-halle.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.uni-leipzig.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 ( fernuni-hagen.de - diploma thesis). , at: FernUni Hagen, fernuni-hagen.de (PDF). Original at: Universität Karlsruhe 1992, Institute for Logic, Complexity and Inference Systems

References and comments

  1. 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.
  2. See E. Grädel (2009) p. 45.
  3. see propositional logic §Buildings of propositional language
  4. For example Kruse, Borgelt (2008) p. 3
  5. See E. Grädel (2009) p. 45 f
  6. E. Grädel (2009) p. 46 f
  7. In the English-language literature there is also the designation (from arity , arity ) instead of .
  8. The two consequences of defining itself as the archetype fibers limitations of the two symbol sets and :   . See W. Vogler (2007/2008) p. 3.
  9. Stefan Brass (2005) p. 16. The explanations there for multi-sort 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 zero-digit functions, zero-digit relations are permitted. The author uses the term predicate symbols with designations , and instead of , and .
  10. a b Stefan Brass (2005), p. 20
  11. Cremers et al., (1994), p. 148; see also polymorphism (programming) .
  12. See also correspondence
  13. The asterisk attached above means the positive envelope .
  14. Expressed in set theory, functions are special relations:, where the power set (set of all subsets) denotes.
  15. Equivalent in set theory:, in particular, is for single-digit relations (subsets) or equivalent . If zero-digit relations (logical constants) are permitted, for them or .
  16. R. Letz (2004) p. 6. The author uses the notation instead of for the interpretation function .
  17. 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 .
  18. See first-order predicate logic §Semantics
  19. Sometimes one speaks of an area ( value or object area ), e.g. B. if it is a number range .
  20. 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 zero-digit relations are allowed. These can be understood as logical constants. then denotes all relation symbols including the zero-digit. In the above relation for the signature is accordingly by replacing; the range of values ​​increases with zero-digit functions and relations
  21. A. Oberschelp (1962), p. 298
  22. 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.
  23. For more details see A. Oberschelp (1962) p. 297f
  24. For example, errors in data type assignments can be recognized quickly (at compile time ) as system errors.
  25. Constants are understood here as zero-digit functions, logical constants possibly as zero-digit relations
  26. . 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).