I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book.
To be wore precise, we have a finite subsystem $\mathcal{T}$ of PA, and a formula $A$ with one free variable, predicate $\text{Thm}_{\mathcal{T}}(x)$ expressing a provability in $\mathcal{T}$ of the formula with the Gödel number $x$. The we want to prove a statement that PA proves $\text{Thm}_{\mathcal{T}}(\ulcorner A[\bar{x}]\urcorner)\Rightarrow A[x]$, where $\ulcorner x\urcorner$ is a Gödel number for $x$.
The reasoning started with noticing that axioms of $\mathcal{T}$ can be packed into a formula $B$, and noticing that the provability of a formula $C$ in $\mathcal{T}$ reduces to the provability of $B\Rightarrow C$ in sequent calculus LK (here it's also not super clear, but has some sense for me as $\mathcal{T}$ is finitely axiomatizable). Then, as I understand, we say that the provability of $B\Rightarrow C$ in sequent calculus LK transforms into the fact of provability of $B\Rightarrow C$ in PA (this is the first more or less vague step where I'd like to have more comments, but I assume it's connected to the fact that provability in LK is transformed to that of in PA by induction).
Therefore, we have $\text{Thm}_{\textbf{LK}}(\ulcorner B\Rightarrow A[\bar{x}]\urcorner)\Rightarrow(B\Rightarrow A[x])$. And the second question is about transforming this fact into the one in the theorem statement (where I also only have a slight guess that we do have $B$ on our hands in PA, but still there is something to say).
I would be glad for any comments and suggestions.