Trying the puzzle, before I read the other comments:
Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.
I think this is the flaw. Löb's Theorem shows that whenever we can prove ((◻C)->C) in PA, then we can prove C in PA. So instead of ((◻C)->C)->C, it would actually be ◻((◻C)->C)->◻C.
At first I looked at ◻((◻C)->C)->◻C and thought it had a similar problem — if we let C be the statement 2 = 1, then clearly C = false, so ◻((◻C)->false)->◻C; so ◻(true)->◻C; and presumably you can prove tautologies in PA, so (true) -> ◻C; therefore, PA contains a proof of 2 = 1. I think my mistake there was that I took ◻(X) as talking about the proposition X, like ◻ is just some function being passed a value that you can manipulate syntactically like any other expression; but I think that's wrong, it has to be treated as the literal quotation of X instead. ◻((◻C)->C)->◻C means "If PA proves 'if PA proves "1 = 2", then 1 = 2', then PA proves '1 = 2'"; you don't get to substitute your outside-the-system knowledge that 1 ≠ 2 into that, because the whole thing is about what PA says about "1 = 2", and about what PA might say about (1 = 2), but not about "1 = 2" or (1 = 2) themselves — except in that PA's claims about numbers have all been true so far, but to treat X and what-PA-says-about-X as logically interchangeable in this context would be begging the question.
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:
However, those familiar with the logic of material implication will realize that:
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?