Gödel's Second Incompleteness Theorem, Proof Sketch

In order for math to prove its own correctness, it would have to be incorrect. This result is Gödel’s second incompleteness theorem, and in this video, we provide a sketch of the proof.

Created by: Cory Chang
Produced by: Vivian Liu
Script Editor: Justin Chen, Brandon Chen, Zachary Greenberg

—

Extra Resources:

[anthonyenglert]

more people need to watch videos from this channel....

[bartkl]

Blown away by how well you understand and explain it, as well as by the care put in the production and metaphors. Tough stuff but you made me get it! (I guess)

[MisterFanwank]

I think you oversimplified the end. It's not technically impossible to prove a math system is consistent, but you have to do that outside of the math system, just like you did when you showed the Smith program would loop forever and that it could not ever return that result.

That was one of the weird quirks of Godel's theorem. He had to prove his self-referential theorems were true statements in Russell's math system _and_ that they could not be proved by the system's axioms.

[ericjenkins]

What if you have two different math systems that can prove each other consistent, and they are complete in the ways that the other one is incomplete in? Would this mean that the math systems were inconsistent, (because it would define them as being in the same system, so therefore inconsistent because the overall system proved itself correct?), or would it result in two different systems that were both correct and can be used to complete math by using different systems?

[francomay]

wow. these 3 videos of gödel incompleteness theorem blew my mind. your explanations are marvelous. thank god i runned into this channel! thank you so much, its an amazing work!

[grencez]

Technically you should say "NONHALTING" instead of "LOOPS" to be clear that it captures aperiodic behavior (which smith(M) certainly has when enumerating proofs). Otherwise, great explanation!

[BelegaerTheGreat]

Undefined Behavior seems a nice mid-point between mathematical complexity and layman understandability. (Worse than Hamkins of course.) Here are the notes from the last 3 videos of his playlist, the only ones innovative to me. (Actually only the last 2 are such.)

Video nicely and quickly explaining what Gödel proved, but not HOW he proved it. There are dozens of other videos out there doing the same.


As explained in this video, it only proves Completeness VS Soundness, not Consistency. It is explained in his next video.

1:00 An example of an unsound but consistent system, is one that proves only one statement, and that statement is false. Obviously unsound, but neither does it lead to a contradiction.

2:55 Reducing Completeness to the Halting Problem.
Our program takes a code C and an input X, and goes down the list of all possible proofs, until it finds a proof that C(X) halts or a proof that C(X) never halts. One of the above two must be true, so the program would have to eventually halt. The amount of time it would take would be finite, but it could be any amount! However long we would wait for the answer, we would not be able to say how much time is left.
So while I cannot refute this proof, it is certainly sketchy.

3:40 This is where the video outdoes Hamkins. It explains clearly how our program going through all the proofs would fail, and how it directly corresponds to what Gödel proved. This is the best Turing-Gödel comparison I found on the internet.

5:00 The program on which our program could not decide whether it loops or halts, must actually loop, because if it halted, there would exist a proof of it, a proof that just runs the program and follows its every step to the point of halting.
Therefore there must exist a program that loops, but we cannot prove it. A beautiful parallel to the Gödel sentence, that is not bouncing like "heterological" or Russell's Paradox, but just is true while being unprovable. That difference bugged me, finally I see the perfect similarity of the 2 theorems.


To my surprise, this video goes around the hard math, and proves the "inability of proving Consistency" with Turing again! (Does not mean that I find that proof intuitive or certain.)

1:13 it starts here. We can prove that a system must be Inconsistent or Incomplete, by proving that the system's Consistency implies its Incompleteness. (Cons⇒Inco ≡ ¬Cons∨Inco)
To achieve this, we assume math is Consistent, and prove its Incompleteness from it. Create the program smith (Oh how much I hate those YouTubers giving nonsensical names to functions!):

function smith(M: program)
{
for each proof P
{
if (P proves M(M) loops) return;
if (P proves M(M) halts) loop();
}
}

(I have 2 comments here, firstly, if we changed M(M) to smith(M) it would be undecidable on EVERY input, which I guess is not what we want. Secondly, if we want this to be operable by a Turing Machine, we actually need to arithmetize the function being inputted, M(⸢M⸣).)

2:29 I will just call smith s. If s(s) would find a proof that it loops, then it would immediately halt. This would mean that there must exist a proof proving that it halts, the brute-force proof, that just runs the program until it finds a return; or a loop();. Since our system, by assumption, is Consistent, there cannot exist a proof s(s) loops because it would lead to a contradiction. The mirror situation happens if we find a proof that s(s) halts. Then it enters a loop, and brute-force confirms it.
The conclusion is that in a Consistent system there must exist neither of those proofs, and the system must be Incomplete. Cons⇒Inco

4:18 Since we have neither of those proofs, s(s) will actually loop forever over all the proofs, trying to find one. Does this count as a proof, and therefore makes s immediately halt? Not exactly.
In order to formulate the new proof, we need to have earlier proven ¬∃(proof of s(s) looping), and in order to have proven ¬∃(proof of s(s) looping) we needed to prove our system to be Consistent. Therefore, if we prove that our system is Consistent, it immediately entails its own inconsistency.

What I am confused about, is why does this mean "(Peano) system cannot prove its consistency" instead of "(Peano) system cannot be consistent".
Ok, I figured it may work like this: When we do not know whether or not our system is Considtent, and we run s(s) and do not see it stop, we do not know whether it will stop tomorrow (Inconsistent system), or never (Consistent system). Only if we were certain that it would never stop, would we be able to formulate the proof that it loops.
Only when we did somehow prove our system Consistent, would we know it loops without waiting an eternity, and would it implode, becoming Inconsistent.

The understanding that UndefBehavior proposed, is that the fact that our system is Consistent ⊢
¬∃(proof of s(s) looping) ⊢
s(s) loops (bc can't find proof) ⊢
our system is Inconsistent.
Therefore, we are not concerned with the truth of "our system is Consistent", only its proof! And if we can prove our system's Consistency, then we can infer its Inconsistency from it!
The only non-contradictory Consistent system is an Incomplete one, in which "our system is Consistent" is one of the true&unprovable statements. Whoosh, I finally understand this Turing's (and also more of Gödel's) Incompleteness!

[allnamesaregiven]

Great great great man!
Can you tell me how this explanation relates to the formal proof of gödels 2. incompleteness theorem?
Because to me its mostly wizardry involving Löbs Theorem.

[Kyanzes]

I could be wrong but since maths builds on axioms, wouldn't that mean that maths must remain incomplete and/or inconsistent by necessity? The axioms limit the abilities of a system that is built on them. In other words: some or all the axioms are incomplete and/or inconsystent. Perhaps certain pairings of axioms cause it.

[Croolsby]

I'm confused about smith(smith). The type definition of smith is "smith: (M: program) => halt | loop". So in order to even begin running smith, you need to pass in the argument, which is also smith. However, smith is a function which takes in a program, M. Without defining what M is, you haven't completly defined the input argument. So it's incorrect to say we are running smith(smith). What you mean to say is that we want to run It's clear to me that this program will loop. In fact, not only does it loop, it never even gets past constructing the memory needed to hold the input argument. It's forever allocating memory.

[benheidemann]

Great videos but... am I the only one who finds the oracle intensely irritating? xD

[codyheiner]

I've read a lot on Godel's incompleteness theorems, but what I love so much about what you do here is that you address those "but what if I try..." questions that naturally follow.

Something I'd be interested to see more clarity on is: where do these proofs fall apart for simpler math systems such as Euclidean geometry + parallel postulate, or arithmetic with addition but no multiplication?

[jamestagge]

i have been working through this for a while now and hope someone will comment on the following. i do think that this theorem makes no sense and rather than discovering a hole in logic/math, introduces one which is pure sophistry.
1. If we consider the statement of Goedel’s that “this statement is true but cannot be proved” it can only mean;
 That the statement “this statement is true but cannot be proved” is itself the statement of issue (self-referencing). So, “if” “this statement is true but cannot be proved” is true as per its own definition/claim then the why and how would have to be known and discernable or all this makes no sense. I might be in error but I think that Goedel presented this “this statement is true but cannot be proved” via his translation of some mathematical statements by his number system as the calculated consequence of some “hole” in mathematics and logic, not a word puzzle/paradox. It is supposed to be a structural phenomenon of mathematics/logic. This would mean that the mathematical statement from which it was translated claimed to be true, (before translation) but could not be determined as such by means of any reasons as to how or why. This is illogical.
• The problem is that the conclusion of his translation claims to be merely just that, a translation such that the mathematical statement from which the translation was the extension, had to be known to be true but also to have no proof before the translation was executed or it could not have been reflected in that translation and that makes no sense. Here we have the tail wagging the dog.
• The problem is that this mathematical statement which when translated claimed that it was true, would have to have had some reason to be considered true, some structural reason which again, would mean that in reflection of that structure, we would have the how and why it was true which would be the proof.

I am sorry but I do think that given the above, it is clear that this entire scheme is sophistry, i.e., that the logic is backward in the acceptance of this scheme. The logic by which his very propositions were defined is being denied in the manipulation of the components of the scheme that it might be asserted and accepted.

Can anyone review this one last post and let me know what you think? I just think that if there is math to prove this, it must be in error or the semantic analogy would make sense and it decidedly does not. Thanks.

[PedroM]

This channel should really be more popular. Please keep the excellent work, sir

[stevendaryl]

This is very nice. The trick that I had seen is this (using self-reference)

Let G be the sentence: "If there is a proof of G, then there is an earlier proof of not G"

(Earlier meaning that the code of the one proof comes before the code of the second proof, if we code proofs as natural numbers)

Then we can reason: Suppose there is a proof of G. Then we can check all earlier proofs to see if any of them is a proof of not G.
Case 1: There is an earlier proof of not G. Then we have proved a contradiction, since our system proves both G and not G.
Case 2: There is no earlier proof of not G. In that case, G can be seen to be false (since it claims that there is an earlier proof of not G). So we can prove that G is false. So we can prover not G. Again, we've proved a contradiction--we've proved G and we've also proved not G.

So if there is a proof of G, then our system is inconsistent.

Now, suppose there is a proof of not G. Then again we can reason as follows:
Case 1: There is an earlier proof of G. Then our system is inconsistent, since it proves both not G and G.
Case 2: There is no earlier proof of G. Then what G says is true (since it says there is no proof of G earlier than the shortest proof of not G). So we can prove G. Again, our system proves both G and not G.

It took me a while to see it, but your construction has the same property. Let G for your construction be the statement "Program P will never halt". Then it is the case that

G is true <-> if there is a proof of G, then there is a shorter proof of not G.

[HavidVideos]

Now what I want to know... If it's inconsistent, unicorns exist? Whatever we want can be proven? We can't proof anything we want, so it has to be consistent. It must be incomplete.

[ROMANVS_STERCIPONITOR]

This math system proves Gödel's theorem (M→G)

Gödel's theorem proves that a math system cannot prove its own consistency (G→-Pc)

(1) Therefore, M→-Pc

Gödel's theorem also proved that a math system that can prove its own consistency is not consistent (G→(Pc→-C))

(2) Therefore, M→(Pc→-C)

But if Pc→-C and M→-Pc, this means M→-Pc→-(-C)

Which means M→C

Which means this math system proves it's own consistency

Therefore, either this math system is inconsistent or Gödel's theorem has a fallacy

[blazingkin]

These are great videos! Always a pleasure to see a new one in my sub box.

[anthonym]

What is the most fundamental metric?

It must exist apart from any other metric (it is sufficient when compared against no other metric)

It must be be the fundamental part, that supports all other metrics.

What is the fundamental metric?

If it exists, then why does it exist?

[nooneatall]

this channel is gold, you are awesome.