Well, Löb's theorem is a straightforward generalization of the Second Gödel's theorem (the latter is Löb's theorem with S being falsehood). So, the line between the two theorems is rather thin...
I am asking about the simpler version of Löb's Theorem, not the Generalized Löb's Theorem. That is, if a system can derive "S is provable implies that S is true", then that system can derive S. I am looking for interesting applications in realms outside of Mathematics: for example, Gödel's Incompleteness Theorems have tremendous philosophical implications, but I do not see analogous applications for Löb. I found an anti-mechanistic argument in a paper "Löb’s Theorem as a Limitation on Mechanism" by Michael Detlefsen at http://www.public.iastate.edu/~dfade...against_ai.pdf, but the arguments appear either dubious when he is being precise and fuzzy in the rest of the paper. Any leads, links, or summaries of arguments would be appreciated.
Thanks for the comment, emakarov, and yes, one of the proofs (Kripke's) appeals to the Second Incompleteness Theorem (although whether this qualifies it as a generalization is debatable: it is an oversimplification to just put "0=1" in for S and get the Incompleteness Theorem). But the "fine line" is enough to obscure its applications. Try to think as a non-mathematician would do in looking at the theorems. (Not, however, with as much clumsiness as, say, Lucas or Penrose.) The incompleteness theorems lead themselves to immediate philosophical conclusions about the nature of truth. However, looking at Löb would seem to tell the philosopher little if he or she did not apply some mathematics to it to derive results (such as the second incompleteness theorem) of more evident applicability. Even if he did, he would then ask what one needed Löb for if one already had the incompleteness theorem: in other words, what new results does Löb give to the non-mathematician?
Thanks; yes, I know Curry's/Löb's Paradox, which is highly amusing, and does warn against injudicious use of comprehension or simply self-reference. At first glance, it has a similar form to Löb's Theorem of (A-->B)-->B, I don't really think that they are sufficiently related to take this paradox as an application of the theorem, so my question remains open. However, thanks for pointing it out.