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:
- Is there any source that uses my definition of the ordering relation?
- Is there any technical reason to prefer the other way of defining the ordering relation?