Talk:Löb's theorem

Can someone add an example? --Michalchik (talk) 09:43, 8 April 2009 (UTC)

Just a point about referring to this page: "Loeb's theorem" is a better ASCII rendering of "Löb's theorem" than the often seen "Lob's theorem": the latter will cause readers familiar with German orthography to wince, and you woulnd't want that, now, would you? I've created the referring page.

Oh, and a question, what do people know about Martin Loeb? The only things I know are what I heard about him in the colloquium held in honour of Robin Gandy: that he was a friend of Gandy, and taught mathematics and philosophy at Leeds University in the 1950s with Gandy. ---- Charles Stewart 10:16, 19 Aug 2004 (UTC)

Sad to say, Martin Loeb died a couple of months ago. I have just done an article based on obituaries. Robin Gandy is mentioned in the obits, but I left him out as I was not sure how important he was. -- 15:40, 3 October 2006 (UTC)

Notes on 5-oct-2004 changes

Forgot to add notes:

• I put provability logic in a section; I don't think it should appear before theorem
• GL has the 4 axiom []phi -> [][]phi
• Statement of Loeb's axiom too strong: original theorem held for systems of arithmetic where inudction was restricted to Sigma-0-1 sentences (ie. equivalent ability to prove functions total as PRA). Don't know what this system is called, when I find out I will change. ---- Charles Stewart 16:58, 5 Oct 2004 (UTC)

You may call modal provability logic KW, GL, or K4W, but the 4 is redundant since it is derivable in KW. Hence I omitted it.

I didn't know that. It makes sense to say that the logic is K+(GL) and observe that (4) is a derivable consequence.

You've incorrectly stated Lob's theorem by forgetting the modal operator on the consequent. It should be []([]P-->P)-->[]P, not []([]P-->P)-->P. Likewise, the inference rule infers the provability of P, not just P.

Right.

And it might be helpful to note that if the inference rule is used, the schema is not needed. But modal logics are more easily characterized by frame properties and schemata than inference rules. It is easier to just say that such theories are closed under MP and necessitation and have such and such schemata.

K is uniquely easy to characterise by both axiomatic and semantic means. IIRC, (GL) has a natural frame characterisation, which we should mention here. ---- Charles Stewart 06:04, 6 Oct 2004 (UTC)

The properties of the frame for KW is convere well-foundedness (and the finite-model property), transitivity (per the Hilbert-Bernays-Lob provability conditions) and irreflexivity (as reflexivity would allow the derivation of []P-->P, which would be a truth predicate - proved not to be derivable by Tarski's indefinability of arithmetical truth theorem). Those are the major properties, and then there are others following by entailment.

Dividing up content between here and provability logic

Most of the content I know of appropriate either for this article or for provability logic could go in either:

1. The case for putting the overlap in provability logic is that that article is most easy to situate within the wider context of modal logic, so the content is eaasier to fit in context;
2. On the other hand this overlap is a nice entry point into provability logic for the majority of logic students who are more familiar with the formalisation of consistency proofs than they are with modal logic.

I'm undecided, but I lean towards giving a reasonable short introduction on this page, and a full treatment on the provability logic page. ---- Charles Stewart 06:38, 6 Oct 2004 (UTC)

I'm not sure exactly what you're saying here. I think an overlap is fine but perhaps redundant provided there is proper linking to the provability logic page. Though the overlap might be, as you said, helpful for those unfamiliar with modal logic.

The questions are (i) where should the main body of information appear, and (ii) how much overlap gives the best reader experience ---- Charles Stewart 11:39, 6 Oct 2004 (UTC)

The more overlap, the more self-contained the section is. If the page is divided up with a TOC, redundancy wouldn't be so much a problem.

Removed wrong text

I have removed the following text:

"This theorem is problematic for a number of reasons, and for this reason, has been referred to by Barwise & Etchemendy as "Löb's paradox." For example, consider the statement: "Santa Claus exists." If it is necessarily true that Santa Claus exists, it seems that we ought to infer that Santa Claus does, in fact, exist---indeed, that this inference must be drawn necessarily. But by Löb's theorem, this implies that Santa Claus necessarily exists, from which we infer that Santa Claus exists! Any statement could be exchanged for "Santa Claus exists," and so a paradox results."

There is misunderstanding of what Lob's theorem proves by the author who inserted this erroneous discussion. Lob's theorem states that if T proves ""exists proof of A in T" -> A" then T proves A. There is no link to necessary existence, where Lob's theorem is hardly to be applied. Indeed Lob's theorem is valid only in theories T that can express the concept of "provability" at first place, otherwise it is not clear how you can formulate the Lob's theorem at first place. Danko Georgiev MD 06:11, 25 June 2007 (UTC)

Löb's theorem as a corollary of Gödel's second incompleteness theorem

Can't we argue in the following way:

Assume $T\vdash ((T\vdash \varphi )\Rightarrow \varphi )$. Then $T+\neg \varphi \vdash \neg (T\vdash \varphi )$.

But $T\vdash \varphi$ iff $T\vdash (\neg \varphi \Rightarrow \varphi )$ iff $(T+\neg \varphi )\vdash \varphi$, and moreover these equivalences are provable in T. Therefore $T+\neg \varphi \vdash \neg ((T+\neg \varphi )\vdash \varphi )$.

Therefore $T+\neg \varphi$ proves its own consistency, so by Gödel's second theorem $T+\neg \varphi$ is inconsistent. Therefore $T\vdash \varphi$.

(One can deduce Gödel's second theorem from Löb's theorem even more easily: If $T\vdash \neg (T\vdash \bot )$ then $T\vdash ((T\vdash \bot )\Rightarrow \bot )$. Then by Löb's theorem, $T\vdash \bot$.)

I believe this is essentially Kripke's proof of Löb's theorem. In the introduction to his book _The Logic of Provability_, Boolos writes "Around 1966, Kripke realized that Löb's theorem is a direct consequence of Gödel's second incompleteness theorem for single-sentence extensions of PA." Then he quickly runs through a proof that I think is essentially this one (though I found this one easier to understand!). John Baez (talk) 05:27, 16 December 2013 (UTC)

I don't get it.

"If there is a proof of the Goldbach conjecture, then the Goldbach conjecture is true" - I can accept that. As a consequence of Löb's theorem, "Goldbach conjecture is true"?? --88.153.45.144 (talk) 19:19, 8 April 2013 (UTC)

"I can accept that." You can accept, but can you describe this acception in PA? --Davidsusu (talk) 22:27, 18 June 2021 (UTC)

"If there is a proof of the Goldbach conjecture, then the Goldbach conjecture is true" - if you have a *proof* of this statement, please share (then Löb's theorem would apply). 2620:0:102F:1100:D267:E5FF:FEF3:E5E6 (talk) 15:56, 6 May 2013 (UTC)

Alternate formulation

The theorem effectively says: "If statement P cannot be proven, then (within the same theory) it cannot be proven that the statement P cannot be proven" (i.e. it can't be proven that there doesn't exist a natural number N that encodes a proof of statement P). (Taking P to be a contradiction, e.g. x!=x, we get Gödel's result that a consistent theory can't prove its own consistency.) - Mike Rosoft (talk) 20:22, 19 January 2016 (UTC)

• And even further: if a theory is consistent, then there doesn't exist any statement that can be proven not to be provable. (Once again, this is the above-mentioned Gödel's result.) - Mike Rosoft (talk) 20:11, 21 January 2016 (UTC)

More consistent notation of the formula

In the formula, '$\vdash$' and 'Prov()', and also '$\to$' and 'if-then' ('${\dfrac {A}{B}}$') are mixed. Also, is the two variant necessary? --Davidsusu (talk) 00:34, 19 June 2021 (UTC)

The string of "and"s make it hard to tell which symbols you consider mixing. Only the if-then and ${\dfrac {A}{B}}$ are equivalent. I think the second is formula is slightly preferable since I think the use of if-then is often taken as $\rightarrow$, which it should not be in this case. AquitaneHungerForce (talk) 09:01, 19 June 2021 (UTC)