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.
Trying the puzzle, before I read the other comments:
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.