How to prove $n\leq x \rightarrow x = n \vee Sn \leq x$ using Robinson Arithmetic

Given the definition $n \leq x \Leftrightarrow \exists y \ni y+n=x$, how can one prove $n\leq x \rightarrow x = n \vee Sn \leq x$ in Robinson Arithmetic? I think this should be a proof by induction, though I'm not sure, and I can't even prove the base case $0 \leq x \rightarrow x=0 \vee 1 \leq x$. Note: in this formula, $n$ denotes a successor of 0, and $x$ an arbitrary element of the model. As shown by one the answers, statement is false if we allow $n$ to be an arbitrary element.

Expansion/Clarification. I am a novice at logic (at least at this level), but I am reading An Introduction to Goedel's Theorems by Peter Smith. The exact claim is that for any natural number (i.e, $0$ sucessor) $n$, $Q \vdash\forall x (n\leq x \rightarrow (x = n \vee Sn \leq x))$, along with with several other properties about $\leq$ in $Q$. So this is perhaps a `meta-theorem' as mentioned in the comments. The text asserts these properties are "trivial but are a bit tiresome to prove", and leaves several of them as exercises to the reader. This particular property has turned out to be not so trivial for me.

• Robinson Arithmetic doesn't have induction. Just a very weak form. (As Henning reminded me) – Thomas Andrews Aug 19 '17 at 19:11
• @ThomasAndrews: In this statement $n$ probably stands for a numeral (that is, a term of the form $SS\cdots SS0$), so saying that it holds for all numerals is really a meta-theorem that we can prove by using induction over $n$ at the metalevel. – Henning Makholm Aug 19 '17 at 20:57
• @HenningMakholm I think you're right, as I found a non-standard model in which the statement expressed as a universally quantified logic statement is false. – Bram28 Aug 20 '17 at 16:59

(I am looking at Wikipedia page on Robinson Arithmetic)

Hmmm, I run into a difficulty as well: how to go from $a + s(d) = b$ to $s(a) + d = b$ Aha! As I suspected ... you cannot prove $\forall x \forall y \ s(x) + y = x + s(y)$ in Robinson Arithmetic, and thus the proof above cannot be completed. In fact, your statement $\forall x \forall y (x \le y \leftrightarrow (x = y \lor s(x) < y))$ cannot be proven in Robinson Arithmetic in any way. Below is a non-standard model $M$ that satisfies all the axioms of Robinson Arithmetic, but in which these two specific claims are false:

Domain

$D^M = \{ q_0, q_1, q_2, q_3, d_0, d_1, d_2, ... \}$ (in other words, a countably infinite number of objects $d_i$ that of course serve the role of the natural numbers as intended, plus 4 more objects)

$0^M = d_0$

Interpretation of successor function

$s^M(q_0) = q_1$

$s^M(q_1) = q_0$

$s^M(q_2) = q_3$

$s^M(q_3) = q_2$

$s^M(d_i) = d_{1+1}$

This will satisfy axiom 1 ($d_0$ is not the successor of any object), axiom 2 (no two different objects have the same successor), and axiom 3 (every object other than $d_0$ has a predecessor (i.e is the successor of some other object).

Interpretation of addition function

(rows are left argument, columns right argument, e.g $q_0 +^M q_1=q_1$ and $q_1 +^M q_0=q_0$)

\begin{array}{c|cccccccc} & q_0 & q_1 & q_2 & q_3 & d_0 & d_{2k+1} & d_{2k+2}\\ \hline q_0 & q_0 & q_1 & q_2 & q_3 & q_0 & q_1 & q_0\\ q_1 & q_0 & q_1 & q_2 & q_3 & q_1 & q_0 & q_1\\ q_2 & q_2 & q_3 & q_2 & q_3 & q_2 & q_3 & q_2\\ q_3 & q_2 & q_3 & q_2 & q_3 & q_3 & q_2 & q_3\\ d_0 & q_0 & q_1 & q_2 & q_3 & d_0 & d_{2k+1} & d_{2k + 2}\\ d_{i+1} & q_2 & q_3 & q_2 & q_3 & d_{i+1}& d_{2k+1+ i+1} & d_{2k+2+i+1}\\ \end{array}

This will satisfy axiom 4 ($x +^M d_0 = x$ for any object $x$) and axiom 5 ($\forall x \forall y x + s(y) = s(x + y)$ ... this is a bit tedious to verify)

Interpretation of multiplication function

(rows are left argument, columns right argument, e.g $q_0 \cdot^M q_1=q_1$ and $q_1 \cdot^M q_0=q_0$)

\begin{array}{c|ccccccc} & q_0 & q_1 & q_2 & q_3 & d_0 & d_{i+1}\\ \hline q_0 & q_0 & q_0 & q_0 & q_0 & d_0 & q_0\\ q_1 & q_1 & q_1 & q_1 & q_1 & d_0 & q_1\\ q_2 & q_2 & q_2 & q_2 & q_2 & d_0 & q_2\\ q_3 & q_3 & q_3 & q_3 & q_3 & d_0 & q_3\\ d_0 & q_0 & q_0 & q_2 & q_2 & d_{2k} & d_{2k+1}\\ d_{2k+1} & q_2 & q_3 & q_2 & q_3 & d_{2k+1} & d_{2k+1+i+1}\\ d_{2k+2} & q_2 & q_2 & q_2 & q_2 & d_{2k+2} & d_{2k+2+i+1}\\ \end{array}

This will satisfy axiom 6 ($x \cdot^M d_0 = d_0$ for any object $x$) and axiom 7 ($\forall x \forall y x \cdot s(y) = (x \cdot y) + x$ ... this is again tedious to verify)

OK, but now notice that:

$s(d_0) +^M q_0 = d_1 +^M q_0 = q_2$, but $d_0 +^M s(q_0) = d_0+^M q_1 = q_0$, so $\forall x \forall y \ s(x) + y = x + s(y)$ is false in this model.

Also notice that while $d_0 \le q_0$ is true since $\exists z d_0 + z = q_0$ is true (simply choose $z = q_0$), $d_0 = q_0 \lor s(d_0) \le q_0$ is false, since $d_0 \not = q_0$ and since $s(d_0) = d_1$, and there is no $z$ such that $d_1 + z = q_0$. So, $\forall x \forall y (x \le y \leftrightarrow (x = y \lor s(x) < y))$ is also false in this model.

• Yes, if I could prove $Sa+b=a+Sb$, I think I would have produced at least three proofs by now. It might (or might not) be related to the fact your $a$ (might $n$) is a 0-sucessor. I've clarified that fact in the question. – Itai Seggev Aug 19 '17 at 20:59
• @ItaiSeggev I know that without the axiom of induction there are all kinds of non-standard models. For example, without induction you cannot prove commutativity of addition, for there is a non-standard model where addition is not commutative. I suspect that's the problem here as well; without induction you simply can't prove Sa + b = a + Sb ... and possibly your very theorem either. – Bram28 Aug 19 '17 at 23:49
• @ItaiSeggev Yes! I found a non-standard model for RA in which both Sa+ b = a +Sb and your claim do not hold, so they are indeed not provable, as I suspected! It's a bit of a big model ... maybe I'll have some time tomorrow to post it. Anyway, you can stop trying to prove these claims from within RA since you'd be trying the impossible! – Bram28 Aug 20 '17 at 3:40
• Hmm, by your addition table I get $s(d_0+q_0)=s(q_0)=q_1$ but $d_0+s(q_0)=d_0+q_1=q_0$. I suspect $d_0+q_1$ should have been $q_1$... and $d_1+q_3$ should have been $q_3$? – Henning Makholm Aug 20 '17 at 17:12
• @HenningMakholm Yes, good eyes! – Bram28 Aug 20 '17 at 17:33

For the case $n=0$, we will use that $\forall x\left(x=0\lor \exists y (x=Sy)\right).$

Then $x=0\implies \left(x=0\lor 1\leq x\right)$.

And $\left(\exists y (x=Sy)\right)$ implies $\exists y (x=y+1)$ or $1\leq x$.

So we conclude that since $\forall x\left(x=0\lor \exists y (x=Sy)\right)$, that $$\forall x(x=0\lor 1\leq x)$$ I'll leave the general $n$ to you.

• It's good that you don't need the induction hypothesis, because Robinson Arithmetic does not have induction at all! All you get is $y=0\lor \exists x:y=Sx$. – Henning Makholm Aug 19 '17 at 19:04
• Ah, I was unaware of that. @HenningMakholm – Thomas Andrews Aug 19 '17 at 19:05
• I see. So we fix a general $n$ which is $n$ applications of $S$ to $0$, and suppose $n\leq a$. Which means $v+n=a$. By $n$ applications of axiom 5 follow by one of axiom 4, $S\ldots Sv = a$. But then applying the same argument as above, either $v=0\rightarrow n=a$, or $v = Sy$. But now $a$ is $n+1$ appliactions of $S$ to $y$, so reversing axiom 5 $n+1$ times gives $y + (n+1)=a$, or $Sn\leq a$. Does that sound right? – Itai Seggev Aug 20 '17 at 3:40

I think both other answers each capture a piece of the overall picture. Having studied more and advanced in the book, I've arrived at the following resolution.

As pointed out in the other answers, it is not the case that $\forall y (y \leq x \rightarrow (y=n \vee Sy < n)$, though you'd need non-standard numbers to get there. Also, $Q$ doesn't have induction, so we're not going to do an argument by induction. Instead, we'll do the following meta-proof. We fix $n\in\mathbb{N}$, and let $\bar{n}=\underset{n~\textrm{times}}{S \ldots S} \bar{0}$ be the represent of $n$ in our system. We then have $$\bar{n} \leq x\leftrightarrow \exists v\left(v+\bar{n}=v+\underset{n~\textrm{times}}{S \ldots S} \bar{0}=x\right).$$ But working with the middle expression, we have $$v+\underset{n~\textrm{times}}{S \ldots S}\bar{0}=Sv+\underset{n-1~\textrm{times}}{S \ldots S}\bar{0}=\ldots = \underset{n~\textrm{times}}{S \ldots S}v+\bar{0}=\underset{n~\textrm{times}}{S \ldots S}v,$$ where the first $n$ equalities are applications of axiom 5 and the last but axiom 4. Now, we invoke axiom 3: $v = 0 \vee \exists y (v=Sy)$ and argue by cases. If $v=0$, we immediately have $x = \underset{n~\textrm{times}}{S \ldots S}\bar{0} = \bar{n}$. Otherwise, we have $$x =\underset{n~\textrm{times}}{S \ldots S}\left(Sy\right) = \underset{n+1~\textrm{times}}{S \ldots S}y + \bar{0}= \underset{n~\textrm{times}}{S \ldots S}y+S\bar{0} = \ldots = y + \underset{n+1~\textrm{times}}{S \ldots S}\bar{0} = y +S\overline{n}.$$ (The first equality is a combination of axioms 2 and 3, next $n$ axiom 5, and the last by definition of $\overline{n}$ and axiom 2). But the existence of such a $y$ of course means that $S \bar{n}\leq x$. Hence $x = n \vee Sn \leq x$. Q.E.D.