4 ms·

I have to say something here, because this is complete nonsense. Nothing in Godel's incompleteness theorems says that new theorems can't be found. It says theo

I have to say something here, because this is complete nonsense. Nothing in Godel's incompleteness theorems says that new theorems can't be found. It says theorems can't be enumerated, which actually means the opposite--there's always something new to find in a sufficiently strong system of mathematics. Not that there are theorem-enumerators of significant power in the first place. Furthermore, proofs generally do not introduce new axioms and a proof that does, that isn't intended to be foundational, would be considered unsound.

fatbird 14y ago
Agree with everything you say about Godel. I'm not sure what your last line means, though. Speaking strictly in terms of axioms and derived theorems, that seems fine, but in thinking of, say, Wiles' proof of Fermat's Last Theorem, which wended broadly through various branches of math, extending them or perhaps inventing them as needed, it seems incorrect to say this. I'm not sure whether you want to characterize Wiles as introducing new axioms, but he certainly wasn't simply deriving new theorems that could have been computationally enumerated. Perhaps I'm wrong; I'm not a mathematician. But my understanding of Godel, axiomatic systems, and proof engines is that what they do simply isn't comparable to, say, what Mochizuki did with the ABC Conjecture.
xamuel 14y ago
Minor nitpick: Godel does not say theorems can't be enumerated, obviously they can be, just use brute force. Rather it says theorems provable from sufficiently strong axioms can't be decided. So if you want to know whether your axioms prove 1=0, you can start enumerating all the theorems they prove, and if they do prove 1=0, eventually you'll see it, but if not, there's no way to "go far enough" to rule out the possibility that 1=0 will appear later on in the enumeration.

4 ms·

I have to say something here, because this is complete nonsense. Nothing in Godel's incompleteness theorems says that new theorems can't be found. It says theo

by cynicalkane 14y ago

fatbird 14y ago
Agree with everything you say about Godel. I'm not sure what your last line means, though. Speaking strictly in terms of axioms and derived theorems, that seems fine, but in thinking of, say, Wiles' proof of Fermat's Last Theorem, which wended broadly through various branches of math, extending them or perhaps inventing them as needed, it seems incorrect to say this. I'm not sure whether you want to characterize Wiles as introducing new axioms, but he certainly wasn't simply deriving new theorems that could have been computationally enumerated. Perhaps I'm wrong; I'm not a mathematician. But my understanding of Godel, axiomatic systems, and proof engines is that what they do simply isn't comparable to, say, what Mochizuki did with the ABC Conjecture.
xamuel 14y ago
Minor nitpick: Godel does not say theorems can't be enumerated, obviously they can be, just use brute force. Rather it says theorems provable from sufficiently strong axioms can't be decided. So if you want to know whether your axioms prove 1=0, you can start enumerating all the theorems they prove, and if they do prove 1=0, eventually you'll see it, but if not, there's no way to "go far enough" to rule out the possibility that 1=0 will appear later on in the enumeration.