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

Question

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.

Answer 1

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.

Answer 2

(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$

ADDENDUM

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.

Answer 3

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.