# Formalization in PA in the Kritchman-Raz proof

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?