Signature (mathematical logic)

From Wikipedia, the free encyclopedia

In mathematical logic, a signature equips non-logical symbols of a formal language with such an information which plays a role similar to typing in computing and mathematics.

1 Without sorts
2 Many-sorted logic
- 2.1 Blur or not
  - 2.1.1 Blur
  - 2.1.2 Avoid blurring
- 2.2 Other aspects for alternatives
3 Notes
4 See also
5 External links

[edit] Without sorts

If we do not deal with many-sorted logics, then signature simply means

maintaining arity information
avoiding confusing relation names with function names.

Thus, two requirements must be met:

partitioning the non-logical symbols into two classes: function versus relation names (or, equivalently, associating a binary flag, e.g. a truth value to each non-logical symbol)
attaching an arity to each non-logical symbol (of a first-order language), or, equivalently, mapping them to the set of natural numbers

There are multiple ways to formalize:

$F + R \to \mathbb N$

where F is the set of non-logical symbols used in the role of funtion names, R is the set of non-logical symbols used in the role of relation names.

Another way:

$I \to (\mathbb N \times 2)$

where I denotes the set of non-logical symbols, and 2 is any two-element set (e.g. $\left\{\mathrm{function},\; \mathrm{relation}\right\}$ can be seen as a didactic choice).

[edit] Many-sorted logic

Also in many-sorted logic, signature is a package of information that keeps track of the the way arguments are filled in an approriate way: manages arity, distinction between assertive versus functional “parts of speech”. And a surplus to this: it also sees to if sorts match.

[edit] Blur or not

[edit] Blur

Sorts (containing a specific sort to denote the type of truth values) can be used to blur the distinction between assertive and functional “parts of speech” of the language, between function symbols (name functors) and relation symbols (predicates). Even logical connectives be treated inside this frame.

Set of sorts S
Set of operations $Ω$ . Each operation can be regarded as a unique name equipped with an ordered pair: this pair consists of a (possibly empty) sequence of sorts, and a sort. This can be formalized as a mapping from a set of operator names to a non-empty sequence of sorts.

[edit] Avoid blurring

Another treatment avoids this blurring (resembling more to the non-sorted case) ^[1]: a signature is a package of information ^[2] providing

distinction between functon symbols and predicate symbols
assigning (in either case) a sequence of sorts to symbols
- in case of function symbols, a non-empty sequence (or a pair of a possibly empty sequence of sorts and a sort)
- in case of relation symbols, a possibly empty sequence of sorts

[edit] Other aspects for alternatives

Independent on whether we blur or not, the case for constants can be merged into the case of function symbols, or can be handled specially (just like in “non-sorted” logic).

We may assign to each variable “its” sort. But there is also a more dynamic solution: variables are not typed before using them in formulas and terms. Formulas and terms are required to prvide an unambigus typing for their variables (they can contain no variable in different typing) ^[3].

There are also other (but in essence, equivalent) formalizations. There may be also other variations, e.g. whether overloading names is allowed.

[edit] Notes

^ Many-Sorted Logic, the first chapter in Lecture notes on Decision Procedures, written by Calogero G. Zarba.
^ there may be many different alternative ways to achieve this
^ Csirmaz, László: Nemsztenderd analízis. TypoTex Kiadó, Budapest, 1999.