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 sufficientl

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.