 Here \(\rform_{\Phi}\) and \(\proof_{\bT_i}\) are arithmetized formalizations of \(\Phi\) and the proof relation in \(\bT_i\), respectively, i.e., \(\rform_{\Phi}(x)\) expresses that x is the Gödel number of a formula in \(\Phi\) while \(\proof_{\bT_i}(y,x)\) expresses that y codes a proof in \(\bT_i\) of a formula with Gödel number x.