When one uses the universal quantifier '∀', it is ungrammatical to not include both a variable it binds, and a formula it scopes over: ∀ x, Φ. Likewise, in natural language, "For all x, Φ is true" is meaningful.

The same is true for sentences using the existential quantifier '∃': ∃ x, Φ. However, in natural language, it sounds sensible to say, "x exists".

One reason it does not make sense in formal logic, is that variables are not "things in the domain"; when you say "x exists", the sentence isn't meaningful because x doesn't refer to anything.

c, a constant, refers to something, but it is still formally wrong to say ∃ c, because we only bind quantifiers to variable symbols, not constants.

One thing you can say, is ∃ x, x = c.

However, given the standard presentation of a signature in first-order logic, the above formula would always be unneeded in a set of axioms. If a constant symbol c exists in the signature, it is required to be mapped to an element in the domain. Thus, it is always given that in a model of a theory, for every constant c, there exists an x such that x = c. (I'll give you 1 million dollars if you can guess which value of x it is.)

There is some interesting writing here for reference, that I include as context for my question. I haven't read it yet.

This came about by trying to formalize the syntax of first-order logic, which I am told is carried out in the textbook by Enderton, which I will read soon.

When we present a signature as a set, I do not think we are declaring the existence of this set. In general, we assume the existence of a world of sets; we can only point to sets that already exist, by specifying them.

However, it feels natural to begin a formal theory by saying: "The following sets exist: a set of constant symbols, a set of variable symbols, etc."

It feels awkward to say, "x equals a particular set". But perhaps this is, after all, the 'correct' way. Which is good to know.