No matter how many articles I read on this subject I cannot comprehend how it proves what it proves. I do well with words and rhetorics, philosophy and science – but as soon as you add numbers my mind goes blank. Not very helpful when those fields often rely on equations and models for explanations and proof. I can somewhat understand equations if explained in a simple or cohesive way – but if at all possible analogies or just word-centric explanations would be very helpful.
In: 25
You can restate the theorems in terms of programs.
You can encode proof-based math inside of a computer program, by telling the program what statement is allowed to follow another statement. For example, I can tell a program that if I have a statement x = x, I’m then allowed to say x + 1 = x + 1. Then if I have the proof
0 = 0
therefore 1 = 1
The program can verify that this is correct based on the rules I gave it. This is a trivial example, but all of math can be formalized in this way – in fact that’s what formalization means, judging the truth of statements based on their form rather than your interpretation of what it refers to.
However, the converse is also – you can describe computer programs from inside of math. The details are kind of complicated, but the gist is that since we can think of the parts of a computer abstractly (the memory is a long array of bits, the processor state changes in a sequence, each processor change is accompanied by a change to one location in memory), this abstraction can be conceptualized as mathematical objects, and the behavior of those mathematical objects can be described using math as well.
So, you can construct a really nasty program, which tries to find a proof of its own behavior, and if it finds such a proof changes its behavior in response. For example, the behavior might be “this program goes into an infinite loop”. If there’s a proof of this, the program will immediately stop, but if there’s a *disproof*, the program will go ahead and loop. This would mean the mathematical system is self contradictory, and its only choice is to be agnostic about this behavior of this program, neither confirming not denying whether it goes into an infinite loop.
This is the first theorem, which effectively states that for all mathematical systems that can 1) encode the behavior of programs and 2) be modeled by programs, there will be some statements that can’t be proved or disproved.
The second theorem, as others have stated, gives a particularly annoying example of such a statement – whether or not the mathematical system is free of contradictions. This can’t be disproved because then we don’t have a valid mathematical system, and it can’t be proved because of a slightly more technical argument along similar lines (having such a proof would let you build another nasty program that has contradictory behavior).
I recommend the book *Godel’s Proof* by Nagel and Newman, it is probably the closest to ELI5 of that proof that is humanly possible, very easy to understand and short for a book, but thorough enough that you get the idea.
If you have the time, there is a fantastic book – a top 5 of all time for me – called Gödel, Escher, Bach that explains it in a wonderful and understandable way.
You can turn any string of letters into a number. Just replace each letter with a specific number and padded the numbers out with zeros so that each letter-number is unique. For example, we could turn the word “Reddit” into “082101100100105116” using the ANSI character set as our letter-number mapping. The key thing this lets us do is turn the rules for constructing valid strings of letters & symbols into mathematical operations. For example, a simple (and often incorrect) rule for pluralizing words with the mapping defined above would be times the number by 1000 and add 115 (the ansi value for the character ‘s’).
Mathematicians have formal notations that they use for expressing sentences like “For all numbers a, there exist a number b, such that a + 1 = b” without any ambiguity. These notations are designed so that there is a basic set of known facts, referred to as axioms, and set of rules of inference that can be used to transform a sentence that is known to be true into another sentence that is also true. Within these notations, a proof is a sequence of sentences that connects the fact you want to prove is true back to one or more of the axioms through the rules of inference. As it turns out, doing this is actually pretty hard, especially when you want to prove that the something is false.
What Godel did was to figure out that by turning these sentences into numbers and the rules into mathematical operators, you could use the techniques from a field of math called number theory to discover and prove things in general about the sentences. However, since number theory is also expressible as a formal system, you can do the same for it, leading to sentences like “The number Y is a true in formal system X” being able to be expressed as numbers and reasoned about using number theory.
By doing things like this, Godel discovered some problematic stuff: All formal systems are incomplete. There exist structurally valid sentences in every formal system for which neither itself, or it’s negation can be proven to be true. Consider the sentence: “Yields falsehood when preceded by itself” yields falsehood when preceded by itself. Is it true or false? If the sentence is true, what it asserts is that it is false, and if it is false, what it asserts is true. Godel was able to create a version of this sentence into valid string in the formal system used by number theory, and then prove that it’s paradoxical. He was then able to use the rules of number theory to show that all formal logical systems either can’t express recursive statements, or they will have sentences that can’t be proven true or false.
Latest Answers