# A property of $\lt$ in Primitive recursive arithmetic

In Primitive recursive arithmetic (PRA), we can introduce $$\lt$$ by introducing its representing function $$K_{\lt}$$, where $$K_{\lt}(x,y) =sg(x+1-y)$$. Here "sg" and "-" are the functions defined by $$sg(0)=0\land sg(x+1)=1$$, $$pred(0)=0\land pred(x+1)=x$$ and $$a-0=a\land a-(b+1)=pred(a-b)$$.

In this situation, I want to prove in PRA that if $$K_{\lt}(x,y+1)=0$$, then $$K_{\lt}(x,y)=0\lor x=y$$.

If $$K_{\lt}(x,y+1)=0$$, then $$sg( (x+1)-(y+1))=sg(pred(x+1-y))=0$$. Note that by the induction axiom $$sg(x)=0\to x=0$$ and $$pred(x)=0\to x=0\lor x=1$$. Hence we have $$x+1-y=0\lor x+1-y=1$$. If $$x+1-y=0$$, then $$sg(x+1-y)=0$$, so $$K_{\lt}(x,y)=0$$.

But, I do not know how to prove in PRA with those recursive defining equations that if $$x+1-y=1$$, then $$x=y$$. Is is necessary to adopt this as a new axiom?

I konw that PRA is strong enough to prove the Gödel incompleteness theorems and many other logical consequnces, and these logical results are proved by introducing new primitive recursive functions with those recursive defining equations. In this point, I want to know whether those recursive defining equations are strong enough to deduce basic properties like "if $$x+1-y=1$$, then $$x=y$$".

• Keep working on the proof that if $x + 1 - y = 1$, then $x = y$. Try a few special cases first: e.g., $x = 0$ or $y = 0$. Try to build a proof up from simpler lemmas. If you continue to have problems, let us know what you have tried. Commented Jul 11 at 21:02
• thank you for the comment. I have proved it when $x=0$ or $y=0$. But I couldn't have the full proof. My attempt was using the induction axiom and those special cases, but I have no idea. Commented Jul 11 at 22:48

Given $$a \in \mathbb{N}$$, and primitive recursive $$f:\mathbb{N}\to\mathbb{N}$$, $$g:\mathbb{N}\to\mathbb{N}$$, $$h:\mathbb{N}^3\to\mathbb{N}$$ the function $$k:\mathbb{N}^2\to\mathbb{N}$$ is primitive recursive, where $$k$$ is defined by the equations: \begin{aligned} k(0,0) &= a \\ k(x+1, 0) &= f(x) \\ k(0, y+1) &= g(y) \\ k(x+1, y+1) &= h(k(x,y),x,y) \end{aligned} This is not exactly how Goodstein stated it but it is basically the same. Once you have this fact, statements like yours are much easier to prove!
• Thank you so much! If we define the $\lt$-representing function $K_{\lt}$ by using that diagonal recursion, then statements like "$K_{\lt}(x,y+1)=0$ implies $K_{\lt}(x,y)=0\lor x=y$" are easily provable. Is this your argument? Commented Jul 12 at 4:04