Audio note: this article contains 49 uses of latex notation, so the narration may be difficult to follow. There's a link to the original text in the episode description.

Löb's Theorem:

• If _vdash Box x to x_, then _vdash x_.
• Or, as one formula: _Box (Box x to x) to Box x_

Payor's Lemma:

• If _vdash Box (Box x to x) to x_, then _vdash x_.
• Or, as one formula: _Box big(Box (Box x to x) to xbig) to Box x_.

In the following discussion, I'll say "reality" to mean _x_, "belief" to mean _Box x_, "reliability" to mean _Box x to x_ (ie, belief is reliable when belief implies reality), and "trust" to mean _Box (Box x to x)_ (belief-in-reliability).

Löb says that if you have trust, you have belief.

Payor says that if you can prove that trust implies reality, then you have belief.

So, both results give conditions for belief. Indeed, both results give conditions equivalent to belief, since in both cases the inference can also be reversed:

• Bidirectional Löb: _vdash Box x to x iff vdash x_
• Bidirectional Payor: _vdash Box (Box x to x) to x iff vdash x_ 

Furthermore, both results relate reliability with [...]

---

First published:

Source:

---

Narrated by TYPE III AUDIO.