4
$\begingroup$

Hello my question is related to Why is it impossible to define multiplication in Presburger arithmetic? and to How is exponentiation defined in Peano arithmetic?. I would have preferred to add it as a comment to one of the above discussions but I don't have commenting powers yet :-( Anyway, when I look at the answer to how exponentiation is defined, using sequences and the Chinese remainder theorem, I assume that Presburger is simply not powerful enough to play the same trick to define $\times$ in terms of +?

thanks

$\endgroup$
7
  • $\begingroup$ The proof that exponentiation is Diophantine is weirdly technical and off-putting, but it is the reason. $\endgroup$ Jan 25, 2015 at 1:58
  • $\begingroup$ Specifically, there is a polynomial $f(x,y,z,w_1,w_2,\dots,w_n)$ such that for any $(x,y,z)\in\mathbb N$, $\exists w_1,w_2,\dots,w_n$ yielding a solution to $f$ if and only if $x^y=z$. That's a deep and weird result. Note that a polynomial can be expressed in terms of sum and product only: $x^3+3xy+z=x\cdot x\cdot x + 3\cdot x\cdot y + z$. $\endgroup$ Jan 25, 2015 at 2:01
  • $\begingroup$ Once you've defined ore assumed $+$ and $\times$, you can define exponentiation without encodings or the like using this result. @CarlMummert $\endgroup$ Jan 25, 2015 at 2:08
  • $\begingroup$ @CarlMummert Having read the proof that exponentiation is Diophantine, I saw nowhere in it that it assumed a particular model. Maybe I'm wrong. $\endgroup$ Jan 25, 2015 at 2:12
  • $\begingroup$ Sigh, no, you just need to prove that the triples $(x,y,z)$ satisfy the recursive definition of triples satisfying it, including that it is single-valued. You don't need to already have exponentiation defined in the structure. @CarlMummert $\endgroup$ Jan 25, 2015 at 2:17

1 Answer 1

2
$\begingroup$

Yes, Presburger arithmetic is not strong enough to quantify over sequences, which is the reason it can't define multiplication.

$\endgroup$

You must log in to answer this question.

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