I am sorry for the following question, because the actual answer to this question is in the beautiful works of Feferman and Jeroslow, but, unfortunately, I havn't any time to go into that specific field right now and maybe some of you is aware of the answer.

The situation with Gödel's second incompleteness theorem is quite delicate. Let Pf(a, b) means that a is the Gödel number of proof of statement with Gödel number b and Neg(a, b) means that b is the Gödel number of negation of statement with Gödel number a. The main result of Gödel's work is representability of predicates Pf and Neg in formal arithmetic. Knowing that, we can define the Consistency of formal arithmetic in formal arithmetic as follows:

" it is not the case that there exist a statement A such that A and (not) A are provable in formal arithmetic " or in the language of formal arithmetic:

$$\forall x_1, x_2, x_3, x_4 [\neg (\operatorname{Pf}(x_1, x_3) \wedge \operatorname{Pf}(x_2, x_4) \wedge \operatorname{Neg}(x_3, x_4))].$$

Let's denote last proposition by W. Gödel's second incompleteness theorem says that W is not provable in formal arithmetic, i. e. the consistency of formal arithmetic is not provable in formal arithmetic. But Solomon Feferman in his remarkable paper of 1960 "Arithmetization of metamathematics in general setting" have found other formalization of consistency of formal arithmetic W' that is provable in formal arithmetic (see notes by E. Mendelson to the second theorem in formal arithmetic chapter of his "Intoduction to Mathematical logic"). Jeroslow ("Consistency statements in formal theories"), thereafter, studied consistency statements in a broader way.

Can someone explain the nature of W'? (obviously, $W\Leftrightarrow W'$ can not be proven in PA).

Can we interpret the provability of W' as the proof of consistency of formal arithmetic in formal arithmetic?

How well are various consistency statements grasped today?

Thanks in advance.