Epistemic status: too good to be true? Please check my math.

We've known for a while that Löb's theorem fails when proof is relaxed to probabilistic belief. This has pros and cons. On the pro side, it means there's no Löbian Obstacle to probabilistic self-trust. On the con side, it means that some Löb-derived insights for proof-based decision theory don't translate to probabilistic decision theory, at least not as directly as one might hope. In particular, it appeared to dash hopes for probabilistic generalizations of the "Löbian handshake" for cooperation.

Recently, Andrew Critch wrote about the Payor Lemma, which allows for a very similar "modal handshake" without Löb's Theorem. The lemma was proved using the same modal assumptions as Löb's, so on the surface it may appear to be just a different method to achieve similar results, whose main advantage is that it is much easier to prove (and therefore explain and understand) than Löb's Theorem.

But, a natural question arises: does Payor's Lemma have a suitable probabilistic version?

I'll give an affirmative proof; but I haven't confirmed that the assumptions are reasonable to my satisfaction.

Setup

Let $L$ be a language in first-order logic, expressive enough to represent its sentences $s \in L$ as quoted terms $┌ s ┐$ , eg, through Gödel numbering; and with a probability function symbol on these terms, $p (┌ s ┐)$ , which can be equated with (some representation of) rational numbers, e.g. $p (┌ ⊤ ┐) = 1$ , $p (┌ s ┐) = \frac{1}{2}$ , etc. I also assume the system can reason about these rational numbers in the basic ways you'd expect.

For all $a, b \in L$ and all $r \in Q$ , we have:

If $⊢ a$ , then $⊢ p (┌ a ┐) = 1$ .
If $⊢ a \to b$ , then $⊢ p (┌ a ┐) \leq p (┌ b ┐)$ .

(These assumptions might look pretty minimal, but they aren't going to be true for every theory of self-referential probability; more on this later.)

Let $B (s)$ abbreviate the sentence $p (┌ s ┐) > c$ for any $s$ and some globally fixed constant $c$ strictly between 0 and 1. This is our modal operator. (This modal operator is often called "p-belief" with the constant $c$ named $p$ instead, but I wanted to reserve $p$ for the probability operator.)

Some important properties of $B$ :

Necessitation. If $⊢ s$ , then $⊢ B (s)$ , for any $s$ .

Proof: Since $⊢ s$ implies $⊢ p (s) = 1$ , and $c \in (0, 1)$ , we have...