Let $PA_0$ be $PA$, for every ordinal $\alpha$, let $PA_{\alpha+1} $ be $PA_\alpha + Con(PA_\alpha )$ and if $\alpha$ is limit ordinal let $PA_\alpha$ be $\cup_{\beta<\alpha} PA_\beta$.
Is every $Con(PA_\alpha )$ statement an encoded first order arithmetical statement, even when $\alpha$ is limit?
Which is the minimum ordinal $\gamma$ for which $PA_\gamma = PA_{\gamma+1}$?
Is $PA_\gamma$ the true Arithmetic?
@Andrès E. Caicedo:
(Edit after comment):
I read https://mathoverflow.net/questions/153272/how-strong-is-the-iterated-consistency-of-zfc and i found it partially answer to my question. This point in the answer of @Andrès E. Caicedo: for me needs some clarifications "(Stopping at $\omega_1^{CK}$ is just an artifact of my wanting to keep all the theories recursive. I don't quite see how to make sense of iterating these theories beyond the recursive ordinals. What do we mean by Con(T) in such a case, since T is no longer r.e.? Of course, we can make sense of this semantically, and just require the existence of models (after some pains formalizing this, as the relevant language in which the theories are formulated would evolve with the ordinal), but even then it seems to me we need to argue that the models are sufficiently correct to see the relevant ordinals, and this seems a distraction from the main goal.)"
Does it mean that consistency at $\omega_1^{CK}$ step by model-theoretic approach could be formulate in a Set theoretic language by a formula intuitively true about not r.e ordinals, but not logical consequence of all True Arithmetic?