Payor’s Lemma

Payor’s lemma is a theorem in mathematical logic that is similar to Löb’s theorem.

For the purposes of Agent Foundations, Payor’s lemma has been proposed as an alternative to Löb’s theorem, due to both being simpler and possibly having a probabilistic generalization in a way that breaks for Löb’s theorem. If it works out, this would provide a way for agents to do the probabilistic version of logical decision theory type stuff like cooperate in the Prisoner’s dilemma when given each other’s source code, this time with uncertainty.

The lemma is:

If then , where

(“turnstile”) means that the proof system proves the statement that follows, and (“box”) is the proof operator in the language itself. e.g. means that the proof system proves that it proves , like how I know that I know what 1+1 is.