# First Incompleteness Theorem made exact…

First Incompleteness Theorem, according to WIKIpedia: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F."

This is disturbing. Can I instead say this more exact version: "Any consistent formal system F, which contains the Peano axioms, is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F."

• It would be more accurate to replace "Peano axioms" by "Robinson axioms". – Asaf Karagila Jan 23 '18 at 19:39
• Even more, it is enough to talk of interpretability rather than containment. Also, the "formal system" should be a recursively enumerable (axiomatization of) a first-order theory. And if you want to be yet more exact, you should say something about the meta-theory in which this result is being established. – Andrés E. Caicedo Jan 23 '18 at 19:52
• Aside: you need additional hypotheses on $F$; e.g. being generated by a set of axioms that is recursively enumerable. – Hurkyl Jan 23 '18 at 19:53
• @AsafKaragila Are the Robinson axioms minimal, in the sense that any theory that has the incompleteness property can do Robinson arithmetic? – eyeballfrog Jan 23 '18 at 19:55
• Hold on! The very Wikipedia page you (the OP) are quoting has a whole section already explaining what it takes to enable "a certain amount of elementary arithmetic [to be] carried out". Perhaps reread the whole page more carefully?? – Peter Smith Jan 23 '18 at 20:18