What is the signature of a formal language?

I will briefly state the context where my doubts arise.
I know the following definitions.

A formal language is a set of well-formed formulas. It's a tuple constituited by an alphabet and a formal grammar.

An alphabet of a formal language is a set of symbols. It's usually consituited by letters (symbols whose interpretation depends on the specific context) and signs(symbols whose interpretation doesn't depend on the context and whose aim is to structure the language).

A vocabulary of a formal language is the set of all letters of the alphabet.

A formal grammar of a formal language is a set of rules specifying how to form a well-formed formula from symbols in the alphabet.

I often find the notion of a signature but it's not intuitive to me. Is that the set of signs of a formal language? If not, what is it?

• Actually, in most cases, a formal language is only an arbitrary set of words (= finite sequences) over an alphabet set (= the set of symbols). Usually, we use that to contain formulas, or programs, or expressions, or other common syntactic objects, but that's only a possible case. – chi Feb 6 at 17:21
• @chi Yes I imagine it as a sort of degenerate case. – Gabriele Scarlatti Feb 6 at 18:16

In my experience a "signature" is something that puts additional constraints on a language made of syntactic terms. I'll try to provide an example.

Consider the alphabet $$\Sigma = \{f,g,a,b,(,),;\}$$. From this we can build the set of all the words $$\Sigma^*$$. This contains any word, including gibberish like "$$)g;;f(($$".

Then, we can craft the set of syntactic terms $$T \subseteq \Sigma^*$$ through an inductive definition.

We start by defining a subset $$F \subseteq \Sigma$$ as $$F = \{f,g,a,b\}$$, and we call this the set of function symbols. Then, inductively, we state that if $$t_1,\ldots,t_n$$ (with $$n\geq 0$$ are terms and $$s\in F$$, the word $$s(t_1;\ldots;t_n)$$ is a term.

Note that $$n=0$$ above gives the "base case" of the induction. We then have that $$f()$$ is a term, $$a()$$ is a term, $$f(a();b())$$ is a term, $$f(f(a();b();a();a(b())))$$ is a term, and so on.

Now, we might want to put more constraints on those terms. For instance, we might want to associate to each $$s \in F$$ a fixed nubmer of arguments, and consider only those terms respecting that. For instance, if we decide that $$f$$ has arity two (f is binary), then we allow $$f(a();b())$$ but not $$f(a())$$ nor $$f(a();f())$$. This restriction essentially defines a subset language $$L\subseteq T$$.

This is sometimes done by specifying a signature. E.g. something like $$\begin{array}{l} f : A \times A \to A \\ g : A \to A \\ a : 1 \to A \\ b : 1 \to A \\ \end{array}$$ The above is a fancy way to state that $$f$$ is binary, $$g$$ is unary, and $$a,b$$ are both constants (= zero-arity function symbols). $$1$$ is used to mean no-arguments.

A possible term here is $$f(g(a());b())$$.

The name $$A$$ above is called a "sort", and has no deep meaning on its own. The above is called a single-sorted signature since it uses only one sort. By contrast $$\begin{array}{l} f : A \times B \to A \\ g : A \to B \\ a : 1 \to A \\ b : 1 \to A \\ \end{array}$$ uses two sorts. This now forbids $$f(g(a());b())$$ since $$g(a)$$ has not sort $$A$$ as required. Instead, $$f(b();g(a()))$$ is still allowed.

When terms are logical formulae, it is common to use signatures to keep our words meaningful. For instance

$$\begin{array}{l} \land : P \times P \to P \\ {\sf prime} : \mathbb N \to P \\ 0 : 1 \to \mathbb N \\ s : \mathbb N \to \mathbb N \\ \end{array}$$ allows $$\land({\sf prime}(0());{\sf prime}(s(0())))$$ (i.e. $${\sf prime}(0) \land {\sf prime}(s(0))$$, in more casual notation), but disallows nonsense such as $$\land({\sf prime}(0());0())$$ (i.e. $${\sf prime}(0) \land 0$$) which tries to use term $$0()$$ as if it were a proposition (a term of sort $$P$$).