> Gödel completeness theorem is the really big deal. Except it isn't. That computer program turns out to be one of those wretched tree search ones that soon bogs down. The real problem turns out to be the combinatorial explosion inherent in unstructured search through the Herbrand universe.
Yup. Incompleteness is sort of a red herring. P≠NP (even though unproven) yields the real, practical, painful incompleteness.
P versus NP could be a red herring too.
If P=NP, but the best asymptotic solution is n^7, and it has so much overhead that the best practical solution is n^9, then it doesn't really matter that it isn't exponential. It's still unsolvable for easily accessible problem sizes.