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.”
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.”