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.



Clarification of Gödel's second incompleteness theorem
The key idea Feferman is exploiting is that there can be two different enumerations of the axioms of a theory, so that the theory does not prove that the two enumerations give the same theory.


Here is an example. Let $A$ be a set of the axioms defined by some formula $\phi(n)$ (that is, $\phi(x)$ holds for exactly those $x$ that are in $A$). Define a new formula $\psi(n)$ like so:


$\psi(n) \equiv \phi(n) \land \text{Con}( \langle x \leq n : \phi(x)\rangle)$


Where Con(σ) is a formula which says that no contradiction is provable from the axioms listed in the sequence σ.


In the case where $A$ is the set of axioms for a suitable consistent theory $T$ that satisfies the second incompleteness theorem, the following hold:


(1) In the standard model, we have $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because $T$ really is consistent. 


(2) T does not prove that $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because this equivalence implies that T is consistent. 


(3) If we use $\psi$ to define a formula Conψ(T), then T will prove (under the assumption that the empty theory is consistent, if this is not provable in T) that the theory defined by ψ is consistent. However, T will not prove Conφ(T), which is the usual consistency sentence for T.


This kind of example is presented in a more precise way in Feferman's 1960 paper that you mentioned, along with precise hypotheses on the theory and sharper results. 


My opinion is that we cannot regard a proof of Conψ(T) as a proof of the consistency of T, because although φ and ψ are extensionally identical, they do not intensionally represent the same theory. Feferman expresses a similar idea on his p. 69. Of course, this is a matter of philosophy or interpretation rather than a formal mathematical question. 




---


***Addendum***


The difference between extensional and intensional equality is easiest to explain by example. Let A be the empty set and let B be the set of integers larger than 1 that do not have a unique prime factorization. Then we know B is also the empty set: so A and B are *extensionally* equal. But the definition of B is much different than the definition of A: so A and B are *intensionally* different. 


This distinction is often important in contexts like computability and formal logic where the things that you work with are actually definitions (also called codes, indices, Gödel numbers, or notations) rather than the objects being defined. In many cases, extensional equality is problematic, because of computability or effectiveness problems. For example, in my answer above, we know that φ and ψ define the same set in the real world, but this fact requires proof, and that proof may be impossible in the object theory we are dealing with. On the other hand, intensional equality is easy to decide, provided you are working directly with definitions. 


