I was stimulated by a recent question about Gödel Completeness Theorem.
All my citations are from Jean van Heijenoort (editor), From Frege to Gödel : A Source Book in Mathematical Logic (1967).
Gödel's paper (1930) [page 583] in the first paragraph says :
the question [...] arises whether the initially postulated system of axioms and principles of inference is complete, that is, whether it actually suffices for the derivation of every true logico-mathematical proposition, or whether, perhaps, it is conceivable that there are true propositions (which may even be provable by means of other principles) that cannot be derived in the system under consideration. For the formulas of the propositional calculus the question has been settled affirmatively; that is, it has been shown [footnote: Bernays 1926] that every true formula of the propositional calculus does indeed follow from the axioms given in Principia mathematica. The same will be done here for a wider realm of formulas, namely, those of the "restricted functional calculus"; that is, we shall prove
THEOREM I. Every valid [footnote: To be more precise, we should say "valid in every domain of individuals", which, according to well-known theorems, means the same as "valid in the denumerable domain of individuals".] formula of the restricted functional calculus is provable.
The concept of valid formula is no longer explained.
Browsing thorugh the volume, is hard to find any reference to the concept.
Frege, Begriffsschrift (1879); very few hints to the "nature" of logical truth [page 28] :
We have already introduced a number of fundamental principles of thought in the first chapter in order to transform them into rules for the use of our signs. [...] Now in the present chapter a number of judgments of pure thought for which this is possible will be represented in signs. It seems natural to derive the more complex of these judgments from simpler ones, not in order to make them more certain, which would be unnecessary in most cases, but in order to make manifest the relations of the judgments to one another. [...] In this way we arrive at a small number of laws in which, if we add those contained in the rules, the content of all the laws is included, albeit in an undeveloped state. [...] in view of the boundless multitude of laws that can be enunciated we cannot list them all, we cannot achieve completeness except by searching out those that, by their power, contain all of them.
Löweheim, On possibilities in the calculus of relatives (1915) ; the editor in the introductory note says [page 228] : Löwenheim's paper deals with problems connected with the validity, in different domains, of formulas of the first-order predicate calculus [...] Löwenheim introduces a number of definitions and symbols. In particular, an "identical equation" is a valid well-formed formula.
But the original paper speaks ony of "identically satisfied" ; [page 238] :
If we now want to decide whether or not [...] is identically satisfied in some domain, then ...
Skolem Logico-combinatorial investigations ... (1920) – the editor in the introductory note says [page 253] : In Skolem's formulation of Löwenheim's theorem and its generalizations the phrases "is a contradiction" and "is contradictory" have to be understood in the semantic sense, that is, as "is not satisfiable" […] The same remark applies to Skolem's subsequent papers (1922, 1928, and 1929), where he also uses "consistent" in the sense of " satisfiable".
Post Introduction to a general theory of elementary propositions (1921) deals with "the propositional calculus, carved out of the system of Principia mathematica, [that] is systematically studied in itself, as a well-defined fragment of logic [introductory note, page 264] :
Let us denote the truth value of any proposition $p$ by $+$ if it is true and by $-$ if it is false [page 267]. The [truth-functions] can then be classified according to their tables as follows: those which have all their truth values $+$, all $-$, or some $+$ and some $-$. We shall call these functions respectively positive, negative, and mixed [page 269].
David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (engl transl of the 2nd german ed, 1938) is definitively "modern":
It is now the first task of logic to find those combinations of sentences which are logically true, i.e. true independently of the truth values of the elementary sentences [page 14].
A formula of the predicate calculus is called logically true or, as we also say, universally valid only if, independently of the choice of the domain of individuals, the formula always becomes a true sentence for any substitution of definite sentences, of names of individuals belonging to the domain of individuals, and of predicates defined over the domain of individuals, for the sentential variables, the free individual variables, and the predicate variables respectively. The universally valid formulas of the predicate calculus will also, for convenience, sometimes be called simply valid [page 68].
So the concept of valid formula is "crawled inside" between Löweheim (1915) and Gödel (1930), which uses it as background knowledge.
Is it possible to track with more detail when this concept has been stated for the first time with precision ?