What Gödel showed was that any such precise (‘formal’) mathematical system of axioms and rules of procedure whatever, provided that it is broad enough to contain descriptions of simple arithmetical propositions (such as ‘Fermat’s last theorem’, considered in Chapter 2) and provided that it is free from contradiction, must contain some statements which are neither provable nor disprovable by the means allowed within the system.