Gödel's Theorem, as a simple corollary of Proposition VI is frequently called, proves that there are arithmetical propositions which are undecidable (i.e. neither provable nor disprovable) within their arithmetical system, and the proof proceeds by actually specifying such a proposition, namely the proposition g expressed by the formula to which "17 Gen r" refers [188]. g is an arithmetical proposition; but the proposition that g is undecidable within the system is not an arithmetical proposition, since it is concerned with provability within an arithmetical system, and this is a metaarithmetical and not an arithmetical notion. Gödel's Theorem is thus a result which belongs not to mathematics but to metamathematics, the name given by Hilbert to the study of rigorous proof in mathematics and symbolic logic.