Talk:Provability logic

From Wikipedia, the free encyclopedia

Another case (in my opinion) of someone pointing out *A* particular thing as *THE* particular thing. I've made corrections where the natural assumption from the statement would be wrong. Nahaj 02:02:58, 2005-09-08 (UTC)

GL more or less is *THE* provability logic, especially in a short introductory article like this. All the other systems are just extensions or modifications of the same idea.

GL is *A* provability reference. And I think it important in a introductory article to make it clear that there isn't just ONE plausable logic. Nahaj 20:48:32, 2005-09-08 (UTC)

Added another reference.

I've removed it. First, it is almost irrelevant to the subject, and second, Hughes & Creswell is quite outdated, there are many better references on modal logic (which are listed on more appropriate places in Wikipedia).

I don't agree but I'm not going to get into an edit war over it. Nahaj 22:00:00, 2005-09-08 (UTC)

Question: The article says it is also called "L". Where is this? My page http://www.cc.utah.edu/~nahaj/logic/structures/systems/index.html documents (specific books, specific pages) the names "Prl" = Segerberg's "KW" = Boolos's "G" = "GL" = "K4W", but I seem to have somehow missed where it was also called"L". I'd appreciate a specific reference [book, page]. Nahaj 02:22:41, 2005-09-08 (UTC)

"GL" is by far the most common name of the logic. IIRC "L" was used in the Solovay's article, but I'm unable to verify it right now; in any case, it is used in the Japaridze-de Jongh survey in HPT, and several other papers. "G" is quite rare, I'm not sure where it came from, but Boolos uses GL. "K(4)W" is Segerberg's name, which predates provability logic as such; for this reason, it was historically used by modal logicians, but nowadays they mostly switched to GL. "Prl" is a generic name for provability logics, often used with some qualifiers as subscripts and/or in brackets; "PrL" is also used in Smorynski's book for GL, but this is quite idiosyncretic (Smorynski seems to be addicted to nonstandard notation, e.g. he writes BML for K4).

Your page is currently inaccessible. Linking it to K4W makes no sense; if there is some relevant info not covered by the usual references, I'll put the link to the References section when it becomes working again, but now it seems to me to be just self-promotion, sorry. -- EJ 12:56, 8 September 2005 (UTC)

G is from Boolos [As noted in [Hughes & Cresswell, 1996, p139]. Boolos [Boolos, 1993, p272(index entry)] uses K4W as the name. Nahaj 21:06:03, 2005-09-08 (UTC)

I do not understand the references (what does H & C have to do with Boolos?) and whether we agree on the meaning of the English word "use". Boolos (1993) is a monograph on provability logic, thus he refers to GL on every other page, and he uses the name "GL" throughout the whole book. At one place he also mentions alternative names for the logic as found in the literature, which is the reason why K4W appears in the index, but I fail to see how this counts as "Boolos uses ...". -- EJ 14:48, 9 September 2005 (UTC)

H&C document many of the names that other authors have used for systems. That's pretty much a necessity given the state of system names in the literature. Nahaj 16:00:03, 2005-09-09 (UTC)

G is from Boolos. I don't know what you have against H&C, but since you accept Boolos: G is from Boolos' "Unprovability of Consistancy: An Essay in Modal Logic" Cambridge University Press, 1979. And, if one gets far enough into Boolos' "Logic of Provability", the preface, page xi, covers his decision to stop using G for the system and start using GL.Nahaj 13:01, 17 September 2005 (UTC)

I see. You're right, I didn't realize that Boolos switched his notation.

I do not have anything against H&C, but against using it in this context. A proper reference to back up "XYZ is from Boolos" is Boolos, not H&C. -- EJ 15:38, 21 September 2005 (UTC)

(The system logs don't show any time the link was unavailiable. (The logs show requests around the clock). The monitor system runs every 15 minutes, and shows no times when it failed. (So, in fact, if it was inaccessible to you, I'd suspect it is on your end.) But in the interests of fairness, when did you try, and what error message did you get? [We have a cluster serving the pages, so it is actually rare for all of them to be down.] Nahaj 20:48:32, 2005-09-08 (UTC)

I tried it several times yesterday (2005-09-08) in the afternoon, about 12:00-15:00 UTC. I don't remember the error message exactly, but it was something along the lines of "Connection refused by www.cc.utah.edu". Maybe the server was just overloaded?

I don't see a problem at that time. And the load on all the machines answering to www.cc.utah.edu seems to have been low at the time. If you see this reappear, please leave a note on my talk pages. Nahaj 16:00:03, 2005-09-09 (UTC) The last 24 hours we've been fighting Denial of Service attacks on our webservers. Since they are coming from a limited number of eastern European IP addresses appropriate blocks should be in place soon.Nahaj 15:03:28, 2005-09-11 (UTC)

Anyway, it works now. I'm sorry for the accusation of self-promotion, now I see that the link was done in good faith. Nevertheless, there is almost zero information on your page on KW (GL), so I don't think it is useful to put it in references here. A few off-topic comments on your list:

I personally think (particularly since you insist on being insulting) that off topic items should have gone to my talk page. I don't know why you think them appropriate here. Nahaj 16:00:03, 2005-09-09 (UTC)

• The info on K4 is patent nonsense. It descibes S4.4.1.

I will check into this. What are your references for S4.4.1? And what did you use to decide that that S4.4.1 isn't yet another name for K4? (Modal logics do, after all, appear in the literature under many different names as they are rediscovered.) Nahaj 16:00:03, 2005-09-09 (UTC)

Disclaimer for Nahaj, and those "many" people who go to this page (although nobody cared about it enough to create it before this september) or who were directed here by a "search engine" (although the page is not even indexed by Google), and who are interested in this topic but cannot "put some work" into clicking the link below to see the end of the discussion: no modal logic named S4.4.1 exists, and there are currently no references for it except Nahaj's personal web pages. -- EJ 14:52, 27 September 2005 (UTC)

Update: Nahaj no longer lists S4.4.1 on his web page. -- EJ 14:07, 28 September 2005 (UTC)

• There is a lot of esoteric entries on the list (such as the crazy Pledger's naming), but many common and important systems seem to be missing. E.g., where is Grzegorczyk's logic? Dummet's logic? Bounded-width and similar systems (BW_n, BD_n, ...)? Also, there is an entry for the implicational fragment of intuitionistic logic, but not on intuitionistic logic itself (or other intermediate logics for that matter).

-- EJ 14:48, 9 September 2005 (UTC)

Personal attacks on Pledger seem uncalled for here. His papers are (to the best of my knowledge) the only complete analysis of systems derived from S3 by identifying modalities. (See, for example: "Modalities of systems containing S3""Zeitshrift fur Mathematische Logik and Grundlagen der Mathematik" Bd. 18, S. 267-283 (1972), "Some Extensions of S3" In the "Notre Dame Journal of Formal Logic, Vol XVI, # 2, April 1975, 271-272, and "Location of Some Modal Systems" by K. E. Pledger In the "Notre Dame Journal of Formal Logic, Vol 21, # 4, October 1980 pgs 683-684) He, at least, has a consistant coherent numbering for the systems. And given the number of systems with multiple names in the literature, and the number of names that have been reused to mean different systems in the literature, I think his numbering worth while. Nahaj 16:00:03, 2005-09-09 (UTC)

Attacks on my web pages also seem inappropriate here. The pages are incomplete, and they say so. (And some logics you list are not even modal logics) But for some issues (such as what names have been used for what modal systems), I'm unaware of any better reference on the net. The Standford Encylopedia of Philosophy's modal logic article even includes a pointer to my pages. Nahaj 16:00:03, 2005-09-09 (UTC)

Just to make things clear: what I wrote was not intended as a personal attack on Pledger (I didn't realize the wording is ambiguous, I of course didn't mean "crazy Pledger", but "crazy naming convention", which it is: inventing yet another naming from scratch is a not a good way to resolve the chaotic situation on naming of modal logics) or on you (the comments were meant to be helpful). I'll continue the discussion on your talk page. -- EJ 16:32, 9 September 2005 (UTC)

Summary of the discussion can be found on User talk:Nahaj#K4 systems (Resolution?). I appologize for calling John Halleck's page patent nonsense. -- EJ 15:11, 22 September 2005 (UTC)

Update: the discussion is now archived on User talk:Nahaj, sections "Modal Logic, et al. [Archived]" and "K4 systems (Resolution?) [Archived]". -- EJ 14:07, 28 September 2005 (UTC)

Now I found that a page on intuitionistic logic exists on your pages, but it does not appear to be listed on [1] under any of its usual names (Int, IPC, H). -- EJ 15:14, 9 September 2005 (UTC)

I'll correct the oversight on IPC. Int is a bit problematic, that's been on my todo list. Do you have a reference for it being called "H"? I've not seen it in the Modal Logic literature, but I might have missed it, or it may appear in some other piece of literature I've missed. Nahaj 16:00:03, 2005-09-09 (UTC)

[Comment on removal of link deleted] I'm sorry, I saw the removeal of a link and missed in being inserted further down. My appologies. Nahaj 22:19:23, 2005-09-08 (UTC)

OK, but please, do not delete text from the Talk page. It is much less confusing to write errata below the old text. -- EJ 14:48, 9 September 2005 (UTC)

You are correct. I'll take that advice. Nahaj 16:00:03, 2005-09-09 (UTC)