Function symbol

In formal systems particularly mathematical logic, a function symbol is a non-logical symbol which represents a function or mapping on the domain of discourse, though, formally, does not need to represent anything at all. Function symbols are a basic component in formal languages to form terms. Specifically, if the symbol ${\displaystyle F}$ is a function symbol, then given any constant symbol ${\displaystyle X}$ representing an object in the language, ${\displaystyle F(X)}$ also represents an object in the language. Similarly, if ${\displaystyle T}$ is some term in the language, ${\displaystyle F(T)}$ is also a term. As such, the interpretation of a function symbol must be defined over the whole domain of discourse. Function symbols are a primitive notion, and are therefore not defined in terms of other, more basic concepts.

In typed logic, F is a functional symbol with domain type T and codomain type U if, given any symbol X representing an object of type T, F(X) is a symbol representing an object of type U. One can similarly define function symbols of more than one variable, analogous to functions of more than one variable; a function symbol in zero variables is simply a constant symbol.

Now consider a model of the formal language, with the types T and U modelled by sets [T] and [U] and each symbol X of type T modelled by an element [X] in [T]. Then F can be modelled by the set

${\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}$

which is simply a function with domain [T] and codomain [U]. It is a requirement of a consistent model that [F(X)] = [F(Y)] whenever [X] = [Y].