Talk:Kripke semantics

From Wikipedia, the free encyclopedia

Contents 1 Priority 2 Major changes 3 Kripke-Joyal semantics 4 Axiom names 5 First paragraph

[edit] Priority

Issues:

Should we call this Kripke semantics at all, since Kripke was not the first to discover them: both Hintikka and Kanger gave semantics of this form before Kripke. One sees the usage "Frame semantics" in the literature; how about we move the article to "Frame semantics", and let Kripke semantics be a redirect to it.

It is called Kripke semantics by mathematicians, logicians, computer scientists, and philosophers, even though it is known by many than Hintikka came up with the idea earlier. So it's best to keep the name but cite references to earlier literature. —the preceding comment is by 62.30.147.160 - 12:30, 24 July 2006 (UTC): Please sign your posts!

There are lots of @@To Do:...@@ tags strew about the article: I haven't time right now to delete them, but if they are not gone tomorrow I shall. ---- Charles Stewart 10:31, 23 Aug 2004 (UTC)

OK, I've changed the TODOs to source comments. As for the naming: I've never heard about Hintikka/Kanger giving Kripke semantics before Kripke, but it doesn't surprise me. It happens all the time in mathematics that important things get unnoticed and then rediscovered. This is not relevant to naming conventions; the article should be named "Kripke semantics" because that's the name most of the world uses. For example, the article on Zorn lemma is named "Zorn's lemma", even though Hausdorff and then Kuratowski discovered it independently before Zorn. Or consider "Ramanujan graphs": the name is simply an honor to a famous mathematician, it doesn't imply anything about authorship. Mathematical concepts (usu not theorems) are often named after people who didn't invent them.

In short: if Hintikka and Kanger found relational semantics independently, it might be worthwhile to mention it in the introductory paragraph. If what they found was just something vaguely similar to Kripke semantics, I'd advise either to not mention it at all, or to put it in a "history" subsection, which would also mention Beth semantics. In any case, the name of the article should stay. BTW, there is already a redirect "Relational semantics".

EJ 11:31, 23 Aug 2004 (UTC)

I agree with EJ about the name of the article. I think it's important to credit earlier discoverers where possible---I was the person who added the discussion of Kuratowski to the Zorn's Lemma page and created the Kuratowski-Zorn lemma redurect---but I don't think that should change the name of the article. There is an idea, called "Kripke Semantics", and whether that name is just or unjust the encyclopedia should treat the topic with that name. -- Dominus 13:35, 23 Aug 2004 (UTC)

Some references to the precedence of Kanger & Hintikka's work: Goldblatt has written a history (gzipped PS file), which discusses the precedence of rival claims to give the first relational semantics on pages 25 to 41. Hintikka's work defined a notion of model that is almost exactly the usual definition of maximal consistent set for modal logic, and applies it to deontic logic; Kripke acknowledges it as similar in his first work. Kanger's work has important technically differences, but the idea of an accessibility relation is there and he does note the correspondence between conditions on accessibility relations and axioms characterising modal systems (reflexivity <-> T axiom, transitivity <-> 4 axiom, symmetry <-> B axiom, and so on), which makes the work pretty sophisticated in my view. The Goldblatt article also names the work of Jonsson-Tarski as a possible predecessor, although they never applied their ideas to modal logic. Goldblatt also discusses work of Carnap, Bayart and Montague, the names maybe are worth mentioning, although they don't develop what I would call a Kripke-style model theory. ---- Charles Stewart 16:25, 24 Aug 2004 (UTC)

I almost forgt to say: OK about not changing the name, the above is just some notes before I figure out how best to incorporate them into the article. ---- Charles Stewart 16:59, 24 Aug 2004 (UTC)

Thank you for the link, it is quite interesting reading. -- EJ 10:48, 25 Aug 2004 (UTC)

[edit] Major changes

I've applied quite a major change, mostly a new section on History&Terminology, with a precis of the above work before Kripke, and a discussion of the rival terminology. I could have pointed out that the Blackburn et al book, now the standard ref. on modal logic, talks about relational semantics, but I didn't, as does Goldblatt, but I didn't. Possible world semantics is also widely used, perhaps as much as Kripke semantics, but it marks you as ignorant to use it: someone more diplomatic than me should put that in. And I added four references. ---- Charles Stewart 16:47, 25 Aug 2004 (UTC)

My understanding is that "possible world semantics" refers to the philosophical interpretation of intensional logics by possible worlds, rather than the formal relational semantics. -- EJ 14:56, 26 Aug 2004 (UTC)

[edit] Kripke-Joyal semantics

Another issue: where does Kripke-Joyal semantics belong? I originally moved it to the section on intuitionistic logic, as I vaguely remembered that topoi have something to do with int. log., rather than modal logic. After reading the Goldblatt paper I'm not so sure about it. It might be better to leave it as a top-level section after all. Can someone who actually understands sheaves confirm this? -- EJ 14:56, 26 Aug 2004 (UTC)

Perhaps it should be joined up with intuitionistic logic. Note that the Tarski-Jonsson topological semantics ofr intuitionistic logic predates Kripke/frame semantics, and is really closer in spirit to what is going on in sheaf semantics anyhow. (I'm not really on top of sheaves, but I have a rough idea about what is going on) ---- Charles Stewart 08:29, 16 Sep 2004 (UTC)

---

However: The Kripke-Joyal semantics is more general than applying just to intuitionistic logic since it may be employed in Boolean categories as well as Heyting categories (or, in fact, in categories which are neither).

Also, why is there no discussion of forcing here? Forcing, afterall, is really a special case of the Kripke-Joyal semantics.

[edit] Axiom names

Axiom names: I can find many many sources (in agreement) for most axioms in the table (such as K, 5, D, B, T, etc.) But so far I'm unable to locate sources for the axiom names "1", and "2". Does someone have an actual reference to these that they could point me at? Nahaj 15:13, 25 September 2005 (UTC)

No. The trouble is that unlike names of logics, there is no generally agreed standard for most modal axioms, different people use different names. I tried to use standard names where available, but the rest of the table is only a local definition for the purposes of Wikipedia (or rather, just this article: I'm unaware of any other Wikipedia article referring to these axioms), whence the warning above the table.

I chose the names "1", "2", and "3" for their simplicity, and didactical clarity: as the names of the other logics are loosely composed of names of their axioms, it is easily understandable for someone who sees the logics for the first time to denote the main axiom of S4.1 as "1". If you have a better idea, feel free to suggest it. -- EJ 12:48, 29 September 2005 (UTC)

Maybe .1, .2, .3 is better? .3 as the axiom characterising no right branching on transitive frames is pretty standard (see, eg. the Blackburn/de Rijke/Venema book), and I can't suppress the spurious association between axiom 1 and S1, etc. --- Charles Stewart 13:45, 29 September 2005 (UTC)

PS: Actually the .3 axiom I was thinking of is different, namely: <>p&<>q => <>(p&<>q) \/ <>(p&q) \/ <>(<>p&q). If I am not mistakened, the two variants give the same S4.3, but different K4.3s. --- Charles Stewart 14:11, 29 September 2005 (UTC)

For future reference, what is a good reference for this .3? Nahaj 00:54, 30 September 2005 (UTC)

Reference for what: the axiom or the name? Prior talks about these axioms (and a third) characterisation S4.3 in K1, K2 and related modal systems, which he attributes without reference to Lemmonn, Hintikka and Geach. If you are after the locus solum for the .3 notation, I don't have it, but it's used in the Blackburn/de Rijke/Venema book, p193. --- Charles Stewart 19:20, 30 September 2005 (UTC)

Both, and thanks, that's everything I was looking for. Nahaj 20:43, 30 September 2005 (UTC)

The axiom naming issue is a mess. But I'd personally prefer some historic name (with that flimsy justificaton of history) over giving it a new name. (Which is why I asked the question, I had hoped that you had such a reference for "1", that I might add to my list...) The Lemmon papers [1966] (distributed widely by hand and finally published as "An Introduction to Modal Logic" by E.J.Lemon in collaboration with Dana Scott [1977]) use "G" for your "2", and "M" (McKinsey) for your "1". I've seen *lots* of folk following Lemmon and using G for 2. Usage of "M" is more mixed, but seems to be very popular. I've been using "MS" for "1" on my pages (Although I appear to have not given my source on that name, I'll have to hunt down where I picked it up, If I can't find it I'll probably drop back to calling it M... The problem being that Chellas use M for something else, and is a very popular introductory text.) I don't seem to have the axiom referred to as "3" in any of my index, so I wasn't worried about it for now. And all the others have MANY sources using them by the names here. [Summary: I'd suggest "M" for "1", "G" for "2"] Nahaj 00:54, 30 September 2005 (UTC)

I was somewhat confused as to 1 being the "main axiom" for S4.1. Then I realized that this must be McKinsey's S4.1, and not Sobocinski's S4.1. McKinsey's 4.1 is generally (to my experience) called S4M nowadays (The "M" being your "1"). And Sobocinski's 4.1 seems to me the one more often meant when I've seen S4.1 in papers lately. I'll have to investigate. Nahaj 00:54, 30 September 2005 (UTC)

The Handbook of Philosophical Logic uses H for the variant .3 I gave (I guess H stands for Hintikka) --- Charles Stewart 19:20, 30 September 2005 (UTC)

Thank you. (For including the source) Nahaj 20:43, 30 September 2005 (UTC)

While I'm at it: CR (for Church-Rosser) is another widely used name for 2. I'd rather not use M for 1 since it is fairly often used instead of T for reflexivity: wouldn't McK work as well? I have the idea that I've seen that somewhere. --- Charles Stewart 21:28, 30 September 2005 (UTC)

I suspect almost anything would work here in the end ("1" and "2" have are serving the function). But I think it would be nice to use a "standard" notation that people would be likely to see else where, without having to scare them with the extent of the current naming mess. I don't remember seeing CR for 2, but that might be either my memory or my choice of reading material. (If you have a specific reference that would be nice.) Whatever it is called, if taken from the literature, is going to conflict with something else in the literature. CR does have two nice properties if you have a source... 1) There is a non-wikipedian tradition to quote, and 2) It doesn't seem to conflict with anything indexed in my catalog, which is usually a sign that it doesn't conflict with anything particularly common. Nahaj 22:08, 30 September 2005 (UTC)

I checked a few refs and discovered that while the axiom if fairly often described as capturing either the Church-Rosser property or confluence (see, eg. Blackburn/de Rijke/Venema p160), it is less often talked about as "axiom CR". The Handbook of Philosophical Logic calls the axiom allowing distribution of different modalities the Church-Rosser property and "axiom chr" for short: axiom 2 is a particular instance of this scheme (2nd edition, p189), and it is commonly used in dynamic logic to mean this (see eg. p13 of Schmidt&Tishkovsky, Multi-agent dynamic logics with informational test, which uses CR for the formula and chr for the frame condition). I didn't find any direct uses of CR to name 2, but I think they must have been in conference proceedings, which I don't have here. --- Charles Stewart 14:54, 3 October 2005 (UTC)

So, what shall we do with the article? The names so far mentioned in the discussion, plus Chagrov & Zakharyaschev's names (which did not appear here yet), give the following options:

• .1, M, MS, McK, ma
• .2, G, CR, chr, ga
• .3, H, sc

Apparently, none of these is simultaneously widely used, historic, and unambiguous, thus no choice will be completely satisfactory, and we must make a decision at some point. My order of preferences is currently:

1. "M", "G", "H" -- traditional, short and nice, but conflicting with other systems (renaming the "GL" axiom to "W" might be worthwhile in this case)
2. ".1", ".2", ".3" -- conflict-free, least effort, but rather nonstandard (save .3) and IMHO a bit ugly
3. "ma", "ga", "sc" -- conflict-free, standard to some degree, but nontraditional, and for consistency it would require to change also the other axioms to use the lower-case C&Z names

Opinions? -- EJ 02:42, 22 November 2005 (UTC)

I do not like the second choice. The first choice (MGH) is my first choice. G is commonly seen when people are building system names. Nahaj 02:50, 22 November 2005 (UTC)

Good. As Charles apparently does not object, I'll change the names to M, G, H now. -- EJ 18:25, 7 December 2005 (UTC)

Thank you. Nahaj 22:37, 8 December 2005 (UTC)

I would have voted for McK, CR and H, but I missed EJ's post and I won't rock the boat now. Just a question: since there are at least three distinct axioms that when added to S4 give S4.3, should we have different names for them? This article probably doesn't need them, but if we want to get into the nitty gritty of temporal logic, we might well want some extended discussion of the axiomatics of S4.3. --- Charles Stewart 22:53, 8 December 2005 (UTC)

I'm sorry that you missed the post, we can of course continue the discussion if you wish.

As for S4.3: obviously, the same name cannot be used for distinct axioms. (I concur that the other .3-like variants are not needed in this article - the point of the list here is not to give a comprehensive survey of modal axioms, but to give a few concrete examples for correspondence theory and subsequent topics, preferrably simple.)

So, if/when it becomes necessary to discuss these axioms on the temporal logic pages, the names will have to be distinguished somehow. I do not have a good idea how this should be done (being no expert on temporal logic, I've never seen a source which would need more than one .3 variant at the same time.) BTW, there is nothing special about S4.3 here: at least the axioms G, Grz, M also have variants in use which are equivalent over S4, but differ in a nonreflexive context. -- EJ 16:40, 12 December 2005 (UTC)

[edit] First paragraph

The phrase

is a formal semantics for modal logic systems, created in late 1950's and early 1960's by Saul Kripke

should be changed to

is a formal semantics created in late 1950's and early 1960's by Saul Kripke for modal logic systems

The reason is that it is a formal semantics for more than modal logics. For example, it is used with intuitionistic logic. —the preceding comment is by 62.30.147.160 - 12:32, 24 July 2006 (UTC): Please sign your posts!

Makes sense. And BTW, you can edit it yourself. -- EJ 18:11, 29 July 2006 (UTC)