Let two languages $\Sigma_1 = \{R^2, P^1, =^2\}$ and $\Sigma_2 = \{c, f^1, =^2\}$. Prove or disprove: There's an algorithm (procedure that halts) which gets as an input a formula $A$ above $\Sigma_2$ and builds a formula $A'$ above $\Sigma_1$ such that $A$ is valid iff $A'$ is valid.
One can see that the terms of $\Sigma_2$ are $\{c,f(c),f(f(c)),\ldots \}$. Moreover, the only operation we can do on them is to "compare" them (I used the quotation marks since it doesn't have to be the equality relation, it's just a symbol!).
Now, in $\Sigma_1$ we have a binary relation, $R^2$ and a function is basically a special binary relation.
With that in mind, I think there is an algorithm but I am lacking the ability I guess to come up with such an algorithm.
I'd be glad for suggestions.
Thanks.
Hint: Take $R(x, y)$ to denote $f(x) = y$ and take $P(x)$ to denote $x = c$. For formulas like $f(f(x)) = y$, use existential quantification to specify the intermediate value $f(x)$.