# Find the representation in Peano system

It's known that all recursive functions are representable in Peano arithmetic. I am trying to find representation of subtraction function

$f(x,y)= \left\{\begin{matrix} x-y &if& x>y\\ 0 & if& x \leq y \end{matrix}\right.$

I think its representation formula is $R(x,y,z) \leftrightharpoons (x>y\Rightarrow x+z=y) \wedge (x\leqslant y \Rightarrow z=0)$. I have to show that

1) If $f(a,b)=c$ then $\vdash R(a,b,c)$

2) $\vdash\exists _{1}z R(x,y,z)$

How to show it?

-

Proof sketch

(1) is straightforward. Argue by cases.

If $f(a, b) = 0$, then not-($a > b$). So $PA \vdash \neg(\overline{a} > \overline{b})$ (why?) and hence $PA \vdash \overline{a} > \overline{b} \to \overline{a} + \overline{c} = \overline{b}$. Also $PA \vdash \overline{0} = \overline{0}$ and hence $PA \vdash \overline{a} \leq \overline{b} \to \overline{0} = \overline{0}$. Putting things together, $PA \vdash R(\overline{a}, \overline{b}, \overline{c})$.

Similarly if $f(a, b) = c$, $c > 0$, then $a + c = b$ and so $PA \vdash \overline{a} + \overline{c} = \overline{b}$ hence $PA \vdash \overline{a} > \overline{b} \to \overline{a} + \overline{c} = \overline{b}$. Also not-$a \leq b$, so $PA \vdash \neg(\overline{a} \leq \overline{b})$ hence $PA \vdash \overline{a} \leq \overline{b} \to \overline{c} = \overline{0}$. Putting things together again, here too $PA \vdash R(\overline{a}, \overline{b}, \overline{c})$.

(2) Query: Are you sure you want to show $PA \vdash\exists _{1}z R(x,y,z)$ rather than the more usual $PA \vdash\exists _{1}z R(\overline{a},\overline{b},z)$?

Anyway, to show (2), prove existence and uniqueness separately. I'll leave existence as an exercise.

For uniqueness, assume $R(x, y, z)$ and $R(x, y, z')$. Argue in $PA$ by cases from $x > y \lor x \leq y$. The first disjunct gives $x + z = y$ and $x + z' = y$ and you need to show (or assume) that those entail $z = z'$. The second disjunct gives $z = 0$ and $z' = 0$ and so $z = z'$. So either way $z = z'$, which completes the proof.

-