> 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.