# Löb's theorem and computer programs

The close relationship between logic and computability allows us to frame Löb’s theorem in terms of a computer program which is systematically looking for proofs of mathematical statements, `ProofSeeker(X)`

.

ProofSeeker can be something like this:

```
ProofSeeker(X):
n=1
while(True):
if Prv(X,n): return True
else n = n+1
```

Where `Prv(X,n)`

is true if \(n\) encodes a proof of \(X\)noteSee standard provability predicate for more info on how to talk about provablity.

Now we form a special sentence called a *reflection principle*, of the form \(L(X)\)= “*If ProofSeeker(X) halts, then X is true*”. (This requires a quine to construct.)

Reflection principles are intuitively true, since ProofSeeker clearly halts iff it finds a proof of \(X\), and if there is a proof of \(X\), then \(X\) must be true if we have chosen an appropriate logical system to search for proofs. For example, let’s say that `ProofSeeker`

is looking for proofs within Peano Arithmetic.

The question now becomes, what happens when we call `ProofSeeker`

on \(L(X)\)? Is \(PA\) capable of proving that the reflection principle for any given \(X\) is true, and therefore `ProofSeeker`

will eventually halt? Or will it run forever?

Several possibilities appear:

If \(PA\vdash X\), then certainly \(PA\vdash L(X)\), since if the consequent of \(L(X)\) is provable, then the whole sentence is provable.

If \(PA\vdash \neg X\), then we cannot assert that \(PA\vdash L(X)\), for that would imply asserting that \(PA\vdash\)“There is no proof of X”. This is tantamount to \(PA\) asserting the consistency of \(PA\), which is forbidden by Gödel’s second incompleteness theorem.

If \(X\) is undecidable in \(PA\), then if it were the case that \(PA\vdash L(X)\) it would be inconsistent that \(PA\vdash \neg X\) for the same reason as when \(X\) is disprovable, and thus \(PA\vdash X\), contradicting that it was undecidable.

**Löb’s theorem** is the assertion that \(PA\) proves the reflection principle for \(X\) only if \(PA\) proves \(X\).

Or conversely, Löb’s theorem states that if \(PA\not\vdash X\) then \(PA\not\vdash \square_{PA} X \rightarrow X\).

It can be proved in \(PA\) and stronger systems. It has a very strong link with Gödel’s second incompleteness theorem, and in fact they both are equivalent.

Parents:

- Löb's theorem
Löb’s theorem