Talk:Löb's theorem

From Wikipedia, the free encyclopedia

	Philosophy Portal This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details.
???	This article has not yet received a rating on the quality scale.
High	This article has been rated as high-importance on the importance scale.
Additional information: Related task forces (core areas): Logic

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)

[edit] 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.

[edit] 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.

[edit] 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)