Well, “(Ex)Prf_T(x, ⌜F⌝) --> F” says that if there exists a proof of F then F is the case. This is neither an axiom nor a theorem of PA. This may seem odd. For how is it possible that if a proof of F exists we cannot conclude F. My understanding is that even if a proof “exists” it could be infinitely long. Thus we may not be able to effectively prove F.

Adding “(Ex)Prf_T(x, ⌜G⌝) --> G” (G is Gödel’s sentence) creates the theory T’ which is also incomplete and has its own Gödel’s sentence G’. My question is how to add the entire hierarchy at once. The resulting system will be inconsistent, but there is a purpose to this madness.

Recursive definitions also look circular, but they are not. I am pretty sure this can be done. I was told something to the effect that it was a fixed point of the hierarchy of theories

T' = T + (Ex)Prf_T(x, ⌜F⌝) --> F
T" = T' + (Ex)Prf_T'(x, ⌜F⌝) --> F
. . .

(don't quote me), or something like that. And that is perhaps somehow equivalent tp P8. Not sure what fixed point means in this context or how it can be constructed.
(BTW, I know the resulting system is inconsistent.)

You are right. I have written papers about this. Here is one.
http://arxiv.org/abs/1510.04393