As Gödel himself stressed, back in 1931, his second theorem is irrelevant to any sensible consistency problem. In any case, if ConF is in doubt, why should it be proved in F (and not in an incomparable system)? […] He knew only too well the publicity value of this catch word [i.e. “consistency”], which –contrary to his own view of the matter– had made his second incompleteness theorem more spectacular than the first.”
Georg Kreisel, 1980, “Kurt Gödel. 28 April 1906-14 January 1978”, Biographical Memoirs of the Fellows of the Royal Society, 26: 174.
I will comment on this passage in relation to the several projects of creating formal theories of arithmetic which, unlike Peano Arithmetic, could possibly prove their own consistency. I distinguish between those formulas of a formal theory F which, under their canonical interpretation, (i) carry the information that F is consistent and (ii) those that do not carry the information that F is consistent. ConF trivially belongs to (ii). Assume that we believe in F’s soundness, and thereby its consistency. If a formula does not carry the information that F is consistent, it is a sensible project to try to prove/disprove this formula in F: one believes that F always tells the truth, and so, one will believe F’s verdict on this formula, which says something different from the things one already believes in. On the other hand, if the formula carries the information that F is consistent, and we already believe that F is sound, and thereby consistent, F’s possibly affirmative verdict is of purely algorithmic interest. We would believe the formula, but only because we already believe in F’s soundness, and thereby its consistency. Finally, if we do not already believe in the soundness of F, F’s potentially affirmative verdict on any formula belonging to (ii), would, in itself, have no epistemological value whatsoever with regard to F’s consistency. I will elaborate on this argument and apply it to arithmetics using Rosser provability.