Doing math with nonstandard numbers

Question

Assume we have a computable, nonstandard model of Robinson arithmetic consisting of the set of integer-coefficient polynomials with positive leading coefficient, plus the zero polynomial, with their usual arithmetic.

Consider the formula

$\sum_{i=0}^{n} i = \frac{n^2 + n}{2}$

Is this formula valid in this model? Let $|2x|$ be the nonstandard natural number represented by the polynomial $2x$. In this model, is the sum of all natural numbers from $|0|$ through $|2x|$ equal to $|2x^2+x|$? If so, does this mean some hyper-finite sums are undefined? For example, the sum of $|0|$ through $|x|$ would be $\frac{x^2 + x}{2}$, which doesn't exist in this model.

---

I am not asking if Robinson arithmetic can prove this statement. I want to know if it is "true" in this model with the simple lexicographical mapping of polynomials to natural numbers. Would a strong meta-theory like ZFC prove these "finite" sums, in this model, are equal to values predicted by this formula when the sums exist?

Answer 1

Elaborating on Andre Nicolas' comment: Try to write down the sentence $$\mbox{"For all $n$, $\sum_{i=1}^ni={n^2+n\over 2}$"}$$ in the language of Robinson arithmetic. There isn't really any way to define an arbitrary summation. For a concrete example, how would you express $$\sum_{i=1}^{X^2+17X-3}i$$ in the language of Robinson arithmetic?

Now, stronger theories such as PA can talk about numbers which code sequences, and can prove the basic facts about these, so that we can legitimately use abbreviations like "$\sum_{i=1}^n$".

EDIT: Specifically, we write "$\sum_{i=1}^n=x$" as shorthand for "There is a number $y$ which codes a sequence of length $n$, such that the first term of that sequence is $1$, the last term is $x$, and for each $k<n$, the $(k+1)$th term is the $k$th term plus $k+1$." Note that proving that such a $y$ exists for every $n$ and $x$ requires induction - which Robinson arithmetic lacks! Also note that even referring to sequences requires a lot of work in the absence of exponentiation, and while the Godel machinery for doing this (via the Chinese Remainder Theorem) goes through in Robinson, seemingly basic facts about sequences so represented will not.

We can make the same definitions in Robinson arithmetic (since the language is the same); however, we can't prove even very basic claims - such as that "$\sum_{i=1}^ni$ exists" in the first place!

---

EDIT: You added:

I am not asking if Robinson arithmetic can prove this statement. I want to know if it is "true" in this model with the simple lexicographical mapping of polynomials to natural numbers.

However, this was exactly the point of my answer! To tell whether a formula holds in a given structure, the formula needs to be in the language of that structure. And the structure you consider here (call it "$M$") does not have the symbol "$\sum$" in its language! So it's meaningless to ask whether a formula involving that symbol is true in $M$.

Now, we can get around this as soon as you tell us what "$\sum$" is an abbreviation for. For instance, let's use the possible interpretation I give above. Then it turns out that $M$ doesn't even think "$\sum_{i=1}^X i$" exists! That is, $M\models\forall y\neg\varphi(y, X)$, where $\varphi$ is the formula stating

"There is a number $z$ which codes a sequence of length $X$, such that the first term of that sequence is $1$, the last term is $y$, and for each $k<X$, the $(k+1)$th term is the $k$th term plus $k+1$."

So the question you are trying to ask is not well-formed, until you tell us what "$\sum$" means in the language of Robinson arithmetic; and even when you do that, the structure $M$ is weak enough that basic facts about $\sum$ (like, existence) will break down.