First publication of first-order language with function symbols

Question

What was the first publication of a first-order language that included function symbols, such as the functors of language B of Carnap’s Einführung in die symbolische Logik (1954)?

Function symbols seem to have become commonplace by the mid 1960s -- e.g, Shoenfield's Mathematical Logic (1967) -- but not earlier.

Answer 1

As Mauro ALLEGRAMZA suggested, function symbols ("Funktionszeichen") are introduced in [1], along with the notion of a term. This is a translation by Google Translate from pages 186-187 of the 1968 edition:

Now the mathematical function signs - we say simply "function signs" - are to be introduced as a new kind of symbols. As a function sign we generally take, i.e., unless some special common symbol is used, lowercase Greek letters. The function signs differ from the predicate symbols in the formalism in that a predicate symbol provided with arguments forms a formula (namely a prime formula), whereas a function sign provided with arguments forms a "term", where "term" from now on should be the common designation for such expressions that can be used for a free individual variable. The insertion rule for the free individual variables now receives an extension. As terms, i.e. for substitution for the free individual variables, [are] admitted:

1. Free individual variables;
2. Individual symbols;
3. Function characters whose argument places are each either through is a free individual variable or is filled by an individual symbol;
4. Expressions obtained by, starting from an expression of the third kind (with at least one free variable occurring in it), once or repeatedly applying the process of replacing a free individual variable by an expression of the third kind.

According to Heijenoort [2], "In Chapter 3 [of his thesis] Herbrand [3] calls any system a theory if it is obtained from his system of Chapter 2 by the adjunction of some of the following: (1) Function letters (called descriptive functions and intended to represent in the system functions from individuals to individuals) together with an extended rule of existential generalization, ...".

In his 1920 paper [4] (translated to English in [2]), Skolem says:

It is now easy to carry out the proof of Theorem 2. Let a first order proposition in normal form,

$$\forall_{x_1} \ldots \forall_{x_m} \exists_{y_1} \ldots > \exists_{y_n} U_{x_1…x_m y_1…y_n}$$

be given, and let us assume that it is satisfied in a given domain for certain values of the relative symbols occurring in $U$. By the principle of choice we can then, for every choice of $x_1, \ldots, > x_m$, imagine a definite sequence chosen from among the corresponding sequences $y_1, \ldots, y_n$, that is the sequences $y_1, \ldots, y_n$ for which $U_{x_1 \ldots x_m y_1…y_n}$ is true. We can appropriately denote by

$$y_1(x_1, \ldots, x_m), y_2(x_1, \ldots, x_m), \ldots, y_n(x_1, > \ldots, x_m)$$

or, more briefly, by $y_1(x), y_2(x), \ldots, y_n(x)$, the sequence of the $y$ that correspond to the sequence $x_1, \ldots, x_m$. Then the proposition

$$U_{x_1 \ldots x_m y_1(x) y_2(x) \ldots y_n(x)}$$

holds for every choice of $x1, \ldots, x_m$. ...

[1] David Hilbert and Paul Bernays. Grundlagen der Mathematik. 1934.

[2] Jean van Heijenoort. From Frege to Gödel. 1967.

[3] Jacques Herbrand. Reserches sur la théorie de la démonstration. 1930.

[4] Thoralf Skolem. "Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen", 1920.