Function symbols in many sorted logic Consider the following definition > We fix an enumerable set **Fun** of `function symbols`. Each function symbol has associated to it an arity of the form $σ1 \times \cdots \times σn \rightarrow σ$, where $n \ge 1$ and $σ1,\cdots , σn, σ$ are sorts. We denote with $Fun_{\\{σ1 \times \cdots \times σn \rightarrow σ\\}}$ the set of function symbols of arity $σ1 \times \cdots \times σn \rightarrow σ$. We assume that $Fun_{\\{σ1 \times \cdots \times σn \rightarrow σ\\}}$ is enumerable, for all sorts $σ1, . . . , σn, σ$. Arity in general refers to the number of arguments a function takes. Is the arity in the definition refers same? Let $f$ is a function symbol, then is my interpretation true that the domain of $f$ is $σ1 \times \cdots \times σn$ and the range of $f$ is $σ$? If not then what are $σi'$s?

In this case _arity_ is not "only" the number of argument places.

The funcion $f$ has $n$ argument places but each argument place $i$ must be "filled" with a term of sort $\sigma_i$.

Consider e.g a binary function $f$ whose arguments are the first one a _natural_ number and the second one a _real_ and whose value is a _complex_ :

> $f : \mathbb N \times \mathbb R \to \mathbb C$.