$F[t]$ has undecidable positive existential theory in the language $\{+, \cdot , 0, 1, t\}$ Consider the ring $F[t, t^{-1}]$ (the polynomials in $t$ and $t^{-1}$ with coefficients in the field $F$). 
Theorem 1. 

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 unecidable. 

Theorem 2. 

Assume that $F$ has characteristic $p>2$. Then the existential theory of $F[t, t^{-1}]$ is undecidable. 

We have that even the positive existential theory of $F[t, t^{-1}]$ is undecidable. 
Now we give a Lemma that, together with the preceding results, allows us to conclude the undecidability of the positive existential theory of $F[t]$ in the language $\{+, \cdot , 0, 1, t\}$. 
Lemma. 

If the characteristic of $F$ is other than $2$, then the solutions of $$X^2-(t^2-1)Y^2=1$$ with $X$ and $Y$ in $F[t]$ are given by $$(X, Y)=(\pm x_n, y_n)$$ where $$x_n+\sqrt{t^2-1}y_n=(t+\sqrt{t^2-1})^n$$ fr $n$ in $\mathbb{Z}$. 

Theorem 3. 

If the characteristic of $F$ is other than $2$, then $F[t]$ has undecidable positive existential theory in the language $\{+, \cdot , 0, 1, t\}$. 

Proof. 
Write $u=t+\sqrt{t^2-1}$. 
Then $u^{-1}=t-\sqrt{t^2-1}$ and $F[u, u^{-1}]=F[t, \sqrt{t^2-1}]$. 
We interpret the positive existential theory of $F[u, u^{-1}]$ in $F[t]$ in the following way: 
an element $x$ of $F[u, u^{-1}]$ is represented as a pair $x=(a, b)$ with $a, b$ in $F[t]$ being the components of $x$ with repsect to the base $\{u, u^{-1}\}$ considering $F[u, u^{-1}]$ as a module over $F[t]$; addition and multiplication of elements of $F[u, u^{-1}]$ is defined accordingly. 
So, we see that the positive existential theory of $F[u, u^{-1}]$ is interpretable in $F[t]$ with only one problem: we do not have constants for $u$ and $u^{-1}$ but only for $\frac{u+u^{-1}}{2}=t$. 
So, the positive existential theory of $F[t]$ is undecidable provided that the theory of $F[u, u^{-1}]$ is undecidable in the language $\{0, 1, u+u^{-1}/2, +, \cdot\}$. 
It is only a matter of routine checking to see that our undecidability result for $F[u, u^{-1}]$ holds true in this language as well: simply substitute $v=u-t$, write all equations involved in the form $fv=g$, where $f$ and $g$ have coefficients in $F[t]$ (the quantity $v^2$, wherever it appears, is replaced by $t^2-1$ which is in $F[t]$) and substitute the equations of this last form by the corresponding equations $f^2(t^2-1)=g^2$. 
Of course, it is necessary to check that the new solutions that come onto the scene through the squaring do not do any harm to the stated equivalences. 
Hence, the theorem follows. 

$$$$ 
How do we use the Lemma at the proof of Theorem $3$ ? How is it useful? 
$$$$ 
EDIT: 
That's how I understood the whole proof of Theorem $3$ :   
We know that the existential theory of $F[u, u^{-1}]$ in the language $\{+, \cdot , 0, 1, u\}$ is undecidable. 
We want to reduce the positive existential theory of $F[u, u^{-1}]$ in the language $\{+, \cdot , 0, 1, u\}$ to the positive existential theory of $F[t]$ in the language $\{+, \cdot , 0, 1, t\}$ to show that this theory is also undecidable.
To do that we do the following: 
We suppose that the positive existential theory of $F[t]$ in the language $\{+, \cdot , 0, 1, t\}$ is decidable. 
We set $u=t+\sqrt{t^2-1}$. So, we have that $u^{-1}=t-\sqrt{t^2-1}$.  
So, we have $F[u, u^{-1}]=F[t, \sqrt{t^2-1}]$. So, $F[u, u^{-1}]$ is an extension of $F[t]$.  
Each element $x$ of $F[u, u^{-1}]$ can be written as followed: $x=a+b\sqrt{t^2-1}$, where $a,b \in F[t]$. 
So, the mapping of the reduction is $x \mapsto (a,b)$.  
$+ \ \ : \ \  $ $$x_1+x_2=a_1+b_1\sqrt{t^2-1}+a_2+b_2\sqrt{t^2-1}=(a_1+a_2)+(b_1+b_2)\sqrt{t^2-1} \mapsto (a_1+a_2, b_1+b_2)$$
$\cdot  \ \ : \ \  $ $$x_1\cdot x_2=(a_1+b_1\sqrt{t^2-1})(a_2+b_2\sqrt{t^2-1})=a_1 \cdot a_2+a_1 \cdot b_2 \sqrt{t^2-1}+a_2 \cdot b_1\sqrt{t^2-1}+b_1 \cdot b_2 (t^2-1)=(a_1 \cdot a_2+b_1 \cdot b_2 (t^2-1))+(a_1 \cdot b_2+a_2 \cdot b_1)\sqrt{t^2-1} \mapsto (a_1 \cdot a_2+b_1 \cdot b_2 (t^2-1), a_1 \cdot b_2+a_2 \cdot b_1)$$ 
$0  \ \ : \ \  $ $$0=0+0 \sqrt{t^2-1} \mapsto (0,0)$$ 
$1 \ \  :  \ \ $ $$1=1+0 \sqrt{t^2-1} \mapsto (1,0)$$
$u \ \ : \ \  $ $u \mapsto u-t=:v$. We write all the equations in the form $fv=g$ where $f,g \in F[t]$ and squaring these equations we get $f^2v^2=g^2 \Rightarrow f^2(t^2-1)=g^2$, so all these equations are in $F[t]$, where $t=(u+u^{-1})/2$.  
So we can convert the algorithm that answers to positive existential questions of $F[t]$ to an algorithm that answers to existential questions of $F[u, u^{-1}]$. 
Since the second theory is undecidable, we get aa contradiction. So the positive existential theory of $F[t]$ is undecidable. 
$$$$ 
Is this correct?  
 A: You are, I believe, asking about a proof in the paper Extensions of Hilbert's Tenth Problem by Thanases Phaedas. You've asked three questions about this. The background is that Phaedas has proved that the existential theory of $F[u, u^{-1}]$ is undecidable (he actually wrote $t$ rather than $u$ when he proved, but he has now switched to $u$). He is trying to get stronger result by reducing decidability in the polynomial ring $F[t]$ to decidability in the ring of Laurent polynomials $F[u, u^{-1}]$. The approach is to extend $F[t]$ to $F[t, s\mathrel{|} s^2 = t^2 - 1]$ (but Phaedas doesn't quite put it like that). Then one observes that $F[t, s]$ is isomorphic to $F[u, u^{-1}]$ under an isomorphism that associates $t$ with $(u + u^{-1})/2$ and $s$ with $(u - u^{-1})/2$.
Your first question is:


an element $x$ of $F[u, u^{-1}]$ is represented as a pair $x=(a, b)$ with $a, b$ in $F[t]$ being the components of $x$ with repsect to the base $\{u, u^{-1}\}$ considering $F[u, u^{-1}]$ as a module over $F[t]$

Does this mean that we write any element $x$ of $F[u, u^{-1}]$ in the form $x=au+bu^{-1}$ ?

It means that every $x \in F[u, u^{-1}]$ can be written uniquely as $x = au+bu^{-1}$ for $a, b \in F[t]$. However, I believe this is false. $F[t, s]$ is a free module of rank $2$ over $F[t]$, a suitable base being $\{1, s\}$ (which Pheidas would write as $\{1, \sqrt{t^2 - 1}\}$). What this means is that every element $x \in F[u, u^{-1}]$ can be written uniquely in the form $a + bs$ with $a, b \in $F[t]$.  I believe this is just a (very significant) typo.
Your second question is:

We have that each element of $F[u, u^{-1}]$ can be represented as an element of $F[t]$, besides $u$ and $u^{-1}$, becasuse the language does not consist of a square root. Is this correct?

What we have is that each element of $F[u, u^{-1}]$ can be represented uniquely as a pair of elements $a, b$ of $F[t]$ with $(a, b)$ representing $a + bs$ (following my correction to Pheidas's statement about the basis above).
Your final question is:


$\ldots$ simply substitute $v=u-t$, write all equations involved in the form $fv=g$, where $f$ and $g$ have coefficients in $F[t]$ (the quantity $v^2$, wherever it appears, is replaced by $t^2-1$ which is in $F[t]$) $\ldots$

Why can we write all the equations in the form $fv=g$, where $f$ and $g$ have coefficients in $F[t]$ ?

$F[u, u^{-1}]$ is generated over $F$ as a ring by $t$ and $v$, hence any equation in $F[u, u^{-1}]$ can be written as $p(t, v) = 0$ where $p$ is a polynomial with coefficients in $F$, but $v^2 = t^2-1$, so we can arrange for $p$ to have the form $vf(t) - g(t)$ for $f, g \in F[t]$. and then $p(r, t) = 0$ is equivalent to $fv = g$.
