I recently read the model-theoretic proof of the Nullstellensatz using quantifier elimination (see www.msri.org/publications/books/Book39/files/marker.pdf). I'm convinced that the Nullstellensatz is true, i.e. by showing that $\exists y_1 \cdots \exists y_n (\bigwedge_{i} (f_i(y) = 0)$ is equivalent to a quantifier free formula, hence if it is true in an algebraically closed extension, it is true in the original algebraically closed field. What However, I don't have any intuition for how this formal sequence of steps leads to the truth of the Nullstellensatz. In particular, what I don't see is what the quantifier-free formulas are that these are equivalent to. For example, what is a quantifier-free formula in $a,b,c,d,e,f,g,h,i,j,k,l$ which is equivalent to the system $ax^2+bxy+cy^2+dx+ey+f=gx^2+hxy+iy^2+jx+ky+l=0$ having a non-trivial solution? And generalizations?
Can one simplify the model-theoretic proof by showing more directly that the existence of solutions to systems of equations (or non-equations) in algebraically closed fields are equivalent to polynomial conditions on the coefficients? I.e. apply essentially the same argument but restrict to the case of algebraically closed fields and avoid general results like Godel's Completeness Theorem to make the argument more clear. My expectation is that this might involve proving an algorithm for determining the quantifier-free formula from the formula with quantifiers.
