Let $\Sigma=\{R^2,=^2\}, \Sigma'=\{R^2,=^2,c\}$ be two signatures where $R$ is a binary relation, $=$ is the equality relation and $c$ is a constant.
Let $M$ be a model for $\Sigma$ and $b$ be such that $b\notin D^M$. We define $M'$ by:
- $D^{M'}= D^M \cup \{b\}$
- $c^{M'}=b$
- $R^{M'}=R^M \cup (\{b\}\times D^{M'}) \cup (D^{M'} \times \{b\})$
I would like to prove that there exists an algorithm, that given a closed formula $\psi$ over $\Sigma'$, it builds a closed formula $\varphi$ over $\Sigma$ such that $M\models \varphi$ iff $M'\models \psi$.
My problem is with removing $c$ from $\psi$. This is not just directly, for example, in the case that $R^M=\emptyset$ then $M'\models \exists xR(x,x)$ only because of the existence of $b$ in $D^{M'}$. So for this example, the translation of $ \exists xR(x,x)$ by the algorithm needs to be true in $M$. So that got me to the need that for every such relation $R$ in $\psi$ I need to add a subformula that will capture exactly that. One thing I have thought of is translating every $R(x,y)$ in $\psi$ to something of the sort: $$(R(x,y)\wedge x\ne c \wedge y \ne c)\vee (((x=c)\vee (y=c))\rightarrow R(c,c))$$ And then, I am left with translating $x=c$ in some way for every variable $x$ and $R(c,c)$. While $R(c,c)$ should be translated to a tautology, I didn't find a way to translate $c$ as part of the equalities.
Another approach was to utilize the fact that the signatures are pretty "weak", containing no functions and only one constant. I thought of translating it somehow to a formula above a signature with no equality, and then use Herbrand models. But I didn't manage to turn that into a solution.
Would appreciate any leads/hints/comments on this. Thanks!
We can describe the translation by induction on formulas. As usual, if you want to prove something about sentences (closed formulas) by induction on formulas, you need to formulate the correct generalization of the statement to arbitrary formulas.
Claim: For every $\Sigma'$-formula $\varphi'(x)$, there exists a $\Sigma$-formula $\varphi(x)$ such that for all $a\in M^x$, $M\models \varphi(a)$ if and only if $M'\models \varphi'(a)$.
If we prove this claim, then in the special case that $\varphi'$ is a sentence, there are no variables to interpret, so we get $M\models \varphi$ if and only if $M'\models \varphi'$.
Base case: Atomic formulas. There are several cases here.
$\varphi'(x)$ is atomic and doesn't mention the constant symbol $c$: Take $\varphi(x)$ to be equal to $\varphi'(x)$.
$\varphi'(x)$ is $x = c$ or $c = x$: Take $\varphi(x)$ to be $\bot$.
$\varphi'(x)$ is $c = c$: Take $\varphi(x)$ to be $\top$.
$\varphi'(x)$ is $R(x,c)$ or $R(c,x)$ or $R(c,c)$: Take $\varphi(x)$ to be $\top$.
If your syntax for first-order logic doesn't include $\top$ and $\bot$, you can use any $\Sigma$-formulas which are always true or always false, respectively. e.g. $\forall z\, (z = z)$ for $\top$ and $\exists z\, (z\neq z)$ for $\bot$.
Inductive steps:
$\varphi'(x)$ is $\psi'(x) \land \theta'(x)$: Take $\varphi(x)$ to be $\psi(x) \land \theta(x)$. Similarly for the other Boolean combinations (e.g. whichever of $\lor$, $\lnot$, $\rightarrow$, $\leftrightarrow$ is in your basic syntax).
$\varphi'(x)$ is $\exists y\, \psi'(x,y)$. This is the tricky one. The formula $\exists y\, \psi'(x,y)$ is equivalent to $(\exists y\, (y\neq c)\land \psi'(x,y)) \lor \theta'(x)$, where $\theta'(x)$ is $\psi'(x,y)$ with $c$ substituted for $y$. Now take $\varphi(x)$ to be $(\exists y\, \psi(x,y)) \lor \theta(x)$.
As usual, we only have to check the $\exists$ step, since we can rewrite $\forall$ as $\lnot \exists \lnot$.
Of course, you still have to verify (by induction, checking each step above) that this construction works.