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?


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).

  • $\begingroup$ Thank you so much for the detailed answer! Just to clarify: so if we fix the set of predicates and variables in our signature, then the language of first-order logic with constants would be strictly more expressive than the language of first-order logic without constants (because there are no ways to translate the individual constants into a language without constants such that $p(c_i)\not\vDash p(c_j)$ for $i\neq j$ comes out true)? $\endgroup$ – discretizer Jul 25 '18 at 13:55
  • $\begingroup$ @discretizer: Generally the only thing that would happen is that you'd need a more complex translation than this one, expressing the constants you remove by co-opting some of the predicates you still have. As long as there's a single binary predicate or a single binary function left in the language, it is still possible to find a translation for the full pure predicate calculus (with a countable infinitely of constants, functions and predicates of every arity). However, if you restrict yourself to unary functions and predicates, then you do lose expressivity. $\endgroup$ – Henning Makholm Jul 25 '18 at 14:51
  • $\begingroup$ ah yes. sorry I overlooked the hilbert-map argument using existing symbols). Many thanks again. $\endgroup$ – discretizer Jul 25 '18 at 15:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.