# Converting a FOL formula to a predicate only version

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.

• In either signature, what's $(x,y)$ supposed to mean? No $(-,-)$ predicate or function symbol exists in either signature... – Malice Vidrine Aug 14 '18 at 15:15
• @MaliceVidrine notice that it is $=(v_1, v_3)$, so the $=$ is the predicate symbol. – Eloo Aug 15 '18 at 6:39
• @Eloo: The reason why one uses the symbol $=$ rather than something else is that things are much easier to read if you write $t_1=t_2$ rather than ${=}(t_1,t_2)$. This convention is tacitly assumed whenever well-known binary relations/operators are said to be part of a logical language. (The underlying formalism does not change, it's just that we depict the symbol string "equals sign", "left parenthesis", something, "comma", something more, "right parenthesis" as "something $=$ something more" in human-readable text for ease of communication.) – Henning Makholm Aug 15 '18 at 10:06
• The prefix form is especially odd looking when there's no extra whitespace, and it looks like you're writing an odd variant of "$:=$", which is what I thought was happening. (You may think no one would ever write that, but...) – Malice Vidrine Aug 15 '18 at 15:07

## 1 Answer

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.