Löb’s theorem

Sometimes written “Loeb’s Theorem” (because umlauts are tricky). This is a theorem about proofs of what is provable and how they interact with what is actually provable in ways that surprise some people.

Löb’s theorem states that, given any statement P, if Peano Arithmetic (PA for short) proves that it can be ‘trusted’ if it proves P (that is, Prove(P) implies P), then it actually just proves P. This means that PA cannot tell you that it can be trusted about P, unless it also just tells you P. It also holds for theories that contain PA.

As a consequence, whenever we try to prove a statement P, we can go ahead and just assume that P is provable, and then see if we can show that that implies that P is true. This might sound really stupid and contradictory at first glance—the important thing is to be really clear about what is proving what. In the condition, PA is saying that if it proves P, then P is true. In ‘our’ view (that is, in a metatheory), we see that if PA says that, then PA will also say that P is true.

This math result often comes up when attempting to formalize “an agent” or “a value system” as somehow related to “a set of axioms”.

Often, when making such mental motions, one wants to take multi-agent interactions seriously, and make the game-theoretically provably endorsable actions “towards an axiom system” be somehow contingent on what that other axiom system might or might not be able to game-theoretically provably endorse.

You end up with proofs about proofs about proofs… and then, without care, the formal proof systems themselves might explode or might give agentically incoherent results on certain test cases.

Sometimes, in this research context, the phrase “loebstacle” or “Löbstacle” comes up. This was an area of major focus (and a common study guide pre-requisite) for MIRI from maybe 2011 to 2016?

It became much less important later after the invention/​discovery of the Garrabrant Inductor. There is also work on using the similar Payor’s Lemma, which possibly allows for a probabilistic version in a way that break’s for Löb’s theorem.

As to the math of Löb’s theorem itself...

We trust Peano Arithmetic to correctly capture certain features of the standard model of arithmetic. Furthermore, we know that Peano Arithmetic is expressive enough to talk about itself in meaningful ways. So it would certainly be great if Peano Arithmetic asserted what now is an intuition: that everything it proves is certainly true.

In formal notation, let stand for the standard provability predicate of . Then, is true if and only if there is a proof from the axioms and rules of inference of of . Then what we would like to say is that for every sentence .

But alas, suffers from a problem of self-trust.

Löb’s theorem states that if then . This immediately implies that if is consistent, the sentences are not provable when is false, even though according to our intuitive understanding of the standard model every sentence of this form must be true.

Thus, is incomplete, and fails to prove a particular set of sentences that would increase massively our confidence in it.

Notice that Gödel’s second incompleteness theorem follows immediately from Löb’s theorem, as if is consistent, then by Löb’s , which by the propositional calculus implies .

It is worth remarking that Löb’s theorem does not only apply to the standard provability predicate, but to every predicate satisfying the Hilbert-Bernais derivability conditions.