Be careful. That's a naive view, and drawing more conclusion than I think you mean.

This it more like it: For any consistent, finite axiomatized formal system that is sufficiently expressive (such as the Principia Mathematica), you can construct a sentence in the language of that formal system that asserts its own un-provability. Therefore, there does not exist a mechanistic method for enumerating over all true statements in the language of that formal system.

By stating "there are some true things that cannot be proved" goes too philosophy deep, and is outside of our pay-grade. Just consider: humans don't reason based on mechanistic principles - and there's no proof as to the expressability of natural language (though we can be sure it's aggravatingly inconsistent)

EDIT: I just want to say that in general, if someone does not really grasp the technical notion of a formal system, consistency, expressiveness, provability, soundness, or recursive enumeration, then it is basically impossible for them to appreciate the incompleteness theorems, and they are very likely to grossly misrepresent it.

> humans don't reason based on mechanistic principles

Do you support an empiricist view of logic then (http://en.wikipedia.org/wiki/Is_logic_empirical%3F) ? That we justify logical rules because they so strongly correspond with our own experiences?

Not really. I'm just saying we don't go around all day doing logic-algebra in our head and saying only true, consistent things :)

Ahh, fair enough. I'd have to agree with you there. My guess is that that plus being able to inductively generate axioms from experience are largely what let us escape that particular weakness of formal systems.

Provability is relative to a formal system. Whether there are _absolutely undecidable_ statements is more controversial, and still an open question in the philosophy of mathematics. Gödel's disjunction is part of this literature: "Either … the human mind … infinitely surpasses the powers of any finite machine, or else there exist absolutely unsolvable diophantine problems." Soloman Feferman has written about this, for instance in a 2006 Philosophia Mathematica paper.

http://math.stanford.edu/~feferman/papers/dichotomy.pdf

If anything is absolutely undecidable, I suspect it will be P=NP.