 Gödel originally only established the incompleteness of a particular though very comprehensive formalized theory P, a variant of Russell’s type-theoretical system PM (for Principia Mathematica, see the sections on Paradoxes and Russell’s Type Theories in the entries on  type theory  and  Principia Mathematica),  and all extension of P with the same language, whose set of axioms is primitive recursive. He also suggested, though did not demonstrate, that the proof could be adapted to apply also to the standard axiom systems of set theory such as ZFC. Though it turns out that Gödel in fact already had a very general result, it was, at the time, unclear just how general this really was (see also  Section 5).