Clear translation with some supporting info can be found here. Also, the description in I am a Strange Loop is really helpful.

Goal was for a *complete* and *consistent* interpretation of mathematics:

The most comprehensive current formal systems are the system of Principia Mathematica (PM) on the one hand, the Zermelo-Fraenkelian axiom-system of set theory on the other hand. These two systems are so far developed that you can formalize in them all proof methods that are currently in use in mathematics, i.e. you can reduce these proof methods to a few axioms and deduction rules.

Hence, we have in front of us a theorem that states its own unprovability. The proof method we just applied is obviously applicable to any formal system that on the one hand is expressive [176] enough to allow the definition of the concepts used above (in particular the concept “provable formula”), and in which on the other hand all provable formulae are also true. The following exact implementation of the proof will among other things have the goal to replace the second prerequisite by a purely formal and much weaker one.