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?

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?