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$.


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.

  • $\begingroup$ Thank you for you informative response! About the example: $f(x)+3<=f(5)$- $x$ is a free variable, does $y_1$ should be free as well? Or under $\exists$ quantifier. I can't decide whether this is even matter. And for the correctness, I should define inductively the translation, and then proof by structure induction the correction? $\endgroup$
    – Ella
    Jun 20 at 9:08
  • $\begingroup$ And one more question, can I do a similar thing with relations? Namely, replace relation with function from the domain to {0,1}? I've tried to do such thing, but ran into difficulties in the proof, so I taught maybe relations can't be represented as functions. $\endgroup$
    – Ella
    Jun 20 at 10:38
  • $\begingroup$ All newly introduced variables must be bound by quantifiers. Regarding functions, I take it you want to replace relations with functions to the codomain $\{0,1\}$ (and not "from the domain $\{0,1\}$" as you stated). You cannot do that in first-order logic, except in limited cases, because there is no way to encode the quantifiers in general. $\endgroup$ Jun 20 at 14:00
  • $\begingroup$ What is the exact problem with the translation of $R(x,y)$ to $R_{=}(f(x,y)=1)$? I taught that the problem is with the element that should represent truth value ( I mean 0,1). $\endgroup$
    – Ella
    Jun 20 at 15:50
  • $\begingroup$ Suppose $Q(x,y) \iff g(x,y) = 1$ and $\forall x, y . g(x,y) = 0 \lor g(x,y) = 1$, i.e., the function $g$ represents the relation $Q$. What function represents the predicate $\forall x . Q(x,y)$? $\endgroup$ Jun 20 at 19:07

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)))$$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.