Strictly speaking, he showed incompleteness or inconsistency for any theory that includes arithmetic and that only when you are limited to certain methods of proof. IIRC arithmetic was later proven correct using transfinite induction.
And any way, the reason to even bring this up is that there is no magical proof machine that can be constructed to prove these statements (EVO,ID,stone soup,etc.), and so will rely on some Human to say otherwise.
In 1931 the mathematician and logician Kurt Godel proved that within a formal system questions exist that are neither provable nor disprovable on the basis of the axioms that define the system. This is known as Godel's Undecidability Theorem. He also showed that in a sufficiently rich formal system in which decidability of all questions is required, there will be contradictory statements. This is known as his Incompleteness Theorem. In establishing these theorems Godel showed that there are problems that cannot be solved by any set of rules or procedures; instead for these problems one must always extend the set of axioms. This disproved a common belief at the time that the different branches of mathematics could be integrated and placed on a single logical foundation.
Alan Turing later provided a constructive interpretation of Godel's results by placing them on an algorithmic foundation: There are numbers and functions that cannot be computed by any logical machine.
More recently, Gregory Chaitin, a mathematician working at IBM, has stressed that Godel's and Turing's results set fundamental limits on mathematics.
These results, along with quantum uncertainty and the unpredictability of determinstic (chaotic) systems, form a core set of limitations to scientific knowledge that have only come to be appreciated during this century.