Bear with me as I present Quine's argument that names (of relata) are, however useful, superfluous in first-order predicate logic:
Chief among the omitted frills is the name. This again is a mere convenience and is strictly redundant, for the following reasons. Think of ‘a’ as a name, and think of ‘F(a)’ as any sentence containing it. But clearly ‘F(a)’ is equivalent to ‘(∃x)( a = x & F(x))’. We see from this that ‘a’ need never occur except in the context ‘a =’. But we can as well render ‘a =’ always as a simple predicate ‘A’, thus abandoning the name ‘a’. ‘F(a)’ gives way thus to ‘(∃x)(A(x) & F(x))’, where the predicate ‘A’ is true solely of the object ‘a’.
“It may be objected that this paraphrase deprives us of an assurance of uniqueness that the name has afforded. It is understood that the name applies to only one object, whereas the predicate ‘A’ supposes no such condition. However, we lose nothing by this, since we can always stipulate by further sentences, when we wish, that ‘A’ is true of one and only one thing:
(∃x)A(x) & ~ (∃x,y)(A(x) & A(y) & ~(x=y) )
...(This identity sign “=” here would either count as one of the simple predicates of the language or be paraphrased in terms of them.)
During reduction to Skolemized form, Skolem functions of ∀x quantified variables, such as g(x) replace the ∃y quantified variables in particular predicates such that P(y) becomes P(g(x)) so that all variables are ∀ quantified. These Skolem functions are minted for the particular purpose of mapping from ∀ quantified relata to what had been ∃ quantified relata.
This is reminiscent of Quine's minting the predicate for an, otherwise, named relata and leads me to conjecture there may have been work done to achieve the aims of Skolemization without the use of either names or Skolem functions.
Has any such work been done?