> I also don't see mathematicians using mathematical logic to prove theorems in "ordinary" mathematics, hence the comment about "business as usual". You don't

> I also don't see mathematicians using mathematical logic to prove theorems in "ordinary" mathematics, hence the comment about "business as usual". You don't know does not equal to that not existing. http://www.cs.miami.edu/~tptp/OverviewOfATP.html http://www.cs.miami.edu/~tptp/OverviewOfATP.html People are even making money using formal reasoning. So please, take time to learn more before disparaging entire fields. Btw, I know about the incompleteness theorems. I teach a course centered around that. Let me ask you a related question: do you stop programming because many of the tasks associated with programming are Turing-uncomputable? (checking if a program halts, checking if two programs compute the same function etc.)