Trouble understanding converse of Tarski's theorem I am working through a paper entitled "Elimination of quantifiers in algebraic structures," and am having a lot of trouble understanding the first theorem. The paper is available here and attempts to prove a partial converse of one of Tarski's theorems (here is the particular theorem they prove the converse of). 

Namely, they want to show that if $K$ is an infinite field, whose $\mathcal{L}$-theory admits quantifier elimination (QE), where $\mathcal{L}=\{=,0,1,+,-,\cdot\}$ (i.e. the language of rings with identity), then $K$ is algebraically closed.

They attempt to do this by contradiction. From here on out I will copy out bits of the proof and walkthrough what is clear, and what is not.

We argue by contradiction. Let $K$ have an algebraic extension $K(\alpha)$ of degree $n>1$.

I get the degree has to be $n>1$ otherwise, $\alpha\in K$ such that $K(\alpha)=K$, contrary to assumption. 

Let $f(y,\bar{x})=y^n+x_{n-1}y^{n-1}+...+x_0$. Then there is a quantifier free formula $\phi(\bar{x})$ which we may take as a disjunction of Type A (this is explained in Lemma 1 in the paper), which is equivalent in $K$ to $\forall y\,(f(y,\bar{x})\neq0)$.

As I understand this, I think they are saying that $f$ is the minimal polynomial for $\alpha$. So clearly, $y\in K$ cannot be a root of it. Otherwise, it would not be minimal. Clearly since $K\vDash\forall y\,(f(y,\bar{x}))$ Now, the paper goes on to assume that $\alpha$ is seperable over $K$. I'm not entirely sure why? Does the proof become obvious if $\alpha$ is not seperable? After this part, I get very confused about what the authors are trying to do. Any help clarifying how I should read this proof would be appreciated.
I'm especially having a lot of trouble seeing the relationships between $f(y,\bar{x})$ and the big $F$ polynomial. I think the crucial part of the proof I don't understand is these couple of sentences somewhere in the middle:

Now $\{F_j(\bar{z})\}$ is algebraically independent over $K$ and $K$ is infinite. Thus, there is no $K$-Zariski closed proper subset $X$ of $K^n$ such that $X\supset\{\langle F_0(\bar{K},...,F_{n-1}(\bar{k}))\rangle|\text{$\bar{k}\in K^n$, $k_i\neq 0$ for some $i>1$}\}$.

 A: I'll try to give some motivation for the main idea of the proof. 
Start by reading the last paragraph first (I think it would have been clearer to begin the proof this way). Here it is proven that if $K$ has QE, then $K$ is perfect. It follows that every algebraic extension of $K$ is separable. 
So we assume for contradiction that $K$ is not algebraically closed, i.e. $K$ has a proper (degree $n>1$) algebraic extension $K(\alpha)$, which we know must be separable by the last paragraph. We define $$f(y,\overline{x}) = y^n + x_{n-1}y^{n-1} + \dots + x_0.$$ You wrote "As I understand this, I think they are saying that $f$ is the minimal polynomial for $\alpha$". This is not correct. $f$ is a polynomial in $(n+1)$ variables, $y,x_0,\dots,x_{n-1}$. It's the "template" for all degree $n$ monic polynomials: every such polynomial is of the form $f(y,\overline{a})$ for some coefficients $\overline{a}$. What's true is that for some choice of $\overline{a}$, $f(y,\overline{a})$ will be the minimal polynomial of $\alpha$. For this $\overline{a}$, $f(y,\overline{a})$ has no root in $K$, but for many other tuples $\overline{b}$, $f(y,\overline{b})$ does have a root in $K$. 

Very broadly speaking, the strategy of the proof is exploit this difference between coefficients, by showing for a contradiction that "most" tuples of coefficients give a polynomial with a root, and also "most" tuples of coefficients give a polynomial without a root. Here the meaning of "most" has to do with genericity in algebraic geometry: whether an algebraically independent tuple in a field extension satisfies the condition. And to make sense of this, it's important that the condition is quantifier-free. 

Back to the proof itself: we use QE to find a quantifier-free formula $\Phi(\overline{x})$ which is equivalent to $\forall y\, f(y,\overline{x})\neq 0$ in $K$. This $\Phi(\overline{x})$ as a quantifier-free "test" on the coefficients of a degree $n$ polynomial that tells you whether it has no root in $K$. So for example, if $f(y,\overline{a})$ is the minimal polynomial of $\alpha$, then $K\models \Phi(\overline{a})$. 
Now we want to establish the following claim:

$\Phi(\overline{x})$ is "too big" in the sense that the set it defines contains a non-empty Zariski open subset of $K^n$ (syntactically, this means that one of its disjuncts has the form $q(\overline{x})\neq 0$, where $q$ is a nonzero polynomial). 

We get a contradiction from the claim as follows: Consider the transcendental extension $K(z_1,\dots,z_n)$. It's a fact that $(\sigma_1(\overline{z}), \dots, \sigma_n (\overline{z}))$ are algebraically independent over $K$, where the $\sigma_i$ are the elementary symmetric polynomials in the $z_j$. An algebraically independent tuple doesn't satisfy any nonzero polynomial, so $q(\sigma_1(\overline{z}), \dots, \sigma_n (\overline{z}))\neq 0$. But thinking of $q(\sigma_1(\overline{z}), \dots, \sigma_n (\overline{z}))$ as a polynomial $q'(\overline{z})$, we see that $q'$ is non-zero, so (since $K$ is infinite) there is some tuple $\overline{k}\in K^n$ such that $q'(\overline{k})\neq 0$, and hence $K\models \Phi(\sigma_1(\overline{k}),\dots,\sigma_n(\overline{k}))$, so $f(y,\sigma_1(\overline{k}),\dots,\sigma_n(\overline{k}))$ has no root in $K$. But this is the polynomial $\prod_{i=1}^n (y-k_i)$, which has all its roots in $K$, contradiction.
It remains to establish the claim, which is done in the second paragraph and the first half of the third paragraph of the proof. The algebra here is more involved, so I won't go into the details, but the idea is to come up with some elements $F_0(\overline{z}),\dots,F_{n-1}(\overline{z})$ in the transcendental extension $K(z_1,\dots,z_n)$ which are algebraically independent and such that $K\models \Phi(F_0(\overline{k}),\dots,F_{n-1}(\overline{k}))$ for almost all $\overline{k}\in K^n$. The $F_i$ are chosen so that the roots of $f(y,F_0(\overline{k}),\dots,F_{n-1}(\overline{k}))$ are the elements $k_0 + k_1\alpha_j + \dots + k_{n-1}\alpha_j^{n-1}$, where $\alpha_j$ is one of the conjugates of $\alpha$ in the algebraic closure of $K(\alpha)$, and these elements are almost never in $K$. The main work is proving the algebraic independence of the $F_i(\overline{z})$, and it's important here that $K(\alpha)$ was a separable extension so that $\alpha$ actually has $n$ distinct conjugates over $K$. It follows that the subset of $K^n$ defined by $\Phi(\overline{x})$ can't be contained in any proper Zariski-closed subset of $K^n$ (i.e. isn't contained in the zero set of any non-zero polynomial), and by irreducibility of $K^n$, or by the syntactic presentation of $\Phi(\overline{x})$, this establishes the claim. 

Above I've more or less followed the argument in the paper. But I would conceptualize the proof as follows (along the lines of the intuition in the first quote block. 
First, show that for all $\overline{k}$ in $K^n$, $f(y,\sigma_1(\overline{k}),\dots,\sigma_n(\overline{k}))$ has a root in $K$. So $K\models \lnot \Phi(\sigma_1(\overline{k}),\dots,\sigma_n(\overline{k}))$. It follows that for generic $\overline{z}$ over $K$, we have $\lnot \Phi(\sigma_1(\overline{z}),\dots, \sigma_n(\overline{z}))$. But if the $\overline{z}$ are algebraically independent over $K$, so are the $(\sigma_1(\overline{z}),\dots, \sigma_n(\overline{z}))$. So $\lnot \Phi$ holds generically. 
Next, find the $F_j$ and show that for almost all $\overline{k}$ in $K^n$, $f(y,F_0(\overline{k}),\dots,F_{n-1}(\overline{k}))$ has no root in $K$. So $K\models \Phi(F_0(\overline{k}),\dots,F_{n-1}(\overline{k}))$. It follows that for generic $\overline{z}$ over $K$, we have $\Phi(F_0(\overline{z}),\dots, F_{n-1}(\overline{z}))$. Prove that if the $\overline{z}$ are algebraically independent over $K$, then so are the $(F_0(\overline{z}),\dots, F_{n-1}(\overline{z}))$ (this is the hardest part). So $\Phi$ holds generically. 
Finally, a quantifier-free condition and it's complement cannot both hold generically. 
