SIGNATURE (MATHEMATICAL LOGIC)

In mathematical logic, a 'signature' describes the non-logical symbols of a formal language.

Contents

Model theoretic conventions

Other first-order conventions

Many-sorted logic

Blur or not

Blur

Avoid blurring

Other aspects for alternatives

Notes

See also

External links

Model theoretic conventions

In model theory a 'signature' σ is a quadruple (''C'',''F'',''R'',''a'') where ''C'', ''F'', and ''R'' are disjoint sets not containing basic logical symbols, called respectively

★ ''constant symbols'', (examples: 0, 1),

★ ''functions symbols'', (examples: +, ×)

★ and ''relation symbols'' , or ''predicates'' (examples: ≤, ∈)
and a function ''a'': ''F'' ∪ ''R'' → 'Z'⁺ assigning ''arity'' to the function and relation symbols.
A signature, along with the logical symbols of first-order logic, form the building blocks for a first-order 'language'.
The first-order language consists of 'formulas' that are inductively built up from these symbols in the usual way: first by building terms, and then closing under logical operations of quantification over variables, negation and conjunction. The conditional "first-order" refers to the scope of the quantifiers: one can quantify over elements of the universe, but not subsets or functions. For example, many statements in functional analysis are not first order sentences about the real numbers in the language of fields. On the other hand, many statements in elementary number theory are first order sentences. A 'sentence' is a formula with no free variables. A 'theory' is a set of sentences, is called 'consistent' if no contradiction can be arrived at by following standard rules of inference, and is called 'closed' if it contains all consequences of its elements; often theories are assumed to be both consistent and closed.

Other first-order conventions

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\; o\; mathbb\; N$
where ''F'' is the set of non-logical symbols used in the role of function names, ''R'' is the set of non-logical symbols used in the role of relation names.
Another way:
:$I\; o\; (mathbb\; N\; imes\; 2)$
where ''I'' denotes the set of non-logical symbols, and 2 is any two-element set (e.g. $left\{mathrm\{function\},;\; mathrm\{relation\}$
ight} can be seen as a didactic choice).

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 appropriate way: manages arity, distinction between assertive versus functional “parts of speech”. And a surplus to this: it also sees to if sorts match.

Blur or not

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 framework.

★ Set of sorts ''S''

★ Set of operations $Omega$. 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.

Avoid blurring

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

★ distinction between function 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

Other aspects for alternatives

Independent of whether we blur or not, constants can be treated as a special 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 provide an unambiguous 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.

Notes

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

See also

★ Assignment (mathematical logic)

★ Signature (universal algebra)

External links

★ Basic notions of model theory section in the Model theory entry of Stanford Encyclopedia of Philosophy

★ An Introduction to the Algebraic Specification of Abstract Data Types written by Jean Baillie

★ Signature entry of PlanetMath describes the concept for the case when no sorts are introduced