Is first-order logic with constants equally expressive as first-order logic without constants

first-order-logiclogicmodel-theory

I define a logic as a set of formulas $\mathcal{L}$ (formulated in some given signature) with a consequence relation $\vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a conservative translation from $L_1$ to $L_2$, i.e.~there is $t: \mathcal{L}_1\rightarrow\mathcal{L_2}$ such that $\Gamma\vDash_1\varphi$ iff $t(\Gamma)\vDash_2t(\varphi)$. Consider $\mathcal{L}_{con}$, the language of first-order logic with denumerably many constants, and $\mathcal{L}$, the language of first-order logic with no constants. I suspect that these two languages are equally expressive. In particular, we can translate any formula with constants in $\mathcal{L}_{con}$ to a formula with only variables in $\mathcal{L}$, with the restriction that different constants are mapped to different variables. So for instance, $F(c_1,c_2)\mapsto F(x_1,x_2)$. Is this right?

I guess a more fundamental question is that I do not have a firm grasp of how to prove properties of translations. I suppose that, given the soundness and completeness of first-order logic, one could induct on the complexity of proofs. But this seems rather tedious and does not extend to logics that are known to be incomplete. Is there a canonical way of proving equal expressiveness (or equivalently, the existence of a conservative translation) between any two logics?

Best Answer

Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example $$ p(x) \vDash p(y) \qquad\text{but not}\qquad p(c_0) \vDash p(c_1) $$ because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.

You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate

  • each constant $c_n$ as $f_n(0)$;
  • all other parts of terms remain unchanged;
  • each atomic formula $p(t_1, \ldots, t_n)$ as $$ \neg \exists 0\Bigl (Z(0) \land \forall x(Z(x)\to x=0) \land \neg p(t[t_1],\ldots,t[t_n]\Bigr); $$
  • and all connectives and quantifiers remain themselves

I hope this qualifies for your concept of a translation $\mathcal L_1\to\mathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $\{0,Z,f_n\}$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.

Suppose that for some $\Gamma$, $\varphi$ we have that $t(\Gamma) \vDash_2 t(\varphi)$ and for some model $\mathfrak M$ we have $\mathfrak M\vDash_1 \Gamma$. Then we can construct a new $\mathfrak M_2$ by selecting a single of $\mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^{\mathfrak M_2}$ map everything to $(c_n)^{\mathfrak M}$ for each $n$.

Then $\mathfrak M_2\vDash_2 t(\psi)$ exactly if $\mathfrak M\vDash_1 \psi$. Now since $\mathfrak M\vDash_1 \Gamma$ we have $\mathfrak M_2\vDash_2 t(\Gamma)$ and then by assumption $\mathfrak M_2 \vDash_2 t(\varphi)$ and then $\mathfrak M\vDash_1 \varphi$.

Conversely, suppose $\Gamma \vDash_1 \varphi$ and we have some $\mathfrak M \vDash_2 t(\Gamma)$. Then,

  • either there is a unique $m_0\in\mathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $\mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^{\mathfrak M_1}$ be $f^{\mathfrak M}(m_0)$ -- such that $\mathfrak M_1\vDash_1 \psi$ iff $\mathfrak M\vDash_2 t(\psi)$.
  • or there is no such element, in which case the translation of every atomic formula is true in $\mathfrak M$ for all values of the variables. In that case let $\mathfrak M_0$ be the model with a single element where all predicates are true; then $\mathfrak M_0\vDash_1 \psi$ iff $\mathfrak M\vDash_2 t(\psi)$.

(The negations in the translation of atomic formulas are there to allow $\mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).

Related Question