Substitution function in FOL

Question

After reading some articles on substitution, I've been trying to translate the substitution operation to first-order logic. For example, given a term $P(x, y)$ and the substitution function $\sigma = \{x \rightarrow a, y \rightarrow b\}$, then $P(x, y) \sigma = P(a, b)$. My first hypothesis is that the expression $P(x, y) \sigma$ means $\exists x \exists y[P(x, y) \land x=a \land y =b]$, which is logically equivalent to $P(a, b)$. A second hypothesis would be that $P(x, y) \sigma$ stands for $\forall x \forall y[x=a \land y=b \rightarrow P(x, y)]$, which is also equivalent to $P(a, b)$. However, in both cases, the function $\sigma$ is presented as the identity function $\sigma(x)=x$, which is not a requirement for $\sigma$ according to the formal definition of the substitution function. Does anyone have any idea for possible translations in FOL of such logical expression $P(x, y)\sigma$?

Answer 1

The substitution operation $\sigma$ is not part of the formal language of first order logic. It is part of the metalanguage. If "$f$" is a function symbol of the language and "$x$" a symbol of a variable or of a constant, thus, a term of the formal language, then "$f(x)$" is also a term of the formal language. But either the symbol "$\sigma$" or the expression "$P(x,y)\sigma$" belong to the language. Moreover, $f$ maps the possible values of $x$ with the correspondent values of $f(x)$. The substitution operation $\sigma$, on the other hand, is a map from a set of symbols to another set of symbols: from the variables to the terms. It would be more accurate to write: $\sigma=\{"x" \mapsto"a","y"\mapsto"b"\}$. It is not possible to express $\sigma$ in the formal language, because the symbols of the language are not elements of the set of objects from witch the terms of the language take their values. Only outside of the language you can have that kind of a map, where you can treat the symbols of the language as objects (individuals).