I always feel like the most impressive part of these kinds of discussion is, the following question has already been answered: "Can you devise a mechanical proc

I always feel like the most impressive part of these kinds of discussion is, the following question has already been answered: "Can you devise a mechanical process that can, given an axiomatic system in first-order logic and a predicate, decide whether the predicate can be deduced from the axioms?" The answer is "no." That people still believe in future self-programming computers in spite of that is just---strange.