How to remove constant symbols from a first-order theory?

Question

This question builds on top of my former question in which I asked whether constant symbols are necessary in first-order theories. In that question I gave a rough idea on how to get rid of these symbols, which was not completely thought through. I will try to fix this now and would be glad if someone can verify this approach.

Lets say we have a first-order theory $T$

• over a language $L$ with (possibly countably infinite many) constant symbols $c_i$.
• we choose (possibly countably infinite many) predicates $\varphi_i(x_1,...,x_{n_i})$ so that $\varphi_i(c_{\sigma_i(1)},...,c_{\sigma_i(n_i)})$ makes up an axiom system of $T$. The $\sigma(i)$ will choose the constant symbols that are present in the $i$-th axiom and $n_i$ (possibly zero) will denote how many are in there.

I want to construct a theory $T'$ over a language $L'$ which got all the constant symbols removed. Still, $T$ and $T'$ should have the exact same models (in some sense). I will do this by replacing the axioms $\varphi_i$

I will need some shorthand notations:

• I write $\vec x$ for a sequence of some of the variables $x_1,x_2,...$ where the exact names are derived from the place of use of this sequence. E.g. in $(\forall \vec x)\varphi_i(\vec x)$ the sequence will consist of the variables $x_{\sigma_i(1)},...,x_{\sigma_i(n_i)}$.
• I write $\vec x=\vec y$ for the statement that the two sequences agree element-wise on the variables that are contained in both of them. If a variable $x_j$ is not in both sequences then $\vec x=\vec y$ does not contain $x_j$.
• I write $\Delta(\vec x)$ for the statement, that all the variables of $\vec x$ are different. So $\Delta(\vec x)$ contains the statement $x_i\not= x_j$ for any pair of distinct variables $x_i,x_j\in\vec x$ conjugated together.

Now I am going to replace the axiom $\varphi_i$ by

$$(A_i)\qquad (\exists \vec x)[\Delta(\vec x)\wedge \varphi_i(\vec x)\quad\wedge\quad(\forall \vec y)\left[\Delta(\vec y)\wedge \varphi_i(\vec y)\rightarrow \vec x=\vec y]\right],$$

and for any pair $\varphi_i, \varphi_j$ of former axioms I will introduce the axiom

$$(A_{ij})\qquad (\forall \vec x \forall \vec y)[\varphi_i(\vec x)\wedge\varphi_j(\vec y)\rightarrow \vec x= \vec y] $$

In the special case that we have constant symbols in $T$, but no axiom contains any of them, I will introduce the axiom $(\exists x)[x=x]$ to ensure that there is at least one element in the model.

In my opinion, this reflects all the properties that the constants inherently brought into the theory. Is this correct? Does this give me an equivalent theory (in some sense, see note 2)?

---

NOTE:

I do not think we should get rid of contant symbols. My motivation is purely academic in the sense, that I want to know whether there is always an equivalent theory without constant symbols, like there is always an equivalent theory replacing function symbols and constant symbols by relation symbols.

As Giorgio and Rene pointed out in there answers to my former question, there are legitimate and useful applications for constant symbols. I do not doubt this.

---

NOTE 2:

I am not sure how to directly compare the (whole "space" of) models of these theories as they are defined over different languages. So the first on is an $L$-structure, the second one an $L'$-structure. Is this done by comparing the categories of structures created by these two theories?

Answer 1

No, constants are needed:

Assume that $\mathcal{L}=\{R,(c_n)_{n\in\omega}\}$ where $R$ is a binary relation and let us consider the following theory $T=\{(R(c_0,c_n))_{n\in\omega},(c_n\neq c_m)_{n\neq m}\}.$ I claim that there is no theory $T'$ of $\mathcal{L}^-=\{R\}$ such that a model satisfies $T$ if and only if its $\mathcal{L}^-$-reduct satisfies $T'$.

Indeed, assume to the contrary that such a $T'$ exists. Let $M=(\mathbb{N}, >)$ be the natural numbers with $R$ defined as the reverse order.

We have that $T\models T'$, that is every model of $T$ satisfies every formula of $T'$. For every formula of $\varphi\in T'$ there exists a finite number of formulas from $T$, let's call it $U_\varphi$, such that $U_\varphi\models\varphi$. This is because if this was not the case, then for every $U$, a finite subset of $T$, we would have that $U\cup\{\lnot\varphi\}$ has a model. This implies by compactness that $T\cup\{\lnot\varphi\}$ has a model, which contradicts the fact that $T\models\varphi$.

Finally, notice that any finite set of formulas of $T$ is satisfied in $M$. Hence for any $\varphi\in T'$, we have that $M\models U_\varphi$. This and the fact that $U_\varphi\models\varphi$ implies that $M\models\varphi$. Since this is true for every $\varphi\in T'$, we have that $M\models T'$.

On the other hand, $M$ can not be expanded to $\mathcal{L}$ so that it satisfies $T$. This concludes the proof.

---

As for your question regarding the size of the language. If the language contains only finite many constants and finite many relations, then you can write in a single formula exactly how the constants relate w.r.t. the relations and hence you can get rid of the constants.

On the other hand, if you have infinite relations then you can do something similar with what I did above: Take $\mathcal{L}=\{c_1,c_2,(R_n)_{n\in\omega}\}$, the theory $T=\{(R_n(c_1,c_2))_{n\in\omega}\}$ and consider the model $M=\{\mathbb{N}, <_n\}$ where $k<_n\ell$ if and only if $n\leq \ell$ and $k<\ell$. Using these you can show exactly what I showed above.

As for functions, this is something that at some point was present in Noah's answer, but it seems removed now, so I add it here: If you have one constant $c$ and one function $f$, then you can define countable many closed terms in the form of $f(f(c))$, $f(f(f(c)))$, etc. Then you can write the same theory as the one I wrote in my original answer by using these terms instead of constants.

---

As Alex points out, the whole idea behind these proofs is that you can have a constant satisfy infinite many relations, but there is no sentence in first-order logic that can express this: The constant binds an object and you can describe infinite many properties of that particular object. This is closely related to the notion of saturation in model theory.

Finally, yes, if you have a theory such that a formula $\varphi$ exists such that $\forall x(\varphi(x)\to(x=c))$ you can do away without $c$, as long as this formula $\varphi$ does not involve $c$.

Answer 2

No, there is no way to just get rid of constants.

Consider the language $L$ consisting of uncountably many constant symbols $c_i$ and no non-constant symbols. Let $T$ be the set of axioms asserting $c_i\not=c_j$ whenever $i\not=j$. Then every model of $T$ is uncountable.

However, by Lowenheim-Skolem there is no theory in the empty language such that every model of that theory is uncountable. So to get an equivalent "constant-free" theory, we would need to add something to the language in addition to deleting the constant symbols.

---

Another construction, this time in a countable language, closely related to but not quite the same as Apostolos' answer:

Take the language $\{c_i: i\in\mathbb{N}\}\cup \{R\}$ where $R$ is a binary relation symbol. Let $T$ be the set of axioms asserting that $R$ is cycle-free and that the $c_i$ form a strictly $R$-descending sequence: $c_0Rc_1Rc_2...$

Now for any theory $T'$ in the language $\{R\}$ containing the axioms asserting that there are no cycles we can construct a model of $T'$ with no infinite $R$-descending sequences (this is a good exercise). Such a model cannot be expanded to a model of $T$.

This example is really really close to Apostolos'; I'm including it, however, because avoiding ill-foundedness is a useful technique elsewhere in logic (as is avoiding well-foundedness, but that's much easier via compactness).

Answer 3

I want to make a point that I think hasn't been clearly articulated yet in the discussion.

Let $L$ be a language with no constant symbols, and let $L'$ be $L$ together with some constant symbols (finitely or infinitely many).

Let's say we have an $L'$-sentence $\varphi$, which mentions the constant symbols $c_1,\dots,c_n$ and no others. Then replacing each constant symbol $c_i$ with the fresh variable $x_i$ everywhere it appears in $\varphi$, we get an $L$-formula $\widehat{\varphi}(\overline{x})$. And the $L'$-sentence $\varphi$ is equivalent to the $L$-sentence $\exists \overline{x}\, \widehat{\varphi}(\overline{x})$, in the sense that an $L$-structure satisfies $\exists \overline{x}\, \widehat{\varphi}(\overline{x})$ if and only if it is a reduct of an $L'$-structure satisfying $\varphi$.

This is all well and good for a single sentence, but you run into some trouble when you try to do this for multiple sentences at once. When $\varphi$ and $\psi$ have some constant symbols in common, an $L'$-structure satisfying both $\varphi$ and $\psi$ is not the same as an $L$-structure satisfying both $\exists\overline{x}\,\widehat{\varphi}(\overline{x})$ and $\exists\overline{x}\,\widehat{\psi}(\overline{x})$. The reason is that the tuple witnessing the existential quantifiers in $\exists\overline{x}\,\widehat{\varphi}(\overline{x})$ is not required to be the same as the tuple witnessing the existential quantifiers in $\exists\overline{x}\,\widehat{\psi}(\overline{x})$.

OK, but we can fix this if we only care about finitely many sentences (i.e. a finitely axiomatizable theory). A model for the $L'$-theory $\{\varphi_1,\dots,\varphi_n\}$ is the same as a model for the $L'$-sentence $\bigwedge_{i=1}^m \varphi_i$, and this sentence is equivalent (in the sense above) to the $L$-sentence $\exists\overline{x}\,\bigwedge_{i=1}^m \widehat{\varphi_i}(\overline{x})$. What we did here was ensure that every instance of a each constant was handled by the same existential quantifier.

But most theories we care about are infinite. And you can't use the trick above for an infinite theory (at least not in first-order logic), because you can't form the infinite conjunction. The situation is even worse when you have infinitely many constant symbols, because you can't form an infinite block of existential quantifiers.