This seems like one these situations where one has to strengthen the claim in order to get through the induction. It may be much too complicated what I am doing here, but as a wise man once said, if it works it ain't stupid.
Let $\Sigma$ be the following set of $\{\in, \dot A\}$-formulas:
- all atomic formulas are in $\Sigma$
- $\Sigma$ is closed under $\wedge$ and $\neg$
- if $\varphi(x)$ is a $\in$-formula, then $\exists x\ \varphi(x)$ is in $\Sigma$
- if $\varphi(x, y)$ is in $\Sigma$ then $\{x\in \bigcup\dot A\mid \varphi(x, y)\}\in \dot A$ is in $\Sigma$
Essentially we allow $\dot A$ as long as we do not quantify over it.
I claim that the lemma holds true for all $\Sigma$-formulas.
For all $x$, $\gamma_1<\dots<\gamma_n<\alpha$ and $\varphi\in\Sigma$ we have:
$$(M_\alpha, \in, U_\alpha)\models\varphi(i_{0, \alpha}(x), \kappa_{\gamma_1},\dots, \kappa_{\gamma_n})$$
iff
$$(M, \in, U)\models\{\{\xi_1, \dots, \xi_n\}\in[\kappa]^{n}\mid \varphi(x, \xi_1,\dots, \xi_n)\}\in U^n$$
Annoyingly, we have to backtrack quite a bit to do it. First let me show that $(M, \in, U)$ satisfies a form of replacement with respect to $\Sigma$-formulas, that is for any $\Sigma$-formula $\varphi$ and parameter $p\in M$, the function $F:\kappa\rightarrow \mathcal{P}(\kappa)$ given by
$$F(\alpha)=\{\beta<\kappa\mid\varphi(\alpha,\beta, p)^M\}$$
is in $M$. We prove this by induction on the complexity of $\varphi$. The only nontrivial case arises when
$$\varphi(x, y, z)= \{u\in\bigcup \dot A\mid \psi(u, x, y, z)\}\in\dot A$$
Let $h:\kappa\rightarrow\kappa\times\kappa$ be a bijection in $M$. By induction, the function $G:\kappa\rightarrow\mathcal{P}(\kappa)$ given by
$$G(\delta)=\{\gamma<\kappa\mid\psi(\gamma, h(\delta)_0, h(\delta)_1, p)^M\}$$
is in $M$. By weak amenability, we have
$$X=\{\delta<\kappa\mid G(\delta)\in U\}\in M$$
But now
$$F(\alpha)=\{\beta<\kappa\mid h^{-1}(\alpha,\beta)\in X\}$$
and thus $F\in M$.
It follows immediately (from weak amenability) that $M$ satisfies the corresponding form of separation with respect to $\Sigma$-formulas that is:
For any $\Sigma$-formula $\varphi$ and parameter $p\in M$ we have
$$\{\alpha<\kappa\mid\varphi(\alpha, p)\}^M\in M$$
We now prove Los's theorem for the $\Sigma$-formulas in our context. Again, almost everyhing is trivial or works as in the usual proof. Note that the $\exists$-case goes through as in that case $\dot A$ is not allowed to appear in the formula. For the new part, suppose $\varphi=\{x\in\bigcup\dot A\mid \psi(x, y)\}\in \dot A$. We look at when
$$(M_1,\in, U_1)\models \{\beta< \kappa_1\mid\psi(\beta, [f])\}\in U_1$$
holds.
Note that $\{\beta< \kappa_1\mid\psi(\beta, [f])\}^{M_1}$ is really a set in $M_1$ and furthermore if we define $g:\kappa\rightarrow M$ by
$$g(\alpha)=\{\beta<\kappa\mid\psi(\beta, f(\alpha))\}^M$$
then $g\in M$ and
$$[g]=\{\beta< \kappa_1\mid\psi(\beta, [f])\}^{M_1}$$
Thus by definition of $U_1$,
$$(M_1,\in, U_1)\models [g]\in U_1\Leftrightarrow (M, \in, U)\models\{\alpha<\kappa\mid g(\alpha)\in U\}\in U$$ and thus
$$(M_1, \in, U_1)\models\varphi([f])\Leftrightarrow (M,\in, U)\models\{\alpha<\kappa\mid\varphi(f(\alpha))\}\in U$$
which is what we had to show.
Finally, we can tackle the lemma in our strenghtened form. Let us go through it to see that now, everything works out fine. Again the case $n=0$ is immediate, as our Los theorem for $\Sigma$ implies that the embeddings $i_{\alpha, \beta}$ are elementerary w.r.t. $\Sigma$-formulas. In the inductive step from $n-1$ to $n$:
$$(M_\alpha, \in, U_\alpha) \models \varphi(i_{0\alpha}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n})$$
$$\text{ iff } (M_{\gamma_n+1}, \in, U_{\gamma_{n+1}})\models \varphi(i_{0,\gamma_n+1}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n})$$
$$\text{ iff }(\ast)_0 (M_{\gamma_n}, \in, U_{\gamma_n}) \models \{\xi \lt \cup U_{\gamma_n} \mid \varphi(i_{0\gamma_n}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_{n−1}}, \xi )\} \in U_{\gamma_n}
$$
$$\text{ iff }(\ast)_1 (M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_{n−1}\} \in [κ]^{n−1} \mid \{\xi \lt \cup U \mid \varphi(x, \xi_1,\dots,\xi_{n−1}, \xi )\} \in U\} \in U^{n−1}
$$
$$\text{ iff } (M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_n\} \in [κ]^n \mid \varphi(x, \xi_1,\dots,\xi_n)\} \in U^n.
$$
The step $(\ast)_1$ is now perfectly justified by our inductive hypothesis. In the step $(\ast)_0$, we used Los's theorem for the $\Sigma$-formulas. This finishes the proof.
Let me try to give some input. So first of all, this definition appears in a proof, so it should be understood in the context of the proof. The $E$ is fixed in the statement of the lemma and thus it is not quantified over in the definition, so what simple means in the proof maybe should be called $E$-simple and being $E$-simple can be different from being $F$-simple for $E\neq F$.
Regarding your second question, in the definition it is not required that the equivalent $\Sigma_0$-formula is uniform in the structures. To finish the proof, one only needs that all $\operatorname{rud}_E$-functions are simple in this sense (as this is quite tedious to do, this statement was packaged as an exercise). The uniformity is not relevant. Anyhow, doing this exercise reveals that for $\operatorname{rud}_E$-functions these formulas can be chosen uniformly. Indeed even more is true: In the same way as one can associate natural numbers to first order formulas by looking at how they are build from the atomic formulas and the connectives, one can do this with rudimentary functions. There is then a recursive map $\eta:\operatorname{Fml}_{\in, E}\times\omega\rightarrow\operatorname{Fml}_{\in, E}$ so that whenever $f$ is $\operatorname{rud}_E$ and $\varphi$ is a $\Sigma_0$ $\{\in, E\}$-formula then $\varphi(f(v_0, \dots, v_n), w_0, \dots , w_m)$ is equivalent to $\eta(\varphi, k)(v_0, \dots, v_n, w_0,\dots, w_m)$ over any transitive $\operatorname{rud}_E$-closed structure, where $k$ is the natural number associated to $f$. [Again, E is fixed here]
Lastly, the reason why one quantifies over not just all transitive but moreover $\operatorname{rud}_E$-closed strucures is simply that the question whether $\varphi(f(v_0, \dots, v_n), w_0, \dots , w_m)$ is equivalent to $\psi(v_0, \dots, v_n, w_0, \dots , w_m)$ over a structure $\mathcal M=(M, \in, E)$ only makes sense if $M$ is closed under $f$. It means
$$\text{for all }x_0,\dots, x_n, y_0,\dots y_m\in M\ \mathcal M\models \varphi(f(x_0, \dots, x_n), y_0, \dots , y_m)\Leftrightarrow\psi(x_0, \dots, x_n, y_0, \dots , y_m)$$
after all.
Best Answer
The accepted answer is incorrect. $\omega$-consistency does not say "If you prove $P(n)$ for each standard $n$, then you prove $\forall n(P(n))$." That would be $\omega$-completeness.
Rather, $\omega$-consistency says "If you prove $\exists x\neg P(x)$, then you must not prove $P(n)$ for each standard $n$." And in particular, both $AST$ and the theory $T$ introduced in that answer are $\omega$-consistent, at least assuming $ZFC$ is to begin with.
Getting back to the main question, it may help to drop $AST$ and consider the simpler fact about $ZFC$ alone, which is itself provable in ZFC:
The key point is that "$A\models ZFC$" is interpreted in reality; we may not have $M\models(A\models ZFC)$.
This also explains why the OP's reflection argument breaks down - it's exactly the same reason.
Here's how to prove $(*)$ in ZFC:
If $ZFC$ is inconsistent then $(*)$ is vacuously true.
Suppose $ZFC$ is consistent. Let $M\models ZFC$. If $M\models Con(ZFC)$ then since $ZFC$ proves the completeness theorem we're done.
So suppose $M\models \neg Con(ZFC)$. Let $n\in\omega^M$ be what $M$ thinks is the largest number such that there is no proof of a contradiction from the first $n$ axioms of $ZFC$. If we can conclude that $n$ is nonstandard, we'll be done: by completeness in $M$, any model $A$ of the first $n-1$ axioms of $ZFC$ in the sense of $M$ will in reality be a model of $ZFC$, even if $M$ doesn't think so.
Now here's the cute bit: we internalize the reflection principle. Looking at the usual argument we see in fact that ZFC proves "ZFC proves every finite subtheory of ZFC." (Note the crucial nested "proves" here.) This means we can next say...