Writing sequences in the language of arithmetic

177 Views Asked by At

I am trying to write a theorem of arithmetic purely in the language of arithmetic. As a simple example, consider the theorem $$\forall m \quad 2(1+\cdots+m) = m(m+1)$$ This is a well known theorem of arithmetic, but the above statement is imprecise. It requires you to interpret the '$\cdots$'. How can this statement be formalized?

I emphasize that I would like to state this purely in the language of arithmetic, ie. using only the symbols $0,=,+,\cdot,<$ and regular first order logic symbols.

1

There are 1 best solutions below

3
On

The standard way to formalize a "$\cdots$" in the first-order language of arithmetic involves using a recursive definition to give meaning to the ellipsis, and then expressing the recursively defined function using Gödel's $\beta$ trick. That is, however, fairly tedious if you want to write it out completely.

In your particular case, you can reasonably hope to get away with claiming directly that the function $f(m)=m(m+1)$ satisfies the recursion equations $$ \begin{align} f(1) &= 2 \\ f(m+1) &= f(m)+2(m+1) \end{align} $$