Diophantine vs. existential definability
Solution 1:
Your definitions are correct (though your definition of existentially definable has an extraneous "$=0$" at the end of the formula, which I assume is a typo). I think this answers your questions 1 and 2.
In fact, over $\mathbb{Q}$, the two definitions are equivalent. I think this answers your questions 3 through 6.
Claim: A set $S\subseteq \mathbb{Q}$ is diophantine in $\mathbb{Q}$ if and only if it is existentially definable in $\mathbb{Q}$.
Proof: In any ring, a diophantine set is existentially definable. Conversely, let's prove that for every quantifier-free formula $\varphi(T,Z_1,\dots,Z_n)$, there is a polynomial $f_\varphi(T,Z_1,\dots,Z_n,W_1,\dots,W_m)$ with integer coefficients such that $$R\models \varphi(t,z_1,\dots,z_n)\text{ if and only if }R\models \exists w_1\dots w_m (f_\varphi(t,z_1,\dots,z_n,w_1,\dots,w_m) = 0).$$ It follows that $$R\models \exists z_1\dots z_n\,\varphi(t,z_1,\dots,z_n)\text{ if and only if }R\models \exists z_1\dots z_n w_1\dots w_m (f_\varphi(t,z_1,\dots,z_n,w_1,\dots,w_m) = 0).$$
In the statement we're trying to prove, there is no special distinction between the variable $T$ and the variables $Z_i$: $\varphi$ is just a formula in $(n+1)$ free variables, which also appear in the polynomial $f_\varphi$. So let's agree to supress mention of these variables, to ease notation.
We may assume $\varphi$ is written in conjunctive normal form, as a conjunction of disjunctions of atomic and negated atomic formulas. So we will prove the claim in steps, for (1) atomic formulas, (2) negated atomic formulas, (3) disjunctions of atomic and negated atomic formulas, and (4) conjunctions of disjunctions of atomic and negated formulas.
- If $\varphi$ is an atomic formula, it is an equality between terms $p_1 = p_2$. Then $\varphi$ is equivalent to $p_1 - p_2 = 0$. We conclude by observing that every term in the language of rings is equivalent to a polynomial with integer coefficients (in the same variables).
- If $\varphi$ is a negated atomic formula, say $\lnot \psi$, then by step 1, $\varphi$ is equivalent to $f_\psi \neq 0$. Since $\mathbb{Q}$ is a field, this is equivalent to the existence of $w$ such that $wf_\psi = 1$. So $\varphi$ is equivalent to $\exists w\,(wf_\psi - 1 = 0)$. This method of turning an inequation into an equation at the expense of adding an extra variable is sometimes called the Rabinowitsch trick.
- Suppose $\varphi$ is a disjunction $\bigvee_{i=1}^k \psi_i$, where each $\psi_i$ is atomic or negated atomic. By steps 1 and 2, each $\psi_i$ is equivalent to $\exists w\,f_{\psi_i} = 0$ (where $f_{\psi_i}$ does not contain the variable $w$ if $\psi_i$ is atomic). Now the existential quantifier distributes over disjunctions, so we can pull the $\exists w$ to the front. And since $\mathbb{Q}$ is an integral domain, some $f_{\psi_i}$ is $0$ if and only if $\prod_{i=1}^k f_{\psi_i}$ is $0$. So $\varphi$ is equivalent to $\exists w (\prod_{i=1}^k f_{\psi_i} = 0).$
- Suppose $\varphi$ is a conjunction $\bigwedge_{i=1}^k \psi_i$, where each $\psi_i$ is equivalent to $\exists w_i( f_{\psi_i} = 0)$. Note that here we have used distinct variables $w_i$ for each conjunct, so that we can pull the existential quantifiers out of the conjunction: $\bigwedge_{i=1}^k \exists w_i (f_{\psi_i} = 0)$ is equivalent to $\exists w_1\dots w_k( \bigwedge_{i=1}^k f_{\psi_i} = 0)$. And since a sum of squares $a_1^2+\dots+a_k^2 = 0$ in $\mathbb{Q}$ is $0$ if and only if each $a_i=0$, all $f_{\psi_i}$ are $0$ if and only if $\sum_{i=1}^k (f_{\psi_i})^2$ is $0$. So $\varphi$ is equivalent to $\exists w_1\dots w_k \sum_{i=1}^k (f_{\psi_i})^2 = 0.$
This completes the proof.
Note that step 1 works in any ring, step 2 works in any field, step 3 works in any integral domain, and step 4 works in any formally real field. Thus the full result is true in any formally real field (e.g. any subfield of $\mathbb{R}$). In a general field, an existentially definable set is definable by a system of diophantine equations.
Finally, note that all of the above applies just as well to diophantine / existentially definable sets in $R^n$, not just $R$: in the definitions and the proof, just replace the variable $t$ with a tuple of $n$ variables.