Lemma 1.
For any $x$ in the ring $F[t,t^{-1}]$ ($F[t,t^{-1}]$: the polynomials in $t$ and $t^{-1}$ with coefficients in the field $F$), $x$ is a power of $t$ if and only if $x$ divides $1$ and $t-1$ divides $x-1$ (the divisibilities are meant, of course, in $F[t, t^{-1}]$).
Lemma 2.
Assume that the characteristic of $F$ is zero. Then for any $n$ in the ring $F[t, t^{-1}]$ ($F[t,t^{-1}]$: the polynomials in $t$ and $t^{-1}$ with coefficients in the field $F$), $n$ is a nonzero integer if and only if $n$ divides $1$ and either $n-1$ divides $1$ or $n+1$ divides $1$, and there is a power $x$ of $t$, so that $(x-1)/(t-1) \equiv n \pmod {t-1}$.
THEOREM.
Assume that the characteristic of $F$ is zero. Then the existential theory of $F[t, t^{-1}]$ in the language $\{+, \cdot , 0, 1, t\}$ is undecidable.
PROOF.
By Lemma 1, we can express the fact that an element $x$ in $F[t, t^{-1}]$ is a power of $t$ by an existential formula $\phi(x)$.
By this and Lemma 2, we can express the fact that an element $n$ of $F[t, t^{-1}]$ is an integer by the existential formula $$(\exists x)(\exists y) [\phi (x) \wedge x-1 = (t-1)n+y(t-1)^2] \wedge (\exists z)(\exists w) (nz =1 \wedge ((n+1)w=1 \text{ or } (n-1)w=1)$$ Call the last formula $\psi(n)$.
Assume for the sake of contradiction, that the existential theory of $F[t, t^{-1}]$ is decidable.
Then we can algorithmically examine the solvability of a diophantine equation in the rational integers in the following way:
if $P(X_1, \dots , X_n)=0$ is a given diophantine equation, we consider the existential formula $$(\exists x_1) \dots (\exists x_n) P(x_1, \dots , x_n)=0 \wedge \psi(x_1) \wedge \dots \psi(x_n)$$
Clearly, the equation of whether this sentence is true in $F[t, t^{-1}]$ is equivalent to the question of whether $P=0$ has integral solutions. But this contradicts the negative answer to Hilbert's Tenth Problem; therefore, the theorem follows.
$$$$
Could you explain to me the formula $\psi(n)$ ?
Could you explain to me the reduction to Hilbert's Tenth Probelm? I haven't really understood it...
$$$$
$$$$
EDIT:
Can we change the theorem and its proof as follows?
THEOREM.
We suppose that the characteristic of $F$ is zero. Then the positive existential theory of $F[t, t^{-1}]$ in the language $\{+, \cdot , 0, 1, t\}$ is undecidable.
Proof. We want to show that there is no algorithm, that given a positive existential sentence $\gamma$, it answers if $\gamma$ is true in the ring $F[t, t^{-1}$ or not. According to Matijasevic, there is no algorithm that with input a polynomial $P(x_1, \dots , x_n)$ with integer coefficients, always decides if the equation $P(X-1, \dots , x_n)=0$ has an integer solution. According to Lemma $1$, an element $x \in F[t, t^{-1}]$ is a power of $t$ iff $$x \mid 1 \ \ \land \ \ t-1 \mid x-1$$ So we can express the fact that an element $x \in F[t, t^{-1}]$ is a power of $t$ with the positive existential formula $$\phi (x) \ \ : \ \ \exists y \exists z ((xy=1) \land (x-1=(t-1)z))$$ According to Lemma $3$, $n$ is a nonzero integer iff
- $n \mid 1 \ \ : \ \ (\exists z)(nz=1)$
- $n-1 \mid 1 \lor n+1 \mid 1 \ \ : \ \ (\exists w)((n+1)w=1 \text{ or } (n-1)w=1)$
- there is a power $x$ of $t$ $\ \ : \ \ (\exists x) \phi (x)$
- $(x-1)/(t-1) \equiv n \pmod {t-1} \ \ : \ \ (\exists y)((x-1)/(t-1)-n =y(t-1)) \Rightarrow (\exists y)(x-1-n(t-1)=y(t-1)^2) \Rightarrow (\exists y)(x-1=n(t-1)+y(t-1)^2)$
So we can express the fact that an element $n \in F[t, t^{-1}]$ is an integer with the positive existential formula $$\psi (n) \ \ : \ \ (\exists x)(\exists y)[\phi(x) \land x-1=(t-1)n+y(t-1)^2] \land (\exists z)(\exists w)(nz=1 \land ((n+1)w=1 \text{ or } (n-1)w=1)$$ We suppose that the positive existential formula of $F[t, t^{-1}]$ is decidable, so there is an algorithm that decides if a positive existential sentence is true in $F[t, t^{-1}]$. Then the problem if a diophantine equation has an integer solution is decidable: the diphantine equation $P(x_1, \dots , x_n)=0$ has an integer solution iff the positive existential sentence $$(\exists x_1) \dots (\exists x_n) ((\psi (x_1) \land \dots \land \psi (x_n)) \land P(x_1, \dots , x_n)=0)$$ is true in $F[t, t^{-1}]$. But the answer to the $10^{th}$ Hilbert's Problem, i.e., if there is an algorithm that decides if the diophantine equation has an integer solution, is negative. So we have a contradiction. That means that the positive existential theory of $F[t, t^{-1}]$ is undecidable.
We explain the reduction, and later, if questions arise, explain $\psi$.
A formula $\alpha(x_1,x_2,\dots, x_k)$ is existential if it has the shape $$\exists t_1\exists t_2\cdots \exists t_l\beta(x_1,\dots,x_k, t_1,\dots,t_l),\tag{1}$$ where the formula $\beta(x_1,\dots,x_k, t_1,\dots,t_l)$ is quantifier-free. Sometimes, informally, as in the definition you quote for $\psi(n)$, the term existential formula is used for formulas that can be mechanically put in the form (1). (Note that as given, the existential quantifiers are not all in front.)
Let $F$ be a field of characteristic $0$. We want to show that there is no algorithm which, given any existential sentence $\gamma$, will tell us whether or not $\gamma$ is true in the ring $F[t,t^{-1}]$.
By the result that culminated in the work of Matijasevic, there is no algorithm which, when given as input a polynomial $P(X_1,\cdots,X_n)$ with integer coefficients, will always determine whether or not the equation $P(X_1,\dots,X_n)=0$ has a solution in integers.
We show that if there were an algorithm for determining the truth in $F[t,t^{-1}]$ of existential sentences, then there would be an algorithm for determining the solvability of Diophantine equations in the integers. But there is no such algorithm.
The reduction strategy is in principle simple. Given any Diophantine equation $P(X_1,\dots,X_n)=0$, we show how to construct explicitly an existential sentence $\alpha_P$ such that $\alpha_P$ is true in $F[t,t^{-1}]$ if and only if $P(X_1,\cdots,X_n)=0$ has a solution in integers. Now suppose we had an algorithm to determine the truth of existential sentences in $F[t,t^{-1}]$. Then by applying the algorithm to $\gamma_P$, we could determine whether or not the Diophantine equation $P(X_1,\dots,X_n)=0$ has a solution, contradicting the (negative) solution of Hilbert's $10$-th Problem.
By Lemmas 1 and 2, there is an existential formula $\psi(w)$ such that $w\in F[t,t^{-1}]$ satisfies the formula $\psi$ if and only if $w$ is an ordinary integer. Thus $P(X_1,\dots,X_n)=0$ has an integer solution if and only if the sentence $$\exists x_1\cdots,\exists x_n((\psi(x_1)\land\dots\land \psi(x_n))\land P(x_1,\dots,x_n)=0)\tag{2}$$ is true in $F[t,t^{1}]$. In the sentence (2), the existential quantification ranges over $F[t,t^{-1}]$. The subformulas $\psi(x_i)$ informally say "$x_i$ is an ordinary integer."
Note that the subformulas $\psi(x_i)$ are existential, involving $4$ existential quantifiers each. We need to use $4n$ distinct existentially quantified variables for the $\psi(x_i)$, and we need to bring them to the front in (2) so that the resulting sentence will be genuinely existential.
That's all there is to the reduction. Suppose further that $-1$ is never a sum of squares in the field $F$. This is true in particular if $F$ is a subfield of the reals. Then by a trick you are by now familiar with, we say a little more. Given any polynomial $P(X_1,\dots,X_n)$ with integer coefficients, we can construct a polynomial $P^\ast(x_1,\dots, x_n,y_1,\dots,y_m)$ with integer coefficients such that the Diophantine equation $P(X_1,\dots,X_n)=0$ has a solution in the integers if and only if the equation $P^\ast(x_1,\dots, x_n,y_1,\dots,y_m)=0$ has a solution in $F[t,t^{-1}]$.