Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I'm especially wondering about the order relation, subtraction, division and exponentiation here:

  • $x \leq y \quad \Leftrightarrow \quad \exists u\ y=x+u$
  • $z= x-y \quad \Leftrightarrow \quad x=y+z\lor (x\leq y \land z=0)$
  • $z=x/y \quad \Leftrightarrow \quad \exists u\ x+u=yz\land Su\leq y$
  • $z=x^y \quad \Leftrightarrow \quad E(x,y,z)$

I know that $E(x,y,z)$ can be defined for Peano arithmetic, but that any explicit formula for $E(x,y,z)$ is ridiculously complicated. Because Peano arithmetic and Robinson arithmetic have the same language, any formula for $E(x,y,z)$ which works for Peano arithmetic is also a valid formula for Robinson arithmetic.

These look like valid possible definitions for the requested predicates, so where is the problem? I'm pretty certain that exponentiation cannot be defined in Robinson arithmetic! This means that no matter which formula for $E(x,y,z)$ that works in Peano arithmetic I use, I won't be able to prove $E(x,y,z)\land E(x,y,z')\ \rightarrow\ z=z'$ in Robinson arithmetic.

I'm not sure whether there are definitions for subtraction and division for which it can be proved (in Robinson arithmetic) that the corresponding formulas define functions. I'm looking for a "clear definite" answer regarding this "uncertainty". I don't really believe that the usual order relation can be defined in Robinson arithmetic. The usual order relation would satisfy the following formulas:

  • $x\leq y \land y\leq z\ \rightarrow\ x\leq z$ (transitivity)
  • $x\leq y \land y\leq x\ \rightarrow\ x=z$ (antisymmetry)
  • $x\leq x$ (reflexivity)
  • $x\leq y \lor y\leq x$ (totality)

Clarification Here one might ask which of these properties have to be provable before we can claim that we defined "the usual order relation". Clearly transitivity and reflexivity cannot be waived. I wouldn't want to waive antisymmetry either if it can be avoided, because this condition is quite similar to the condition which shows that a predicate defines a function. There is no need to prove totality, because totality is not a "Horn property", and because the line has to be drawn somewhere.

In order to show that a predicate $P(x,y,z)$ defines a function, at least the condition $P(x,y,z)\land P(x,y,z')\ \rightarrow\ z=z'$ must be provable. It would be nice if $\exists z\ P(x,y,z)$ would be provable as well, but because this is not a "universal Horn property" and the line has to be drawn somewhere, it can be waived. Then we just have a partial function instead of a total function, but at least we still have a function.

Insight Asaf and Peter raise a very valid point, which I didn't even notice before. By which criteria do I decide that a predicate (given by an arbitrary first order formula in $Q$) corresponds to a certain natural number predicate? Peter suggests an answer, which I would slightly weaken such that it also applies to predicates which don't define functions. For $E(x,y,z)$ my condition reads

If $m^n = k$ then $Q \vdash E(\overline{m}, \overline{n}, \overline{k})$ and
if $m^n \neq k$ then $Q \vdash \lnot E(\overline{m}, \overline{n}, \overline{k})$

where $\overline{m}$ is $Q$'s formal numeral for $m$.

If it should turn out that some of the "harmless" natural number predicates can't be defined in Robinson arithmetic, then it would be interesting to know whether there is a conservative extension (="equiconsistent") of Robinson arithmetic where all canonical "harmless" natural number predicates can be defined. Exponentiation is not "harmless", because if $x$, $y$ and $z$ are binary encoded, the length of $z=x^y$ will be of the order $|x|y$, which is exponentially larger than $|x|+|y|$.

share|improve this question
I think you hit the hammer on the head with the remark about exponentiation. Everything that can be defined in $\Bbb N$ can still be defined if we consider it as a model of $\sf Q$ rather than $\sf PA$. The question should be whether or not any theory of arithmetic $T$ can prove that this predicate has the wanted properties, or not. For example Robinson arithmetic can't even prove that $Sx\neq x$ for all $x$. So maybe you should ask which predicates provably have their $\sf PA$ counterparts characteristics, but then you need to specify what characteristics you might be interested in, and so on –  Asaf Karagila Jul 12 at 13:09
So is part of this Question which order properties can be proven in Robinson arithmetic, starting from the definition of $x \le y$ given at top? –  hardmath Jul 12 at 13:33
@hardmath I tied to clarify this now. It turns out that I just want to know whether transitivity, reflexivity and antisymmetry can be proved for a suitable definition (by a first order formula in $Q$) of $x\leq y$. I'm quite convinced that this isn't possible for the definition given in the question, so either one has to come up with a definition for which this can be proved, or show that no such definition can exist. –  Thomas Klimpel Jul 12 at 17:43

1 Answer 1

Any explicit formula for $E(x,y,z)$ [in the language of PA] is ridiculously complicated.

Well, actually it's not that complicated! It is a tedious but easy exercise, once you've grasped how to use Gödel's beta-function (which itself can be written in primitive notation in half a line or so) to write down a candidate $E$ in primitive notation in a few lines.

Exponentiation cannot be defined in Robinson arithmetic!

Well, it depends what you mean by defined! Different authors mean different things by "define" (one of the mildly annoying things in this area is that is little consistency accross textbooks here).

Certainly, the following holds for $Q$ (Robinson Arithmetic): there is a formula $E(x, y, z)$ such that

if $m^n = k$ then $Q \vdash E(\overline{m}, \overline{n}, \overline{k})$ and

for every $m, n$, $Q \vdash \exists!zE(\overline{m}, \overline{n}, z)$

where $\overline{m}$ is $Q$'s formal numeral for $m$. And plenty of authors will call that defining (even "strongly defining") exponentiation. Indeed, in this sense, $Q$ can (initially surprisingly) define all the primitive recursive functions.

But yes, $Q$ is absolutely lousy at proving generalizations, and in particular (as I think you are pointing out)

$Q \nvdash \forall x\forall y\exists!zE(x, y, z)$

and so, $Q$ can't show that exponentiation is (as they say) a provably total function. Is this what you mean by defining?

Probably so: still, before proceeding further with your questions, we perhaps need an explicit statement of what exactly you mean by "definition" here.

share|improve this answer
Maybe it's time you write a book about these things! :-D –  Asaf Karagila Jul 12 at 17:43
Here is an explicit formula for $E(x,y,z)$. It's only 6 lines, but it uses abbreviations/auxiliary predicate definitions. But I agree that even if these abbreviations would be expanded, the resulting formula would still not be that complicated. –  Thomas Klimpel Jul 12 at 23:39
My initial expectation for a function "definition" (and my statement "...exponentiation cannot be defined in Robinson arithmetic!") were based on the requirements for eliminating an additional function symbol in the non-logical language by a suitably defined predicate (i.e. a first order formula). But because Robinson arithmetic seems to be unable to prove totality, it seems like a good idea to omit the totality requirement. (After all, some logics also have terms and function symbols without existential import. Totality isn't a "Horn property" either...) I updated the question accordingly. –  Thomas Klimpel Jul 12 at 23:43

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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