Roger Penrose asked how computer systems might ever be able to deal with the concept of infinity. Think of this statement: “Add two odd numbers together; then you always get an even number.” That’s a statement about an infinite number of things, and you don’t have to think too hard to realize that this is true for all numbers – and that’s an infinite number of numbers. Note that this statement is mathematically proven. It’s a mathematical truth. Now, imagine you put this statement (adding two odd numbers gives an even number) on a computer system.
The question then is, “Can a computer system prove this mathematical truth?” To prove this statement, we need a set of rules (axioms). These rules will then give you a proof. So, if you want to use these rules, you need to believe that each rule is true and that the set of rules you want to use is consistent. Consistency (in rough terms) means that you can’t derive nonsense (contradictions) from these rules (e.g., 2 equals 3).
In mathematics, these rules are incredibly simple. For example, imagine the natural numbers x and y. One rule (the Peano Axiom) says, “When x equals y, then y equals x.” That’s easy, so we believe that this rule is true. What does that mean? The Austrian mathematician Kurt Gödel showed (in rough terms) that if you have a set of rules, you can construct a statement (e.g., adding two odd numbers always gives an even number) within that set of rules that has the strange property that it is true (on the one hand) but there is no proof of that statement within this set of rules (no matter how big that set of rules is).
This is what is known as Gödel’s Theorems. These theorems place a hard limitation on what we might be able to know in mathematics. In simple terms, this means that mathematical truths cannot (always) be reduced to mechanical rules. This (in turn) implies that mathematical truths cannot (always) be checked by computer systems. As a result, there is a gap between truth and proof, since not all true mathematical statements can be proved. For this reason, Penrose (among many others) concluded that understanding is not rule-driven. He claimed that what goes on in our brains is not rule-driven. It’s not algorithmic, so it’s not machine decidable. Astounding.
Not convinced yet? Then watch this explanation by Marcus du Sautoy.