Löb’s Lemma: an easier approach to Löb’s Theorem

[Andrew_Critch]

Related to: Löb’s Theorem for implicit reasoning in natural language: Löbian party invitations

tl;dr: Löb’s Theorem is much easier to grok if you separate the parts of the proof that use the assumption $\square p\to p$ from the parts that don’t. The parts that don’t use $\square p\to p$ can be extracted as a stand-alone result, which I hereby dub “Löb’s Lemma”.

Here’s how it works.

Key properties of $⊢$ and $\square$

Here is some standard notation. In short, $⊢$ is our symbol for talking about what PA can prove, and $\square$ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.

• “$⊢$ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “$⊢$” applies to the whole line that follows it. Also, $⊢$ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.

• “$\square \left(\text{1+1=2}\right)$” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”$⊢$ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.

• ″$\square X$ ” is short for “$\square \left(X\right)$” in cases where “$X$” is just a single character of text.

• “$X⊢Y$” means “PA, along with X as an additional axiom/​assumption, can prove Y”. In this post we don’t have any analogous notation for $\square$.

The proofs here will use the following standard properties of $⊢$ and $\square$ (source: Wikipedia), which respectively stand for provability and provability encoded within arithmetic.

1. (necessitation) From $⊢A$, conclude $⊢\square A$. Informally, this says that if A can be proven, then it can be proven that it can be proven (by just writing out and checking the proof within arithmetic). Note that from $X⊢A$ we cannot conclude $X⊢\square A$, because $\square$ still means “PA can prove”, and not “PA+X can prove”.

2. (internal necessitation) $⊢\square A\to \square \square A$ . If A is provable, then it is provable that it is provable (basically the same as the previous point).

3. (box distributivity) $⊢\square (A\to B)\to (\square A\to \square B)$. This rule allows one to apply modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.

4. (deduction theorem) From $A⊢B$, conclude $⊢A\to B$: if assuming $A$ is enough to prove $B$, then it’s possible to prove under no assumptions that $A\to B$.

Point 4 is helpful and pretty intuitive, but for whatever reason isn’t used in the main Wikipedia article on Löb’s Theorem.

Löb’s Lemma

Claim: Assume $\Psi$ and $p$ are any statements satisfying $⊢\Psi \leftrightarrow \square \Psi \to p$. Then $⊢\square \Psi \leftrightarrow \square p$.

Intuition: By assumption, the sentence $\Psi$ is equivalent to saying “If this sentence is provable, then $p$”. Intuitively, $\Psi$ has very little content, except for the $p$ part at the end, so it makes sense that $\square \Psi$ boils down to nothing more than $\square p$ in terms of logical equivalence.

Reminder: this does not use the assumption $\square p\to p$ from Löb’s Theorem at all.

Proof:

Let’s do the forward implication first:

1. $\square \Psi ⊢\square \square \Psi$ by internal necessitation ($\square \Psi \to \square \square \Psi$).

2. $\square \Psi ⊢\square (\square \Psi \to p)$ using box distributivity on the assumption,
   with $A=\Psi$ and $B=\square \Psi \to p$.

3. $\square \Psi ⊢\square p$ from 1 and 2 by box distributivity.

4. $⊢\square \Psi \to \square p$ from 3 by the deduction theorem.

Now for the backwards implication, which isn’t needed for Löb’s Theorem, but is handy anyway:

1. $⊢p\to (\square \Psi \to p)$ is a tautology.

2. $⊢\square p\to \square (\square \Psi \to p)$ by box distributivity on 1.

3. $⊢\square \Psi \leftrightarrow \square (\square \Psi \to p)$ by box distributivity on the assumption.

4. $⊢\square p\to \square \Psi$ by 2 and 3.

I like this result because both directions of the proof are fairly short, it doesn’t use the assumption $\square p\to p$ at all, and the conclusion itself is also fairly intuitive. The statement $\Psi$ just turns out to have no content except for $p$ itself, from the perspective of writing proofs.

Löb’s Theorem, now in just 6 lines

If you can remember Löb’s Lemma, you can write a very straightforward proof of Löb’s Theorem in just 6 lines:

Claim: If $p$ is any sentence such that $⊢\square p\to p$, then $⊢p$

Proof:

Let $\Psi$ be any sentence satisfying $⊢\Psi \leftrightarrow (\square \Psi \to p)$, which exists by the existence of modal fixed points (or by the Diagonal Lemma).

1. $⊢\square \Psi \to \square p$ by Löb’s Lemma.

2. $⊢\square p\to p$ by assumption.

3. $⊢\square \Psi \to p$ by 1 and 2 combined.

4. $⊢\Psi$ by 3 and the defining property of $\Psi$

5. $⊢\square \Psi$ by necessitation.

6. $⊢p$ by 3 and 5.

«mic drop»

[tristanhaze]

Why is it OK to use deduction theorem, though? In standard modal logics like K and S5 the deduction theorem doesn’t hold (otherwise you could assume P, use necessitation to get []P, and then use deduction theorem to get P → []P as a theorem).

[Andrew_Critch]

Well, the deduction theorem is a fact about PA (and, propositional logic), so it’s okay to use as long as $⊢$means “PA can prove”.

But you’re right that it doesn’t mix seamlessly with the (outer) necessitation rule. Necessitation is a property of “$⊢$”, but not generally a property of “$X⊢$”. When PA can prove something, it can prove that it can prove it. By contrast, if PA+X can prove Y, that does mean that PA can prove that PA+X can prove Y (because PA alone can work through proofs in a Gödel encoding), but it doesn’t mean that PA+X can prove that PA can prove Y. This can be seen by example, by setting $X=Y=\neg \square (1=0)$”.

As for the case where you want $⊢$ to refer to K or S5 instead of PA provability, those logics are still built on propositional logic, for which the deduction theorem does hold. So if you do the deduction only using propositional logic from theorems in $⊢$ along with an additional assumption X, then the deduction theorem applies. In particular, inner necessitation and box distributivity are both theorems of $⊢$ for every $A$ and $B$ you stick into them (rather than meta theorems about $⊢$, which is what necessitation is). So the application of the deduction theorem here is still valid.

Still, the deduction theorem isn’t safe to just use willy nilly along with the (outer) necessitation rule, so I’ve just added a caveat about that:

Note that from $X⊢A$ we cannot conclude $X⊢\square A$, because $\square$ still means “PA can prove”, and not “PA+X can prove”.

Thanks for calling this out.

[philh]

It might be worth being explicit that ⊢ has lower precedence than the other operators (which in some sense are part of a different language). I, like maybe Gurkenglas, spent some time wondering why $(⊢\square A)\to (\square \square A)$ wasn’t just a special case of necessitation.

I’m confused by your use of the deduction theorem. It’s only used in the forward implication argument, and seems unnecessary to me. (The linked wiki article doesn’t mention it.) More precisely, it only seems necessary to move things left-to-right across a turnstyle, because you’ve previously moved them right-to-left in a way that isn’t obviously-to-me valid.

(I mean, it’s obvious to me that if we can prove that A implies B, then assuming A lets us prove B. But it would also be obvious to me that if assuming A lets us prove B, we can prove that A implies B, yet you dedicated a theorem to allowing that. And I don’t trust things that are obvious to me to be actually “true”, let alone valid moves here.)

We can just make the whole argument without doing that and it seems fine to me? Looking at it in more depth:

(This does require that we can do logic with the things we’ve proved. E.g. if we have $⊢x$ and $⊢x\to y$, we can conclude $⊢y$. I think that’s okay, but seems worth being explicit about.)

1. $\square \Psi ⊢\square \square \Psi$ by internal necessitation ($\square \Psi \to \square \square \Psi$).

This is just doing the thing I question.

1. $\square \Psi ⊢\square (\square \Psi \to p)$ using box distributivity on the assumption, with $A=\Psi$ and $B=\square \Psi \to p$.

The assumption is $⊢\Psi \leftrightarrow (\square \Psi \to p)$, i.e. $⊢A\leftrightarrow B$. Weaken it and use necessitation to get $⊢\square (A\to B)$. Box distributivity is $⊢\square (A\to B)\to (\square A\to \square B)$. From those two, we can get $⊢\square A\to \square B$. Expanding again, this is $⊢\square \Psi \to \square (\square \Psi \to p)$.

1. $\square \Psi ⊢\square p$ from 1 and 2 by box distributivity.

Box distributivity lets us go from $⊢\square (\square \Psi \to p)$ to $⊢\square \square \Psi \to \square p$. So using 2, we have $⊢\square \Psi \to (\square \square \Psi \to \square p)$. And internal necessitation gives us $⊢\square \Psi \to \square \square \Psi$, so combining those, $⊢\square \Psi \to \square p$.

1. $⊢\square \Psi \to \square p$ from 3 by the deduction theorem.

No need for this, we already finished.

[Andrew_Critch]

It’s true that the deduction theorem is not needed, as in the Wikipedia proof. I just like using the deduction theorem because I find it intuitive (assume $A$, prove $B$, then drop the assumption and conclude $A\to B$) and it removes the need for lots of parentheses everywhere.

I’ll add a note about the meaning of $⊢$ so folks don’t need to look it up, thanks for the feedback!

[philh]

Thanks, that makes sense. And the added explanation helps a lot, I can see the argument for going from $⊢A\to B$ to $A⊢B$ now:

• PA proves $A\to B$;

• So PA + $A$ certainly proves $A\to B$, since it can prove everything PA can;

• Also, PA + $A$ proves $A$;

• So we have $A⊢A\wedge (\neg A\vee B)$;

• Which in turn gives us $A⊢B$.

[quetzal_rainbow]

Can you explain more formally what is the difference between $⊢$ and $\square$? I’ve looked in Wikipedia and in Cartoon Guide on Löb’s theorem, but still can’t get it.

[Andrew_Critch]

I’ve now fleshed out the notation section to elaborate on this a bit. Is it better now?

In short, $⊢$ is our symbol for talking about what PA can prove, and $\square$ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.

• “$⊢$ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “$⊢$” applies to the whole line that follows it. Also, $⊢$ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.

• “$\square \left(\text{1+1=2}\right)$” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”$⊢$ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.

• ″$\square X$ ” is short for “$\square \left(X\right)$” in cases where “$X$” is just a single character of text.

• “$X⊢Y$” means “PA, along with X as an additional axiom/​assumption, can prove Y”. In this post we don’t have any analogous notation for $\square$.

[quetzal_rainbow]

Thank you, it’s much more clear now.

[Algon]

A set of axioms $\Sigma$ within a vanilla first-order-logic language does not necessarily allow for the ability to speak about what statements are provable from $\Sigma$ within that language. Consider the axioms scheme $\forall x\forall y(x=y)$. There’s not enough strength in $\Sigma$ to create encodings of statements, which is neccesary to make formal statements in the language which could be interpreted in some standard model to mean “Statement X is provable”. Seriously, try doing it. It should clear things up the need to build in some notion of provability into the syntax and semtantics of a logic if you want to talk about provability within a language. Then read upto section 3 in this SEP article.

EDIT: That is assuming you know stuff about provability predicates already, and things like arithmetization. If you don’t, then the above exercise is way too hard. In that case, I’d just say that $\Sigma ⊢\psi$ and $\Sigma ⊢\square \left(\psi \right)$ represent “axioms $\Sigma$ proves statement $\psi$” and “axioms $\Sigma$ proves that $\psi$ is provable in some set of axioms T”. T is a “sufficiently strong” set of axioms, like Peano arithmetic, which can do interesting things.

[Gurkenglas]

It seems important to clarify the difference between From ⊢A, conclude ⊢□A and ⊢□A→□□A. I don’t feel like I get why we don’t just set conclude := → and ⊢:=□.

[Andrew_Critch]

Well, $A\to B$ is just short for $\neg A\vee B$, i.e., “(not A) or B”. By contrast, $A⊢B$ means that there exists a sequence of (very mechanical) applications of modus ponens, starting from the axioms of Peano Arithmetic (PA) with $A$ appended, ending in $B$. We tried hard to make the rules of $⊢$ so that it would agree with $\to$ in a lot of cases (i.e., we tried to design $⊢$ to make the deduction theorem true), but it took a lot of work in the design of Peano Arithmetic and can’t be taken for granted.

For instance, consider the statement $\neg \square (1=0)$. If you believe Peano Arithmetic is consistent, then you believe that $\neg \square (1=0)$, and therefore you also believe that $\square (1=0)\to (2=3)$. But PA cannot prove that $\neg \square (1=0)$ (by Gödel’s Theorem, or Löb’s theorem with $p=(1=0)$), so we don’t have $⊢\square (1=0)\to (2=3)$.

[philh]

To check, are you reading the second as $(⊢\square A)\to (\square \square A)$? It’s meant to be $⊢(\square A\to \square \square A)$.

[Gurkenglas]

Nah.

[Algon]

How would the semantics for that work out?

[Gurkenglas]

⊢ already is to □ as □ is to quoted □. If we redo the post one □ further in, we never need external necessitation. Not sure if that answers your question.

[deleted]

[Jason Gross]

I think this factoring hides the computational content of Löb’s theorem (or at least doesn’t make it obvious). Namely, that if you have $f:\square p\to p$, then Löb’s theorem is just the fixpoint of this function.

Here’s a one-line proof of Löb’s theorem, which is basically the same as the construction of the Y combinator (h/​t Neel Krishnaswami’s blogpost from 2016):

$$\text{löb}\left(f\right):=\text{let}\psi :=(\lambda \psi :\Psi .f(\psi \text{.fwd}(‘‘\psi ")\left)\text{in}\psi \text{.bak}\right(\psi )$$

where $‘‘\psi "$ is applying internal necessitation to $\psi$, and .fwd (.bak) is the forward (reps. backwards) direction of the point-surjection $\Psi \leftrightarrow (\square \Psi \to p)$.