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).
Latest Answers