- #1
- 210
- 53
If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?
If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?
Godel's incompleteness theorem implies that one can't go on like that. You will eventually get to theorems that are impossible to prove within the system.
http://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems
Yes. At any given point in time it will only have given us finitely many theorems, but there are infinitely many (assuming a moderately interesting axiom system and a computer with finite computing powers).If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?
The question is why? You won't find anything significant because of all the useless theorems and proofs.
It is similar to the idea that a computer could enumerate all images and would therefore have painted all current, past and future art. Or by having a computer go through all combinations of letters it will eventually write any story.
For theorems it's actually a lot like art. Most theorems are worthless and the computer won't be able to rule out garbage theorems.It's different from art. In art a computer cannot sort out a good picture from garbage. In case of mathematical theorems proof, a computer can clearly rule out the invalid ones. Using it to derive all the mathematical proofs will be nearly impossible. But for a given specific problem, a computer may be able to find proof for it and rule out the invalid ones.
If there are 5 different symbols it would take 5^1000000 combinations to reach a proof of length 1 million. If the computer could go through 5^10000 combinations each nanosecond (5^10000 has ~7000 digits), then it would still take 10^33000 years to reach a proof of length 40000 symbols. Given all the short-cuts and cross-references mathematicians employ I suspect that we already have many proofs much larger than 10million symbols if they were written down explicitly.At least we can prove that, there is no proof exist for, say Reimann hypothesis, in x number of steps. x could be in millions.
What would be true is that every theorem and proof would eventually appear, but you will never have them all (clarification: what this means is that given a theorem or a proof you can be confident that if you wait long enough at some point the computer will output it).
Necessarily not.What would be true is that every theorem and proof would eventually appear, but you will never have them all (clarification: what this means is that given a theorem or a proof you can be confident that if you wait long enough at some point the computer will output it).
Not necessarily.
In each axiomatic system that contains arithmetics, there exist a sentence that is true, but there is no proof of it in this axiomatic system.If it just keeps enumerating proofs, at some point we will get to arbitrarily long proofs, so any proof of finite length N will be covered
But then it doesn't matter. I only claimed that every proof will eventually appear. I did not claim that for every true theorem we would eventually find a proof.In each axiomatic system that contains arithmetics, there exist a sentence that is true, but there is no proof of it in this axiomatic system.
You underestimate how many proofs are possible; at best, x could be dozens if we are enumerating proofs by length, if we want to see the results in our lifetime.At least we can prove that, there is no proof exist for, say Reimann hypothesis, in x number of steps. x could be in millions.