Godel was quite at home with the idea that as logic and mathematics progress, machines would increasingly take over the “Yes-No” part of the enterprise. Any notion that Godel would have embraced an argument by analogy from the undecidability of FOL to the perpetual intractability of the k-symbol provability problem is utterly misguided: He writes: “[I]t would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine.”

From Bringsjord, “An Argument for P=NP”