The following puzzle is given in A Cartoon Guide to Lob's Theorem:

The Deduction Theorem 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.

[Edit per suggestion by @NicolinoWill]: There are two hidden boxes in the above statement. One goes in place of "we have," and the other in place of "we can prove." So the statement in full rigorousness is $$\square ((\square C)\rightarrow C) \rightarrow\square C.$$ This question is a great example to underscore the distinction between a statement made inside a system (object language) and statements humans make about such statements (metalanguage) since it is easy to conflate the two leading to perplexing and erroneous results.

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 have upvoted your Question because of its intrinsically interesting problem, but I feel that in immediately offering your self-answer you expose a weakness in how the Question is posed. In its current form this is a bare problem statement (although to your credit you have provided a source). If your intent was to get feedback about the way you solved it, then your resolution, at least in the sketchy form provided, should be included in the body of the Question, as the actual help wanted is hypothetically feedback about that solution. Commented Dec 21, 2022 at 4:55
• @hardmath Thanks for the feedback, this was my first attempt at the "answer your own question" format, so I will bear that in mind. Commented Dec 21, 2022 at 6:37

The resolution of the paradox is recognizing the omission of the provability predicate - $$\square$$ - in both the antecedent and the consequent. At that point it no longer fits the axiom schema $$[(X \rightarrow Y) \rightarrow Y] \rightarrow [\neg X \rightarrow Y]$$, so the deduction theorem is inapplicable. Please feel free to comment on my analysis and whether you agree.

• The paradox substitutes $\Box C$ for $X$ and $C$ for $Y$, which seems like a valid instance of the axiom schema.
– Nico
Commented Dec 21, 2022 at 6:02