[lacewing]

Right, if you're a software engineer, the realization that the two theorems are nearly-equivalent really takes the air out of a lot of the existential philosophizing around Gödel's incompleteness.

Gödel's argument basically says that any system of mathematics powerful enough to implement basic arithmetic is a computer. This shouldn't be surprising to software engineers because the equivalency between Boolean logic and arithmetic is easy to show. And if you have a computer, you can build algorithms whose outcome can't be programmatically decided by other algorithms.

[cobbal]

I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.

[voxl]

There is no logic that is more expressive than a Turing machine. In fact, just about every logic you know can only expressive necessarily terminating programs. There is a bit of an issue on what exactly someone means by expressive, but if we're talking programs that compute outputs from inputs (without caring about the invariants imposed on said programs) then this holds.