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][1] 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.


  [1]: https://plato.stanford.edu/entries/quantification/#QuaPreExiFreRus