Motivation

Löb's theorem is pretty counterintuitive. Speaking informally about one or more agents engaging in logically valid reasoning, the theorem says something like this:

"If it's believed that believing a particular prophesy would cause it to self-fulfill, then the prophecy will be believed."

Formally, the theorem just says $□ (□ C \to C) \to □ C$ , where $□ X$ means " $X$ is provable". This is most weird if X is a false statement, because it means you can't prove that you can't prove X (Gödel's theorem).

(Also: the box symbol above is not an unrendered symbol; it's supposed to be a box.)

Meta-motivation

I'd like to make Löb's theorem more intuitive for humans, because it shows how agents can sidestep the need to mentally simulate each other in games, by instead using reasoning/arguments that happen to self-fulfill in a good and defensible way. Basically, Löbian reflection helps agents to avoid metacognitive stack overflows when thinking about themselves and each other, and I want more human beings to understand how that can work, and sometimes already does work, in real world agents.

State of the art

The best attempt I've seen to make Löb's theorem more intuitive is Eliezer Yudkowsky's Cartoon Guide to Löb's Theorem, which is still quite confusing. The confusingness comes from thinking about a self-referential statement ( $Ψ$ on Wikipedia; S on Arbital) that's used to carry out the proof. The statement basically says "If this statement is provable, then C." Dealing with that sentence is pretty cumbersome, and requires a lot of fiddling around with nested statements and implications.

Doing better

I think we can make a new proof of Löb's theorem that doesn't use that weird self-referential sentence, by instead making the proof of Löb's theorem itself self-referential. Page 15 of the following paper poses an open problem on how to do this, which I think is possible to resolve affirmatively:

Cooperative and uncooperative institution designs: Surprises and problems in open-source game theory (Critch, Dennis, Russell, 2022)

Here's a screenshot from it:

If we can make a proof like that work, we could then use the following much shorter and simpler cartoon guide to explain it:

In other words, I want to write a proof of Löb's theorem that is structured much like a Quine. I'd like the details to (eventually) be rea...

Quines