2
$\begingroup$

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 it necessary to adopt this as a new axiom?

I know 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$" and even "If $pred(a)=1$, then $a=2$".

Improve this question
$\endgroup$
9
  • $\begingroup$ Crossposted: math.stackexchange.com/q/4944796/28111 $\endgroup$
    – Noah Schweber
    Commented Jul 12 at 0:53
  • $\begingroup$ Generally I recommend not cross-posting until at least a week has passed with no answer. $\endgroup$
    – Gerald Edgar
    Commented Jul 12 at 2:00
  • $\begingroup$ Could someone tell me whether we can make badly behaved nonstandard models of PRA as easily as for, say, Robinson's Q? In that theory you can just adjoin a point or two at infinity and make things strange. Does this method work in PRA as well? If so, the answer here will be negative. $\endgroup$
    – Joel David Hamkins
    Commented Jul 12 at 17:55
  • $\begingroup$ @JoelDavidHamkins Since PRA has induction + injectivity of successor, that shouldn't work. (More substantively, see Francois Dorais' answer at the MSE version.) $\endgroup$
    – Noah Schweber
    Commented Jul 13 at 5:12
  • $\begingroup$ @NoahSchweber Oh, I had thought that PRA specifically did not have induction. Isn't that the point of it, that it is weak that way? I thought we just have the recursive definitions of the primitive recursive functions, and that's it. Of course if you have induction then the whole question here is easy. (Meanwhile, having one point at infinity that is self-successor does not violate injectivity of successor, but you can't make a model of PRA this way, since the parity function won't work.) But how easily can we make nonstandard models of PRA? $\endgroup$
    – Joel David Hamkins
    Commented Jul 13 at 12:26

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .