Another try at understanding/explaining this, on an intuitive level.
Teacher: Look at Löb’s theorem and its mathematical proof. What do you see? Student: I don’t really follow all the logic. T: No. What do you see? S: … A containment vessel for a nuclear bomb. T: Yes. Why? S: Because uncontained self-reference destroys any formal system? T: Yes. How is this instance of self-reference contained? S: It resolves only one way. T: Explain how it resolves. S: If a formal system can prove its own soundness, then any answer it gives is sound. As its soundness has already been proven. T: Yes. S: However in this case, it has only proven its soundness if the answer is answer is true. So the answer is true, within the system. T: Yes. Can you explain this more formally? S: The self-referential recipe for proving the soundness of the systems’s own reasoning if the answer is true, necessarily contains the recipe for proving the answer is true, within the system.
Which isn’t quite the same thing as understanding the formal mathematical proof of Löb’s theorem, but I feel that (for now) with this explanation I understand the theorem intuitively.
Another try at understanding/explaining this, on an intuitive level.
Teacher: Look at Löb’s theorem and its mathematical proof. What do you see?
Student: I don’t really follow all the logic.
T: No. What do you see?
S: …
A containment vessel for a nuclear bomb.
T: Yes. Why?
S: Because uncontained self-reference destroys any formal system?
T: Yes.
How is this instance of self-reference contained?
S: It resolves only one way.
T: Explain how it resolves.
S: If a formal system can prove its own soundness, then any answer it gives is sound. As its soundness has already been proven.
T: Yes.
S: However in this case, it has only proven its soundness if the answer is answer is true. So the answer is true, within the system.
T: Yes. Can you explain this more formally?
S: The self-referential recipe for proving the soundness of the systems’s own reasoning if the answer is true, necessarily contains the recipe for proving the answer is true, within the system.
Which isn’t quite the same thing as understanding the formal mathematical proof of Löb’s theorem, but I feel that (for now) with this explanation I understand the theorem intuitively.