Suppose there are 2 signatures: $ \sigma_2= \{c, f^1, =^2 \}$ where $c$ is a constant, $f$ is a function symbol of arity 1, and $=$ is a predicate symbol of arity 2. Also, $\sigma_1 =\{R^2,P^1, =^2 \}$, where $R, P, =$ are all predicate symbols with their corresponding arities. Does there exist an algorithm that converts a formula A over $\sigma_2$ to a formula over $\sigma_1$ such that $ \vdash_{FOL}A \leftrightarrow \vdash_{FOL}A'$.
My idea was to replace different terms with variables, and conjoin predicate symbols in $A$ with a $\wedge$ so as if for example $A := =(c, f(f(c)))$, then $A':= =(v_1, v_3)\wedge P(v_1) \wedge R(v_1, v_2) \wedge R(v_2, v_3)$
I know that by this construction, one direction is satisfied, as we can choose $P$ to have 1 item and that will be the interpretation of $c$ in the satisfying model, and $R$ will be the same interpretation of $f$.
However, I am stuck in the other direction, as for example the relation $R$ in the satisfying model may not be a function and seems like it may cause problems, and in any way I tried thinking how to prove this direction with induction and failed.
Am I going in the right direction? Is there any more simple way to construct $A'$, maybe an algorithm such as this doesn't exist? But then, how is it possible to disprove it?
thanks.
edit: this question was in an exam by a different lecturer than mine, and after asking my TA about this happening in other questions the equality symbol here is agreed upon to be interpreted as the identity relation. I'll try to solve this again using this new info and update the question. Sorry for wasting your time.
Your idea goes in the right direction, yes. You do, however, need to quantify the new variables you introduce when you translate an atomic formula. Once you're assuming that $R$ and $P$ work like they "should", it will work to bind them all with $\exists$s.
For the other direction, where you have problems:
If you're interested in preserving satisfiability, you can take each full sentence $\psi$ and translate it to $$ (\forall x\exists! y\, R(x,y)) \land (\exists! y\, P(y)) \land \overline\psi $$ where $\overline\psi$ means $\psi$ with every atomic formula translated according to the scheme you've already found. Then your translated sentence can only be satisfied by structures where $R$ and $P$ behave correctly, such that you can convert the structure back to a structure in the original language.
However, here you're being asked to preserve provability, which is (well known to be) the same as validity. Then you need to translate to $$ \neg(\forall x\exists! y\, R(x,y)) \lor \neg(\exists! y\, P(y)) \lor \overline\psi $$ such that your translated sentence will automatically be satisfied in the "spurious" structured where $R$ is not functional or $P$ not unique.
If you're careful it is also possible to do everything in the translation of atomic formulas, so you don't need to special case the top level of the formula. An example of this (with a translation between another pair of languages) is shown here.