Peano Arithmetic consists  of axioms $P_1, P_2, \ldots P_7$ plus first order classical logic. Let us call this theory $T$. This theory has its unprovable Gödel’s sentence $G$ such that
$$
G\leftrightarrow \sim\mathrm{Prov}_T(⌜G⌝)
$$
(Needless to say $\mathrm{Prov}_T(⌜G⌝)$ means $G$ is provable in $T$.)

We can add all the instances of the reflection schema to $T$:
$$
\mathrm{Prov}_T(⌜\phi⌝)  \to  \phi
$$
This new theory proves $G$, but has its own unprovable Gödel’s sentence $G’$.

Let $U$ be a theory consisting of $P_1, P_2, \ldots P_7$ plus $\mathrm{Prov}_T(⌜\phi⌝) \to \phi $.

**My question is this**. How do we add the reflection schema to a theory such that the proof predicate $\mathrm{Prov}_U(\cdot)$ includes the reflection schema itself. Would the following do the trick?
$$
P_8:  P_1\; \& \;P_2 \;\& \;\ldots \;\&\; P_7 \;\& \;\mathrm{Prov}_T(⌜\phi⌝)\to \phi
$$
Is there any publication that addresses this issue?