The set $R$ of rational points on the curve $y^2=x^2+1$ can be viewed as a group under the following operation: if $X_1=(x_1,y_1),\ X_2=(x_2,y_2)\in R$, define $X_1*X_2:=(x_1y_2+x_2y_1,x_1x_2+y_1y_2)$. Does this group finitely generated, i.e. does the Mordell-Weil theorem holds for this case? I don't think so by the following reason.
By the usual parametrization, we can write $x_1=\frac{1}{2}(a-\frac{1}{a}), x_2=\frac{1}{2}(b-\frac{1}{b})$. This gives $x_1y_2+x_2y_1=\frac{1}{2}(ab-\frac{1}{ab})$. If $R$ is finitely generated, each point $X\in R$ should be written as $X=(x,y)=(\frac{1}{2}({a_1}^{n_1}\cdots{a_i}^{n_i}-\frac{1}{{a_1}^{n_1}\cdots{a_i}^{n_i}}))$ for some generators $X_1=(\frac{1}{2}(a_1-\frac{1}{a_1}),\frac{1}{2}(a_1+\frac{1}{a_1})),\cdots ,X_i=(\frac{1}{2}(a_i-\frac{1}{a_i}),\frac{1}{2}(a_i+\frac{1}{a_i}))$. However, not every rationals can be written in the form ${a_1}^{n_1}\cdots{a_i}^{n_i}$, a contradiction.
If the above is true, is there a group structure for $y^2=x^2+1$ that the Mordell-Weil theorem can be applied? If yes, could anyone give an explicit form?