Peano Arithmetic consists of axioms P_1, P_2, … 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 ↔ ~Prov_T(⌜G⌝)

(Needless to say Prov_T(⌜G⌝) means G is provable in T.)

We can add all the instances of the reflection schema to T:

Prov_T(⌜phi⌝)  →  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, … P_7 plus Prov_U(⌜phi⌝) → phi.

My question is this. How do we add the reflection schema to a theory such that the proof predicate Prov_U() includes the reflection schema itself. Would the following do the trick?

P8: P_1 & P_2 & … & P_7 & Prov_T(⌜phi⌝) → phi

Is there any publication that addresses this issue?