Talk:Löb's theorem
From Wikipedia, the free encyclopedia
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:
- 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;
- 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.
