I've been trying to get acquainted with proof theory (particularly ordinal analysis) as part of a school project, and am trying to tease out the story behind the appearance of infinite ordinals in a couple of related (I think?) contexts.
Context 1: In Takeuti's Proof Theory, he presents a proof of the consistency of arithmetic that involves assigning ordinals to the sequents appearing in a proof, based on the inference rules which produce them. In particular, the lower sequents of Cut and Ind rules have ordinals of the form $\omega^\alpha$ for some appropriate $\alpha$.
Context 2: Schütte and Pohlers both make use of a semi-formal system involving a relation $\vdash^\alpha_\rho\Delta$ between ordinals $\alpha,\rho$ and a finite set of sentences $\Delta$ (of whatever language). In the development of the semi-formal system, there are theorems like
For any pseudo-$\Pi^1_1$ sentence $F$ provable in $\mathsf{NT}$ [a theory mutually interpretable with $\mathsf{PA}$], there are finite ordinals $m,r$ such that $\vdash^{\omega+m}_rF$.
or
$\vdash^\alpha_{\beta+\omega^\rho}\Delta$ implies $\vdash^{\varphi_\rho(\alpha)}_\beta$
where $\varphi$ is the binary Veblen function.
Why are these infinite ordinals showing up in proof theoretic devices? What aspects of the structure of a proof are they here to capture?
I'm not at all made uncomfortable by infinite things in general, but they seem odd in these contexts where proofs seem to be entirely finite objects (Takeuti, for instance, doesn't formulate arithmetic with any infinitary inference rules).