I recently had to explain how the basic axioms in Simpson's *Subsystems of Second Order Arithmetic* were interpretable in Robinson's Q. Most of the axioms are actually the same, except that Simpson includes an ordering relation $\lt$ with the axioms
$$\lnot(m \lt 0)$$
and
$$m \lt n + 1 \leftrightarrow m \lt n \lor m = n.$$
(Perhaps I shouldn't call it an "ordering relation" since the axioms are too weak to prove that it is transitive.) Though some flavors of Robinson's Q include an ordering relation, it is usually simply defined in terms of addition. In my explanation, I instinctively defined $m \lt n$ to mean $\exists k(n = m + (k + 1))$ and proceeded to show that this relation satisfies Simpson's two axioms.


I later tried to find a reference for this simple fact. To my dismay, it appears that the usual way to define the ordering relation in Robinson's Q is the other way around. For example, Hájek and Pudlák define $m \leq n$ as $\exists k(n = k + m)$ in *Metamathematics of First-Order Arithmetic*. Sadly, this variant doesn't work for the purpose above. In fact, I've convinced myself that while they all satisfy the first axiom, mine is essentially the only variation on the theme that satisfies the second axiom.


I haven't checked every source but I haven't found any that use my version of the ordering relation. This is not a serious problem since all variants work equally well for the ordering of standard natural numbers and all variants agree once a very mild amount of induction is added to the picture. Nevertheless, I'm puzzled:


1. Is there any source that uses my definition of the ordering relation?
2. Is there any technical reason to prefer the other way of defining the ordering relation?



The definition of < in Robinson's Q
1. I can’t give you a source from the top of my head, but I’m pretty sure that all obvious variants of the definition of ordering in Q appear *somewhere*.
2. The technical advantage of the definition in Hájek and Pudlák is that it provably satisfies
$$x\le\overline n\lor\overline n\le x$$
for every standard $n$, which is used in the canonical proof of representability of recursive functions in Q (though this can actually be circumvented) and in various Rosser-style arguments. The reverse definition does not have this property, as Q does not even prove that every nonzero $x$ is of the form $0+y$.


