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?
  • $\begingroup$ The Wikipedia article suggests the same procedure: en.wikipedia.org/wiki/… $\endgroup$ – Christian Remling Jul 24 '14 at 17:36
  • $\begingroup$ @ChristianRemling: I noticed that too but according to Google books, Burgess actually suggests defining $x \lt y$ as $\exists z(z' + x = y)$. I haven't read the book though, so I'm not sure about the context. $\endgroup$ – François G. Dorais Jul 24 '14 at 17:45
  • 2
    $\begingroup$ @FrançoisG.Dorais: Whatever the reasons might be for preference of one definition over another, Wikipedia is supposed to agree with its sources, so I fixed the definition there. $\endgroup$ – Emil Jeřábek Jul 24 '14 at 20:58
  • $\begingroup$ François: the following reference would be of interest to you in connection with interpreting second order systems in Q, but perhaps you know of it already: Ferreira, Fernando; Ferreira, Gilda Interpretability in Robinson's Q. Bull. Symbolic Logic 19 (2013), no. 3, 289–317. $\endgroup$ – Ali Enayat Jul 26 '14 at 16:34
  • $\begingroup$ Thanks for the pointer @AliEnayat, I wasn't aware of that very nice paper. $\endgroup$ – François G. Dorais Jul 28 '14 at 14:41
  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$.

  • $\begingroup$ I might also mention that while the $\exists z\,(z+x=y)$ definition (which, BTW, comes from the original Tarski–Mostowski–Robinson paper) does not Q-provably satisfy Simpson’s axioms, it satisfies a different inductive definition of ordering: $$\begin{align}0&\le y\\Sx&\nleq0\\Sx&\le Sy\leftrightarrow x\le y\end{align}$$ $\endgroup$ – Emil Jeřábek Jul 25 '14 at 10:12
  • $\begingroup$ Thanks Emil! That makes a lot of sense. I guess everybody is just following the original definition. $\endgroup$ – François G. Dorais Jul 25 '14 at 12:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.