What does Godël’s Incompleteness Theorem actually mean and imply? I just saw Ted-Ed’s video on this topic and didn’t fully understand what it means or what the implications of this are.
In: 742
In mathematics there are axioms and theorems. We consider axioms as something given and theorems as something we can prove. But what is a proof? It is just words, and it can be incorrect. How can we verify the proof? Could there be mistakes? If 10 mathematicians say it’s correct, is it enough or not? 100 mathematicians? 1000?
All this is questionable. But what if we can design a system where it will be possible to formally verify any proof? A system where there will be a procedure to check any proof of any theorem and tell whether this proof is correct or not. For example, a computer would be able to do it. Then we will have a big advantage. But is it possible?
Before even making such a system we can formulate its fundamental properties. There should be no possibility to prove and disprove the same theorem at the same time (obviously) and there should be a possibility to prove any correct theorem (within the bounds of the system).
Goedel proved that this is impossible for some formal systems. The important word here is “some”. For example, formal 1st order logic is complete and non-contradictory. Also, any modular arithmetic is complete and non-contradictory. But traditional infinite arithmetic is not.
What are properties of a system that make it incomplete? First of all it has to be a formal system, i.e. where it is possible to express any proof (and any theorem or axiom) as a number or a string of symbols of any kind and there is an algorithm that decides on the correctness of this proof. Second, the formal arithmetic should be a part of the system. Then this system is incomplete.
Why is this theorem important? It states that a formal system can be incomplete. So – no formal system will save mathematics from possible errors.
The similar theorem exists in theory of algorithms. It states that it is impossible to make a computer program that will tell us whether any given program will run forever or will stop in some distant future.
Latest Answers