Lo! A cartoon proof of Löb's Theorem!
Löb's Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent. Marcello and I wanted to be able to see the truth of Löb's Theorem at a glance, so we doodled it out in the form of a cartoon. (An inability to trust assertions made by a proof system isomorphic to yourself, may be an issue for self-modifying AIs.)
It was while learning mathematical logic that I first learned to rigorously distinguish between X, the truth of X, the quotation of X, a proof of X, and a proof that X's quotation was provable.
The cartoon guide follows as an embedded Scribd document after the jump, or you can download as a PDF file. Afterward I offer a medium-hard puzzle to test your skill at drawing logical distinctions.
Cartoon Guide to Löb's ... by on Scribd
Cartoon Guide to Löb's Theorem - Upload a Document to Scribd
And now for your medium-hard puzzle:
The Deduction Theorem (look it up) states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F) is a theorem in classical logic.
Let ◻Z stand for the proposition "Z is provable". Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.
Applying the Deduction Theorem to Löb's Theorem gives us, for all C:
((◻C)->C)->C
However, those familiar with the logic of material implication will realize that:
(X->Y)->Y
implies
(not X)->Y
Applied to the above, this yields (not ◻C)->C.
That is, all statements which lack proofs are true.
I cannot prove that 2 = 1.
Therefore 2 = 1.
Can you exactly pinpoint the flaw?
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."