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$~$%%note:See 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].