The confusing part is this:
(C is provable → C) → C
I can grok the part inside the parenthases—that’s what we’d all like to believe; that this system can assure us that everything it proves is true. The weird step is that this statement itself implies that C is true—I guess we either take this on faith or read the Deduction Theorem.
What I find most strange, though, is the desire to have the proof system itself distinguish between provability and truth. Isn’t that impossible? A formal system only provides proofs given axioms; to it, the only meaning of truth beyond that of provability is the behavior of truth within formal logic operations, like implication and negation. “Truth” as “believability” only happens in the brains of the humans who read the proof later.
So, I disagree with the misleading paraphrasing of Lob’s proof: “Löb’s Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent.”
This dereferences the word “truth” wrongly as “soundness,” when truth’s meaning within the system is behavior in formal logic operations. The paraphrasing should be “Lob’s theorem shows that a consistent mathematical system cannot assert that theorems it proves will behave as true under the symbol manipulations of formal logic.”
Michael Rooney: I don’t think Eliezer is saying that it’s invalid to say “I don’t know.” He’s saying it’s invalid to have as your position “I should not have a position.”
The analogy of betting only means that every action you take will have consequences. For example, the decision not to try to assign a probability to the statement that Xinwei has a string in his pocket will have some butterfly effect. You have recognized this, and have also recognized that you don’t care, and have taken the position that it doesn’t matter. The key here is that, as you admit, you have taken a position.