7
$\begingroup$

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?
Improve this question
$\endgroup$
5
  • $\begingroup$ The Wikipedia article suggests the same procedure: en.wikipedia.org/wiki/… $\endgroup$
    – Christian Remling
    Commented Jul 24, 2014 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
    Commented Jul 24, 2014 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
    Commented Jul 24, 2014 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
    Commented Jul 26, 2014 at 16:34
  • $\begingroup$ Thanks for the pointer @AliEnayat, I wasn't aware of that very nice paper. $\endgroup$
    – François G. Dorais
    Commented Jul 28, 2014 at 14:41

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\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
    Commented Jul 25, 2014 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
    Commented Jul 25, 2014 at 12:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .