Löb’s Theorem: Santa Claus and Provability

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. \square

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. \square

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. \square

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. \square

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”

About these ads

1 Comment

Filed under Provability Logic

One response to “Löb’s Theorem: Santa Claus and Provability

  1. jaykovfoukzon

    Generalized Löb’s Theorem

    http://arxiv.org/abs/1301.5340

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s