We study the Second Incompleteness Theorem, G2, in the Feferman-style. This means that we work with a fixed provability-predicate but allow the representations of the axiom set to vary. Feferman observed that the axiom set of Peano Arithmetic, PA, has a Π01-representation for which PA proves its own consistency.

We isolate a condition that Feferman’s example fails to satisfy. This condition gives a reasonably general version of G2. We show that this version yields a proof of G2 for Σ01-semi-numerations of the axiom set which works even if the theory itself is not recursively enumerable. We discuss an interesting example that illustrates that we may have G2 even in the absence of the Löb conditions.