Problem with formalism in first order logic

Question

This is a general question in first order logic.
Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols).
I want a new alphabet, $\Sigma'$, which is the same as the original, except that the function $f$ will be replaced by a new binary relation $R_f$.
I ran into difficulties when I tried to formulate it. For example, for formulas as: $R(x,f(x))$, I need to replace $f(x)$ but I don't know how exactly.

In general, I couldn't find a way that accurately defines a new formula, such that: the new formula will be satisfied above $\Sigma'$ iff the original formula was satisfied $\Sigma$.

Answer 1

What you are looking for is replacing a function symbol $f$ with the corresponding graph, which is the relation $R_f$ characterized by $R_f(x,y) \iff f(x) = y$.

So we can replace $f(x) = y$ with $R(x,y)$ if $x$ and $y$ are variables. But what do we do about $f(t)$ where $t$ might contain futher occurrences of $f$? That's the tricky bit.

The idea is to use intermediate equations, for instance $$f(f(x)) = f(f(f(y)))$$ can be replaced with $$ \exists x_1, y_1, y_2, y_3. f(x) = x_1 \land f(y) = y_1 \land f(y_1) = y_2 \land f(y_2) = y_3 \land f(x_1) = y_3 $$ which in turn is replaced with $$ \exists x_1, y_1, y_2, y_3 . R_f(x, x_1) \land R_f(y, y_1) \land R_f(y_1, y_2) \land R_f(y_2, y_3) \land R_f(x_1, y_3). $$ We can use a similar trick even if some other symbols and relations are present. For example $$f(x) + 3 \leq f(5)$$ translates to $$\exists y_1, y_2 . R(x,y_1) \land R(5, y_2) \land y_1 + 3 \leq y_2.$$ It is a good exercise to spell out the precise procedure after you've learned the trick, but let me know if you'd like more details.

Answer 2

You can always find a relation to replace any total or even partial function albeit it inevitably complicates the original wff with additional quantifiers and conjuncts, so usually you'd much better off with more generic and flexible function symbols defined in your alphabet $\Sigma$. However, a relation symbol cannot be replaced with only function symbol(s) in general in first order languages because function symbol is used to get terms corresponding to grounded objects in the domain of discourse and truth values are never grounded objects in the object language.

Now for your specific question to translate the formula $R(x, f(x))$ using only $R_f$. For simplicity the first case assumed here is that your function $f$ is total and per your function replacement $R_f$ assumption we can derive in a formal system:

$$\forall x \exists! y (f(x)=y \rightarrow R_f(x, y)) \vdash \forall x(R(x, f(x)) \rightarrow \exists! y (R(x, y) \land R_f(x, y)))$$

, where $\exists!$ is just a shorthand for the unique existence quantifier which can be replaced using a more complicated formula by adding a universally quantified conjunction.

Now for the second case where your original function $f$ is partial, then we can have a similar derivation in the same formal system:

$$\exists x \exists! y (f(x)=y \rightarrow R_f(x, y)) \vdash \exists x (R(x, f(x)) \rightarrow \exists! y (R(x, y) \land R_f(x, y)))$$

Or if you know $f$ is undefined at $p$, for example, then you can derive below: $$\forall x \exists! y (x \neq p \land f(x)=y \rightarrow R_f(x, y)) \vdash \forall x(x \neq p \land R(x, f(x)) \rightarrow \exists! y (R(x, y) \land R_f(x, y)))$$