Consider the following argument for the existence of Santa Claus (which is called Curry’s paradox):

Let *S* be the sentence

If *S* is true, then Santa Claus exists.

*Lemma*: *S *is true.

*Proof.* *S* is of the form “If *P*, then *Q*.” so to show *S* we just have to assume *P* and show *Q.* So, assume that *S* is true (with the goal of showing that Santa Claus exists). Since we’ve assumed that *S* is true, it follows that if *S *is true, then Santa Claus exists (since that’s exactly what *S* says). Then, since *S* is true, Santa Claus exists.

*Corollary*: Santa Claus exists.

*Proof.* Since *S* is true, it is the case that if *S* is true, then Santa Claus exists (since that’s exactly what *S* says). Therefore, since* S *is true, Santa Claus exists.

Since Santa Claus doesn’t exist, this argument seems to just prove that informal reasoning combined with self-reference can often lead you astray. Can we extract any interesting theorems out of this argument? It turns out that we can.

Let PA denote Peano Arithmetic, which is a first-order theory of arithmetic. In the course of proving his incompleteness theorems, Gödel found a way to represent way PA-provability in PA. For every sentence *A*, there is a sentence Prov(*A*) such that PA proves *A* iff PA proves Prov(*A*). It has the following two further properties:

1. For all *A* and *B*, PA proves that Prov(*A*→B) together with Prov(*A*) implies Prov(*B*).

2. For all *A*, PA proves that Prov(*A*) implies Prov(Prov(*A*)).

Furthermore, Gödel was able to prove his diagonalization lemma, which implies that you can use self-reference as long as it is in reference to provability. That is, you can formulate the sentence “This sentence is not provable” (i.e., there is an *S* such that PA proves *S* ↔ ~Prov(*S*)) but you cannot formulate the sentence “This sentence is not true” (i.e., there is no *S* such that PA proves *S * ↔ ~*S*).

Now let’s try to redo the above argument that Santa Claus exists in the context of PA-provability.

Let *A* be the assertion that Santa Claus exists. As above, let *S* assert “If *S* is provable, then *A* is true.” In other words, we use Gödel diagonalization to find an *S* such that PA proves *S* ↔ (Prov(*S*) → *A*).

In proving the following lemma, it turns out that we need an extra assumption, which I’ve put in italics.

*Lemma*: *S *is provable in PA.

*Proof*. We’ll work within PA. Assume Prov(*S*). Then, by property 1 above, we have Prov(Prov(*S*) → *A*), and it again follows from property 1 that Prov(Prov(S)) implies Prov(*A*). Then, *if we knew that *Prov(*A*) *implied A*, we would conclude that *A *is true and thus that *S* is.

*Corollary*: *A *is provable in PA.

*Proof.* We’ll work within PA. Since we know *S* from above, we know that Prov(*S*) → *A. *However, we also know from the above that Prov(*S*) holds. Therefore, *A* holds.

So, we have proved that *A* is provable in PA given that PA shows that Prov(*A*) implies *A* (we used this assumption in the proof of the above Lemma). This is Löb’s theorem.

Löb’s Theorem: For any sentence *A*, if PA proves Prov(*A*) implies *A*, then PA proves *A*.

We can use to answer the following natural question: Gödel proved his incompleteness theorem by finding a *G* such that PA proves *G *↔ ~Prov(*G*). (*G* essentially says “*G* is not provable in PA.”) It follows that, given that PA only proves true things, *G* must be true and unprovable. But what about the sentence *H* which says “*H* is provable in PA.” ? Is it true and provable or false and unprovable?

Löb’s Theorem provides the answer. Since, by definition, PA proves Prov(*H*) → *H*, it turns out that *H* is both true and provable.

For more information, see the Stanford Encyclopedia of Philosophy’s entry on provability logic and George Boolos’s book “The Logic of Provability”

Generalized Löb’s Theorem

http://arxiv.org/abs/1301.5340