I know that in first order logic one can use (n+1)-ary predicates instead of n-ary function symbols to "simulate" a partial function. So, I'm loking for the axioms for real numbers field expressed using ternary predicates (es. sum(x, y, z)) instead of binary function symbols, but I did not find them. I found only formulation with function symbols.
Could you tell me where I could find them?
On
Translation can be made systematically:
To translate a preposition ultimately boils down to translating expressions that occur in equations or predicate parameters. The expressions can be constants, or variables, or the sum of two expressions, or the product of two expressions. Note the recursion introduced by the last two options.
To simplify the argument, we write equality $\alpha=\beta$ explicitly as a binary predicate $\operatorname{eq}(\alpha,\beta)$. Let $\Sigma$ and $\Pi$ be the ternary relations corresponsing to addition and multiplication, respectively.
As long as our statement contains a predicate that has at least one parameter that is neither a constant nor a variable, say $R(\ldots, \alpha,\ldots)$ where $\alpha$ is the sum $\beta+\gamma$ of two expressions $\beta,\gamma$ (or their product $\beta\cdot\gamma$ or more generally a $k$-ary function $f(\beta_1,\ldots, \beta_k)$ of $k$ expressions), we replace $R(\ldots, \alpha,\ldots)$ by $\exists t\;(\Sigma(\beta,\gamma,t)\land R(\ldots, t,\ldots)$ (or $\exists t\;(\Pi(\beta,\gamma,t)\land R(\ldots, t,\ldots)$ or $\exists t\;(\Phi_f(\beta_1,\ldots,\beta_k,t)\land R(\ldots, t,\ldots)$ with the $(k+1)$-ary relation $\Phi_f$ corresponding to the $k$-ary function $f$), where $t$ is a "new" variable. If you repeat this step, you will ultimately eliminate all functions (because the "complexity" of expressions occurring decreases with each step), i.e., all predicates will only be fed with constants and variables.
For example, the core equation of the axiom of distributivity $$ \tag1\forall a,b,c\colon a\cdot(b+c)=a\cdot b+a\cdot c$$ runs through the following translation stages $$\begin{align}\operatorname{eq}(a\cdot(b+c),a\cdot b+a\cdot c)\\ \exists t\colon \Pi(a,b+c,t)\land\operatorname{eq}(t,a\cdot b+a\cdot c)\\ \exists t,u\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\operatorname{eq}(t,a\cdot b+a\cdot c)\\ \exists t,u,v\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\Sigma(a\cdot b,a\cdot c,v)\land \operatorname{eq}(t,v)\\ \exists t,u,v,w\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\Pi(a,b,w)\land \Sigma(w,a\cdot c,v)\land \operatorname{eq}(t,v)\\ \exists t,u,v,w,s\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\Pi(a,b,w)\land\Pi(a,c,s) \land\Sigma(w,s,v)\land \operatorname{eq}(t,v)\\ \end{align}$$ This can be simplified, namely we can eliminate $v$ because it equals $t$: $$\exists t,u,w,s\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\Pi(a,b,w)\land\Pi(a,c,s) \land\Sigma(w,s,t).$$ Putting this back in the context of $(1)$, we finally have $$\forall a,b,c\;\exists t,u,w,s\colon \Sigma(b,c,u)\land\Pi(a,u,t)\land\Pi(a,b,w)\land\Pi(a,c,s) \land\Sigma(w,s,t). $$
Why not take an existing set of axioms and translate them? For example, associativity of addition:
$$ \forall x,y,z\; (x+y)+z=x+(y+z) $$
could be written as
$$ \forall x,y,z,s,t,u\; (sum(x,y,s) \wedge sum(s,z,t) \wedge sum(y,z,u) \implies sum(x,u,t))$$