Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Joe2 comments on The Cartoon Guide to Löb's Theorem - Less Wrong

12 Post author: Eliezer_Yudkowsky 17 August 2008 08:35PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (92)

Sort By: Old

You are viewing a single comment's thread.

Comment author: Joe2 17 August 2008 10:42:35PM 1 point [-]

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