Limit case of PA theories? It seems to me that if one is to "believe" in PA, then one must "believe" in Con(PA) (this is, in some sense, what it means to believe in the theory!). Similarly, I think such a wishful thinker might believe in Con(PA+Con(PA)) also and then Con(PA+Con(PA)+Con(PA+Con(PA))) etc.
I wondered when considering this - is there such a well-defined concept as the limiting case for things like it? As in, can you construct a theory that for all $n\in\mathbb{N}$ has its own consistency expressed, as above, to the $n$th level in a meaningful way? If so, is this a well-known theory and can we give it a proof-theoretic ordinal?
I apologise if the above is completely nonsensical, as I am a complete beginner in logic, set theory etc. and self-teach because of interest.
 A: You can certainly form
$$ T_0 = PA \\ T_1 = PA \cup \{\mathit{Con}(PA)\} \\ \vdots \\ T_{n+1} = T_n \cup \{\mathit{Con}(T_n)\} \\ \vdots $$
for every $n$. And all of these theories will be true in the actual integers, or so you will have to believe if you think there's anything deserving of the name "actual integers" in the first place.
(Remember that PA is not what creates the integers; it is a formal system for deducing facts about the integers we already feel we know what are from elementary school).
Then you can go to the limit with
$$ T_\omega = \bigcup_{n\in\mathbb N} T_n = PA \cup \{\mathit{Con}(PA), \mathit{Con}(T_1), \mathit{Con}(T_2), \ldots \} $$
This theory is still true in the actual integers and therefore consistent. It trivially proves all of the $\mathit{Con}(T_n)$s we have seen so far -- but it does not prove $\mathit{Con}(T_\omega)$! So it makes sense to consider $T_{\omega+1}$, and then we're in business again, continuing the process into transfinite ordinals.
However, something starts to go awry when we get to "sufficiently complex" ordinals. Writing $\mathit{Con}(T_\alpha)$ depends on having a formula that represents the property of being the Gödel number of one of the axioms of $T_\alpha$, which means that we need an arithmetical description of $\alpha$ itself. And there can easily be several different formulas that describe $\alpha$ but which $T_\alpha$ itself doesn't prove are equivalent. This will lead to several possible candidates for $\mathit{Con}(T_\alpha)$. This problem becomes acute when we reach the limit of iterating "$\alpha \mapsto$ the proof-theoretic ordinal of $T_\alpha$".
So now it is questionable whether our process for generating new theories is well defined anymore. Still, if we don't care about being constructive, we might be able sidestep that by specifying that each $T_\alpha$ is represented by the first formula that represents it in the true integers, in some appropriately and carefully defined way. Though perhaps not; the ways I can immediately imagine doing this turn out to be second-order when you look closely at them.
However, when we get to sufficiently large (but still countable) $\alpha$ things break down completely for the opposite reason, namely that there is no finite arithmetical formula that represents $\mathit{Con}(T_\alpha)$ in any recognizable way. (It must be so because there are only countably many arithmetical formulas but uncountably many countable ordinals).
