Does using constant symbols in a first-order theory implicitely induce an existence axiom?

Question

If I have a first-order theory $T$ with a constant symbol $c$ in its language, does this implicitely imply that I have to include the following axiom into $T$?

$$\exists x[x=c]$$

More generally, for an n-ary function symbol $f$, do we have to include the following axiom?

$$\forall y_1,...,y_n\exists x[f(y_1,...,y_n)=x]$$

Answer 1

It depends on your definitions and rules of inference. In the usual system, an $L$-structure must make assignments for all of the symbols in $L$; in particular, for $M$ to be an $L$-structure for a language $L$ containing constant symbols, it must identify what those constant symbols refer to, and therefore cannot be empty.

Likewise, most systems of inference allow the following reasoning: $c = c$ by the definition of $=$; therefore $(\exists x)(x = c)$.

So, yes, $T$ must include $(\exists x)(x = c)$ (if you want $T$ to be a complete and consistent theory). But I'm not sure I would count it as an axiom; it's a consequence of the rules of derivation, as much as "$P \vee \neg P$" is.

But! There's no reason we have to have these rules. We could say that an $L$-structure need not make these assignments. In that case, the usual system of inference is unsound (because it proves $(\exists x)(x = c)$) so we would need a new system. I'd recommend one in which $c = c$ is replaced by $(\exists x)(x = c) \to c = c$. Under these definitions, a constant symbol doesn't necessarily preclude the empty universe.

Answer 2

Yes. For example in the theory of fields the constants $0$ and $1$ are used in the axioms, so you must have elements that satisfy the identity relationships $0+a=a, 1\cdot a=a$. Often they are defined to be different with an axiom $0=1$, which eliminates the field with only one element.