Sorts in many sorted logic

Question

In the syntax of many sorted logic, the following statement has been encountered

We fix an infinite set $S$ of sort symbols and consider an infinite set $X$ of (sorted) variables, each uniquely associated with a sort in $S$.

Let $S=\{\ s_1, s_2, s_3 \cdots\}$ and $X=\{x_1, x_2, x_3\cdots\}$

Now, what is the difference between a sort and a sort symbol. Are they same? It is evident from the statement that $s_i$ for any natural $i$ is a sort symbol. Then what is sort here, if it is different from sort symbol?

Further is sort symbol a set by itself? If yes, then what such set contains?

Answer 1

A sort is the same thing as a sort symbol. It's just a symbol--it's not a set (except in the way that everything is a set in axiomatic set theory). You should think of it as somewhat analogous to a function or relation symbol.

Now, when you have a structure over the language, it will have a set associated with each sort (just like it has a relation associated with each relation symbol and a function associated with each function symbol). These sets can sometimes also be referred to as "sorts". This usually does not cause any confusion, just as not distinguishing carefully between a function symbol and the associated function in a structure usually does not cause any confusion.

Answer 2

You're not reading the sentence correctly when you write

Let $S=\{\ s_1, s_2, s_3 \cdots\}$ and $X=\{x_1, x_2, x_3\cdots\}$

Instead, you should say

Let $S=\{\ s_1, s_2, s_3 \cdots\}$ and, for each $s_i$, let $X_i=\{x^{s_i}_1, x^{s_i }_2, x^{s_i}_3\cdots \}$

Every variable is explicitly tied to one of the sorts, and there is a separate set of variables for each sort.

In particular, the sorts are part of the syntax of multisorted logic - when we write a formula, we have to explicitly annotate a sort onto every variable, constant symbol, and function symbol, and every term will also have exactly one sort.

There are no variables that are "ambiguous" as in the set $X$ you wrote. That kind of variable appears in regular non-sorted first-order logic.