Talk:Signature (logic)

This  level-5 vital article is rated B-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:

Mathematics Low‑priority This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles Low This article has been rated as Low-priority on the project's priority scale.

The name of the article Signature (in mathematical logic) is not too good, it should be “Signature (mathematical logic)”. But this latter name redirects to Signature (universal algebra).

Maybe merging, renaming, redirecting can be thought of.

Physis 11:33, 5 November 2006 (UTC)[reply]

For now I moved (using the admin tools) signature (in mathematical logic) to signature (mathematical logic). I can't say if some merge with signature (universal algebra) should take place as I am not an expert. Oleg Alexandrov (talk) 03:59, 6 November 2006 (UTC)[reply]

It makes no sense to keep signature (mathematical logic) and signature (universal algebra) separate, as it is a very simple basic concept which is common to both areas. One special point in universal algebra is that usually (not always) relations are not allowed in a signature. In many contexts in model theory, on the other hand, arguments can be simplified by assuming (w.l.o.g. for these contexts) that signatures contain only relations. Also in model theory people use formulations like "language" or "non-logical symbols of the language" when they are really referring to a signature. --Hans Adler 20:57, 12 November 2007 (UTC)[reply]

I couldn't find a definition of sorts in Wikipedia. Is it just any enumerable set? An alphabet? Is it defined by the role its playing? Is it part of category theory? -- Bartosz 20:07, 25 November 2006 (UTC)[reply]

Sorts are a simple and very fundamental concept of model theory (and universal algebra) which, for historical reasons, is almost never explained in introductory texts. They are similar to types in a programming language. For example, one way of describing a vector space (although for many purposes not a good one) is as a two-sorted structure, with one sort for the field of scalars and one sort for the vectors. In a many-sorted setting, the arity of a symbol contains additional information. For example, it's not enough to know that scalar multiplication is a binary function. It's a function from scalars ${\displaystyle \times }$ vectors to vectors. And there are two addition symbols, one for the scalars and one for the vectors. It should be clear from this explanation that an arbitrary set will do as a set of sorts. It's only used to index things. It can be finite or infinite of arbitrary cardinality. To avoid stupid special cases we may want to require that it's non-empty, however. --Hans Adler 21:09, 12 November 2007 (UTC)[reply]

Does anyone know a mathematical (as opposed to historical or philosophical) argument why so many authors exclude nullary relation symbols? --Hans Adler (talk) 11:46, 22 November 2007 (UTC)[reply]

A nullary relation is either true or false, and these can be achieved as ${\displaystyle \forall x(x=x)}$ and its negation, so I don't think there is much benefit to including them. — Carl (CBM · talk) 01:55, 26 November 2007 (UTC)[reply]

It only gets interesting when you consider several structures. If you add a nullary predicate to the language of groups, then you will tag every ring with either "false" or "true". Homomorphisms can go from "false" groups to "false" groups, from "true" groups to "true" groups and from "false" groups to "true" groups, but never from a "true" group to a "false" group. In logic you can emulate this by using a unary predicate P and adding an axiom ${\displaystyle \forall x\forall y(Px\leftrightarrow Py)}$. But universal algebra, where this would actually be useful (because of applications in computer science) can't even do that. (Actually, it may be possible to fix this by introducing the Boolean operator → into universal algebra, but that seems to be a much bigger change.) The translation also introduces a silly problem if you allow empty structures. Of course they should be tagged as well.

With nullary predicates first-order logic actually contains propositional logic. I read the following in Dawson, "The compactness of first-order logic: from Gödel to Lindström" (1993, p. 17) on Gödel's completeness proof (1930): "First, Gödel works within the formal framework of the 'restricted functional calculus' of Hilbert and Ackermann, a framework that subsumes both the propositional calculus and first-order logic.'" I am not sure what that means, but it could mean that others have felt similarly before me.

But really my main concern here is elegance. Authors seem to feel the awkwardness of saying "the arity can be any natural number including 0, but if the symbol is a relation it must not be 0". On the other hand they don't want to change this funny tradition, and so they treat constants separately in order to hide the awkwardness. (Which does make a lot of sense from a didactic POV, of course, but leads to a lot of silly duplication if inductive proofs are carried out in full.) --Hans Adler (talk) 09:55, 26 November 2007 (UTC)[reply]

PS: I just became aware of an elegant many-sorted workaround. Replace a propositional constant by a new sort, and add the axiom ${\displaystyle \forall x(x=x)}$ for the new sort. This sort can have 0 or 1 element, 0 representing "false" and 1 representing "true". This seems to demonstrate that any mathematical problems from admitting nullary predicates would also arise in many-sorted first-order logic with possibly empty sorts. --Hans Adler (talk) 10:40, 26 November 2007 (UTC)[reply]

PPS: Many-sorted first-order logic with 0 sorts is exactly propositional logic if nullary predicates are allowed. Otherwise it's essentially nothing. --Hans Adler (talk) 10:44, 26 November 2007 (UTC)[reply]

The sentence

Signatures play the same role in mathematics as type signatures in computer programming,

which is found in the lead is not sourced and not discussed in the body of the article. A type signature in computer science applies to a single function and describes its arguments. A signature in logic applies to a formal language and describes the symbols that it uses. There is some vague similarity between these two concepts (besides both having the name "signature"), but not enough to warrant this sentence. Dominic Mayers (talk) 02:14, 11 November 2020 (UTC)[reply]