Löb's Theorem:

If $⊢ □ x \to x$ , then $⊢ x$ .
Or, as one formula: $□ (□ x \to x) \to □ x$

Payor's Lemma:

If $⊢ □ (□ x \to x) \to x$ , then $⊢ x$ .
Or, as one formula: $□ (□ (□ x \to x) \to x) \to □ x$ .

In the following discussion, I'll say "reality" to mean $x$ , "belief" to mean $□ x$ , "reliability" to mean $□ x \to x$ (ie, belief is reliable when belief implies reality), and "trust" to mean $□ (□ 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: $⊢ □ x \to x ⟺ ⊢ x$
Bidirectional Payor: $⊢ □ (□ x \to x) \to x ⟺ ⊢ x$

Furthermore, both results relate reliability with belief, through the intermediary of trust.

Löb is usually thought of as a negative statement, that you can only have trust when you already have belief. One explanation of this is that Löb is the converse of the "trivial" case of trust, where you derive trust from simple belief: $□ x \to □ (□ x \to x)$ . (Recall that this is the pivotal step 2 in the proof of Payor's lemma.) Löb simply reverses this; combining the two, we know that trust is synonymous with belief: $□ x \leftrightarrow □ (□ x \to x)$ . "The only case where we can have trust is the trivial case: belief."

But this doesn't totally dash hopes of productive use of trust, as the negative reading of Löb might suggest. In the decision-theoretic application of Löb, we can take advantage of Löb to help ensure preferred outcomes:

For some desirable proposition $x$ , we can arrange things so that $□ x \to x$ (reliability), and provably so (trust). Applying Löb, we get $□ x$ (belief). But we already arranged for $□ x \to x$ ; so now we get $x$ out of the deal. This can allow cooperative handshakes between logic-based agents.

We can turn this into a general decision procedure by searching for the best $x$ we can make real in this way. More precisely, we search for possible implications of each action, and take the action for which we can find the most desirable implication. So we search for the relative provability of $x$ , in the context of an assumption that we take an action; and if we like what we see, we make that context real by taking that action.

Admittedly, this is a weird and spooky ...