In their paper Kritchman and Raz present a proof of Gödel's second theorem using Kolmogorov complexity. To make it work, they operate in some (weak) formal theory $T$ that incorporates some arithmetic, say Peano arithmetic ($\mathbf{PA}$).
Let $m$ be the number of integers $0 \leq x ≤ 2^{L+1}$, such that, $K(x) > L$. They argue:
Equation 2 is just $\Sigma_1$-completeness of $T$ over formulas and $r = 2^{L+1} + 1 − i$.
My issue is with step 4. Kritchman-Raz seem to interchange freely two different types of existential quantifiers concerning $y_1,\dots,y_r$, one formal within the theory $T$ (as in step 1,2), and one in the metatheory in step 3. But $\exists \text{ different } y_1,\dots,y_r \, \varphi(y_1,\dots,y_r)$ within a formal theory doesn't guarantee existence of concrete instances (meta theoretic numbers) $y_1,\dots,y_r$ such that $\varphi(\bar{y_1},\dots,\bar{y_r})$ within that same formal theory, in general. And it seems to me this is exactly what Kritchman-Raz are doing here. However, I'm very much a beginner w.r.t. formalizations in arithmetic. Is my analysis correct? If so, how do we fix it?
I asked a similar question first on MSE, but got no response (even after having set a bounty). I hope this question is on the appropriate level for MO. If not, my apologies.