This is actually a common misconception perpetuated by zealous Scientific American reporters (and cognitive scientists :) . Many complete, consistent self-justi

This is actually a common misconception perpetuated by zealous Scientific American reporters (and cognitive scientists :) . Many complete, consistent self-justifying axiom systems exist today. Formal verification schemes employing metamathematical logic also exist and can be both complete and consistent. Even MORE systems have been created that can verify their own semantic tableux exclusively (and by extension are consistent & decidable). Even still there are systems like Presburger Arithmetic, which can by proven decidable (although they cannot prove themselves) On page 12 of the english translation (and possibly the original german), Godel addresses certain criteria for distinguishing a sufficiently powerful system (as well as recursively axiomitizable, etc). I have personally written such a software verification scheme, and even have an inferior interaction mode for SMT solvers that can help you verify such schemes (it's in my profile & github). There are also great books like the extremely cheesily-named graduate textbook: "Your Guide to Automated Reasoning", that examine this issue from every perspective imaginable.