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$ %%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].