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

Read this document on Scribd: Cartoon Guide to Löb's Theorem

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?