Talk:Kripke semantics

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)

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)

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.

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)

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)

S5

I have changed the axioms in the list of S5. I was unsure what the list T,5 or D,B,4 meant, but if it means either the two axioms T,5 or the three eaxioms D,B,4 it was wrong. To see that T,5 is not transitive, try a frame with three nodes, u,v,w, where each has a reflexive edge and u and v have edges to each other and v and w have edges to each other, and let some A hold in u and v but not in w. Now T and 5 hold, but it is not transitive, as there is no edge from u to w (and axiom 4 does not hold). To see that D,B,4 is not reflexive look at a frame with two nodes and two edges, one in each direction and let some A hold in both. Dag Hovland 09:33, 18 September 2007 (UTC)

The equivalence of S5 with T+5 and D+B+4 is a quite standard fact, see e.g. SEP (NB they denote M what is denoted T here). "Deontic S5" is a name used for D+4+5, which is weaker than S5.

Your first frame does not satisfy 5: the point v sees u and w, but u does not see w, hence the relation is not Euclidean. More concretely, $v\Vdash \Diamond \neg A$, but $v\nVdash \Box \Diamond \neg A$ (as $u\nVdash \Diamond \neg A$). In general, every reflexive Euclidean relation is transitive: if xRy and yRz, then xRx by reflexivity, hence yRx by Euclideanness, hence xRz by more Euclideanness. A syntactic derivation of 4 in KT5 goes as follows:

1. $\Box A\to \Diamond \Box A\to \Box \Diamond \Box A$ by T and 5,
2. $\Diamond \Box A\to \Box A$ by 5,
3. $\Box \Diamond \Box A\to \Box \Box A$ by Nec and K from 1,
4. hence $\Box A\to \Box \Box A$ from 1 and 3.

Your second frame is not transitive (xRyRx, but not xRx, if you name the points in the obvious way). Indeed, let R be a serial symmetric transitive relation, and x any point. There exists y such that xRy by seriality, hence yRx by symmetry, hence xRx by transitivity, that is, R is reflexive. Alternatively, here is a syntactic derivation of T in KDB4:

$\Box A\to \Box \Box A\to \Diamond \Box A\to A,$

where the first implication is by 4, the second by D, and the third by B. -- EJ 12:26, 18 September 2007 (UTC)

5

Can please someone explain the axiom 5 on the following frame?

• 1 -> 2
• 1 -> 3
• 2 -> 3
• 3 -> 2

This is an euclidean frame (1R2 and 1R3 -> 2R3 and 3R2), right? Then the axiom 5 must hold. Now suppose that A holds only on 2. Then, on 1 holds $\Diamond A$, but $\Box \Diamond A$ doesn't hold. Where is the mistake? I cannot figure it out. I suppose the point is that this frame is not euclidean, but this means that there is something in the definition that I'm not able to catch... Thanks! -- Stefano 11:53, 7 June 2010 —Preceding unsigned comment added by 95.244.18.126 (talk)

This is not a Euclidean frame, as 1 → 2 and 1 → 2 would force 2 → 2. By the same token, 3 → 3 (and in general, the target of every arrow has to be reflexive). When you fix the frame like this, $\Box \Diamond A$ does indeed hold in 1.—Emil J. 11:26, 7 June 2010 (UTC)

Woa, thank you soooo much! -- Stefano —Preceding unsigned comment added by 95.244.18.126 (talk) 12:29, 7 June 2010 (UTC)

Possible world semantics

Is it really different than this? I know that Kripke semantics do not involve an ontological commitment to possible worlds: [1]. So, please explain what's the difference claimed in the lead here. Tijfo098 (talk) 17:19, 20 April 2011 (UTC)

I also note that despite the unsourced claims in this article that possible world semantics is deprecated (as a term), SEP uses it [2]. Tijfo098 (talk) 17:24, 20 April 2011 (UTC)

Perhaps a sourced explanation from Béziau p. 90 (2nd paragraph) [3] should replace the current unsourced claims. Tijfo098 (talk) 17:43, 20 April 2011 (UTC)

Dunn and H say pretty much the same thing, perhaps not as clearly [4]. Tijfo098 (talk) 18:21, 20 April 2011 (UTC)

Agreed. I was a bit taken aback to read that relational semantics was not possible-world semantics as I've been using the two interchangeably for decades. --Vaughan Pratt (talk) 20:36, 23 November 2012 (UTC)

hard to grasp

OK the only thing I can follow is $\Box p\leftrightarrow \lnot \Diamond \lnot p$ Can an analog of truth tables be made? In combinational logic you list the possible states of variables (for each variable either true or false) and the result of logic gates, but also => etc can be written this way... what are the modal values of the completely parsed statements? true/false?

necesary,possible?

or true and necessary, true and possible, false and necessary false and possible (4)

or 8: true, necessary, possible true, necessary, not possible, true, not necessary, possible, ... ?

Can these symbols be seen as logic gates with value tables?

Is there software that lets you compute on relatively short expressions? perhaps the easiest way to learn these things is by many examples... — Preceding unsigned comment added by 83.134.181.100 (talk) 02:10, 23 January 2012 (UTC)

Major Omissions

The definition of L-consistency:

"A set of formulas is L-consistent if no contradiction can be derived from them using the axioms of L, and Modus Ponens."

is incomplete. The article neglects to incorporate the necessitation rule. This makes the theory $\{p,\,\neg \Box p\}$ L-consistent (in the sense of the above definition) for any propositional variable p and logic L with no axioms (or only with axiom scheme K). Also, because propositional axioms are not incorporated, the theory $\{p,\,\neg \neg \neg p\}$ is L-consistent for the same logic L as above.

I would speculate that the reason for the above flaws is that the author of the article attempted to use semantically-defined notion of "derivable", despite this statement (quoted from the article):

"Semantics is useful for investigating a logic (i.e. a derivation system) only if the semantic consequence relation reflects its syntactical counterpart, the syntactic consequence relation (derivability)."

apparently hoping to get away without any rules of inference, based on the fact that if a logic in question is sound and complete (in the classical sense and not in the article's sense) then its semantic consequence relation is equal to its syntactic consequence relation. (That is what the completeness theorem usually states.) This didn't work quite well, because of some details (like the ones above) that need to be fixed.

The above would explain a simplistic definition of (modal) logic as "a set of formulas". Usually, a logic has a provability relation $\vdash$ incorporated in it (whether syntactically or semantically defined) that the author, apparently, hoped to avoid up until his definition of L-consistency.

I can offer here a quick fix to all these flaws. Just define L-consistency this way:

"A set of formulas $\Sigma$ is L-consistent iff $\Sigma \cup L$ has a Kripke model."

But then axiom K (as well as the rules of inference) are superfluous.

Also, the presentation may use some polishing. For instance, the falsehood symbol $\bot$ is used in the section Semantics of intuitionistic logic but never formally introduced. Having $\bot$ aboard, negation $\neg \varphi$ may be introduced as an abbreviation of $\varphi \rightarrow \bot$. This would allow to simplify the set of propositional axioms that are needed for the correctness of the syntactical definition of L-consistency (mentioned above).

A link to forcing needs an explanation.— Preceding unsigned comment added by 76.95.183.31 (talk) 19:49, 2 July 2013‎ (UTC)

I’m afraid you’ll need to learn at least the basics of modal logic before offering such “fixes”. Yes, $\{p,\neg \Box p\}$ is an L-consistent set (that is, unless L proves $p\to \Box p$). The purpose of the definition is not consequence relations (though it can be in fact used to define the local consequence relation of the logic), but the construction of canonical models. The maximal consistent sets correspond to sets of formulas satisfiable in a particular point of a Kripke model, not true in the whole model. Defining consistent sets semantically makes no sense, as the whole point of the construction is to prove the completeness theorem, we need to start with a syntactically consistent set, and show that it is satisfiable in a model, not the other way round. All of this is described in any modal logic textbook (e.g., Sections 4.1–2 of Blackburn, De Rijke, and Venema, or Section 5.1 of Chagrov and Zakharyaschev; a preemptive warning, both books use $\vdash$ to denote local consequence, so no necessitation).

I have no idea what you are talking about vis a vis intuitionistic logic. $\bot$ is one of the basic connectives of intuitionistic logic, so it needs no more “formal introduction” than $\land$ or $\to$. This is an article on semantics, its business is not to introduce the language of intuitionistic logic, which is described properly in the intuitionistic logic article.—Emil J. 11:52, 3 July 2013 (UTC)

Rebuttal to replay to Major Omissions

Don't be arrogant.

Whatever the "modal logic textbooks" you know of are doing, can most likely be done differently. It's not that mathematical logic serves at pleasure of modal logic. You may wish to take a note of it. (A side comment: the rest of the world uses the term theory where you and few others use logic.)

Anyway, I didn't make false statements. You did. And the article you defend has flaws.

• Even in the local sense, the definition of L-consistency is still incomplete. It declares the theory $\{p,\,\neg \neg \neg p\}$ L-consistent for any propositional variable p and logic L with no axioms (or only with axiom scheme K).

• Your stipulation that "defining consistent sets semantically makes no sense" is false. That's what some skilled logicians (e.g. late Barwise) did/do in order to prove the completeness theorem (which incorporates both completeness and soundness). One of the immediate consequences of the completeness theorem is that the semantic and the syntactic definitions of consistency are equivalent. And vice versa, the completeness theorem is an easy conclusion of the consistency theorem (the equivalency of the semantic and the syntactic definition of consistency). This is particularly easy in propositional logic, to which the trick with elimination of necessitation rule is apparently reducing the modal one.

• Your claim that "we need to start with a syntactically consistent set, and show that it is satisfiable in a model, not the other way round" is false, to. The "other way round" is typically used to prove the soundness (which is part of the completeness theorem in the standard sense). Besides, it appears naive to believe that one can or cannot prove the completeness theorem depending on which definition one begun with.

It's just a matter of technicalities which definition is used, unless, that is, one uses the syntactic definition without properly formulating it. So, it would be better if you used semantic definition taking into account your reluctance to admit that rules of inference are part of (the definition of) logic, for instance,

"A set of formulas $\Sigma$ is L-consistent iff $\Sigma \cup L$ true in (satisfied by) a possible world in a Kripke model",

and then prove, if you can, that $\Sigma$ is L-consistent iff L can't derive $\bot$ from $\Sigma$. This will land you right away on a completeness (soundness included) theorem. Or - to make it even more clear - you could use this definition:

"A set of formulas $\Sigma$ is L-consistent iff $\Sigma \cup L$ satisfied by a truth assignment that treats each formula $\Box \varphi$ as a propositional variable,

working out details of the proof of the completeness theorem like many do in mathematical logic.

Or if you prefer yours (which I bet you do regardless of the consequences), at least make sure it's correct and does not make $\{p,\,\neg \neg \neg p\}$ L-consistent for L as above.

Also, calling these sets propositionally L-consistent would be more honest as some of them disobey the necessitation rule.

• $\bot$ is the falsehood constant and hardly just a "basic connective of intuitionistic logic". (It's silly to call it connective as it does not connect anything nor is it connected to anything.) You used it in section on intuitionistic logic without including it in the alphabet of the language (just like you did with the $\top$ truth constant in the scheme D), although you did bother to include $\rightarrow$ and $\neg$, much more common connectives than $\bot$, at the beginning of the article. It shows poor workmanship to have all three: $\bot$, $\rightarrow$ and $\neg$, particularly if you use both $\Box$ and $\Diamond$ in your axiom schemes. You may declare $\neg A$ is an abbreviation of $A\rightarrow \bot$, which will make at least the "$\{p,\,\neg \neg \neg p\}$ is L-consistent" problem go away. (I am sure there are may ways of fixing flaws of this article.)

And an aesthetic comment. I added $\Diamond (A\rightarrow A)$ to your list of axioms rather than $\Diamond \top$ because the former looks more like the rest of them. If you use the latter, you need to include $\top$ in the language's alphabet together with variables, connectives and modalities, or else your article will have one more flaw.. — Preceding unsigned comment added by ‎76.95.183.31 (talk) 04:31, 4 July 2013 (UTC)

You call me arogant, and yet you continue to make baseless claims about “major omissions” and “flaws” in the article, which are actually due to your poor understanding of the subject.

Since you still do not get it: the section “Canonical models” is about canonical models, not about consistency. As it happens, the construction of canonical models involves a notion of consistent sets. The definition that makes the construction of canonical models work is the one in the article, not any of those you suggest. It is completely irrelevant that some other notions of consistent sets may or may not be useful in a different context. In any case, the definitions and terminology in this section are perfectly standard. And no, $\{p,\neg \neg \neg p\}$ is not consistent, because it derives a contradiction already in classical propositional logic (though this admittedly wasn’t clear when the definition was originally worded with axioms in place of theorems).

In intuitionistic logic, $\bot$ is a nullary connective, whether you like it or not. The language of intuitionistic logic is defined in the intuitionistic logic article where it should be, it is quite tangential to the topic of this article, so there is no point in repeating it here. There is no problem with $\{p,\,\neg \neg \neg p\}$, but even if there were, this would concern the first part of the article dealing with modal logic, it would have nothing to do whatsoever with the definition of $\neg p$ as $p\to \bot$ in intuitionistic logic.

As for the usage of $\top$ and $\bot$ in the modal part, I think that readers are not idiots, and therefore it is not necessary to point out at the very beginning the obvious convention that since modal logic extends classical logic, other Boolean connectives than those indicated are introduced as abbreviations the same way as in classical logic (while you are making so much fuss about $\top$ and $\bot$, modal formulas in the article also include $\lor$ and apparently two different notations for equivalence), but in principle this would not do any harm. Finally, including alternative formulations of axioms is redundant and unhelpful unless there is a very good reason for it, such as when an axiom is commonly used in two different forms. The D axiom is commonly written as $\Box p\to \Diamond p$ or as $\Diamond \top$, but it is not commonly written as $\Diamond (p\to p)$, so including the latter does not make sense.

On a general note, this is an article about semantics, not syntax, so nitpicking on trivial syntactic matters such as what exactly is taken as the set of basic connectives is distracting and unhelpful to the readers.—Emil J. 11:04, 4 July 2013 (UTC)

The "fix" with theorems injects another omission

The "fixed" definition:

"A set of formulas is L-consistent if no contradiction can be derived from it using the theorems of L, and Modus Ponens"

with which you replaced the original definition:

"A set of formulas is L-consistent if no contradiction can be derived from them using the axioms of L, and Modus Ponens"

(that improperly declared the theory $\{p,\,\neg \neg \neg p\}$ L-consistent for any propositional variable p and logic L with no axioms (or only with axiom scheme K) since in the language of propositional modal logic defined in the article one cannot derive $p$ from $\{\neg \neg p\}$ nor vice versa using only axioms K and Modus Ponens) injects the concept of "the theorem of L" which you haven't defined in your article. It replaced a major flaw with an undefined concept. (Also "if" needs to be replaced with "if, and only if,").

Another omission is the use of "proves" in "L1 does not prove all theorems of L2" and "but does not prove the GL-tautology" in the article without a definition of "proves" there (specifically, what axioms beyond L1 and what rules of inference are allowed in your definition of "proves"?).

And the list does not end here.

Your statement that

"The D axiom is commonly written as $\Box p\to \Diamond p$ or as $\Diamond \top$, but it is not commonly written as $\Diamond (p\to p)$, so including the latter does not make sense"

is a fallacy as it derives a false conclusion from a true premise.

The definition of $\neg A$ as an abbreviation of $A\rightarrow \bot$ is commonly used in elegant formulations (like Lyndon's) of propositional logic, and your trying to confine $\bot$ to intuitionistic logic in this respect suggest your unfamiliarity with that fact.

Then you claim

"It is completely irrelevant that some other notions of consistent sets may or may not be useful in a different context."

Wrong, again. The fact that you don't see how the classic concept of consistency is relevant to this article shows only your inability or unwilligness to see it. Consistency is a ubiquitous logical term with - given a logic in question - pretty unambiguous meaning, notwithstanding the existence of its different definitions. Your characterization of the one I gave before as "some other notion" is incorrect. It was your original definition (corrected later) of consistency that deserved such a characterization.

Some more examples of flaws in your comments:

"you continue to make baseless claims about “major omissions” and “flaws” in the article, which are actually due to your poor understanding of the subject"

(two falsehoods here: 1. if my claims were "baseless" then you wouldn't have to make any fixes, which you did; 2. the "poor understanding" part is not just false, it has all appearances of projection)

"Since you still do not get it: the section “Canonical models” is about canonical models, not about consistency. As it happens, the construction of canonical models involves a notion of consistent sets."

(as if being "about" or being "involved" had any bearing on the need for a correct definition; also, if you claim I didn't get something then prove it; besides, your statement is self-contradictory as is this one: X is not about Y, X only happens to define Y)

"while you are making so much fuss about $\top$ and $\bot$, modal formulas in the article also include $\lor$ and apparently two different notations for equivalence"

(as if one flaw or omission was an excuse for another; it seems very likely that the article also has other flaws/omissions, some of them may become apparent after you properly fix those that I noted)

"The definition that makes the construction of canonical models work is the one in the article, not any of those you suggest."

(you are so wrong on "not any of those you suggest" - or prove it!)

I tried to tone down an earlier version on this post, and need to add a comment for completeness.

You have been working with no compensation writing articles for Wikipedia, for the benefit of others. This is highly commendable. (I often feel that scholars and resaerchers - creators of intellectual property, if you will - are being mercilessly exploited by the rest of the humanity) For that reason, I am sorry for my harshness, but, perhaps, it's in my nature and I couldn't help it.— Preceding unsigned comment added by ‎76.95.183.31 (talk) 17:33, 6 July 2013 (UTC)

A normal modal logic is defined as a set of formulas with certain closure properties. Those are its theorems. Thus, being a theorem is a primitive notion in this context, it cannot be defined in terms of anything simpler. As for “if and only if”, it shouldn’t be used for definitions, per MOS:MATH#Writing style in mathematics. I could go on, but I’m not going to waste any more time on this discussion, as it’s obviously not going anywhere.—Emil J. 18:54, 9 July 2013 (UTC)

Sadly, it is not going anywhere, indeed. If you consider fixing errors and omissions a waste of time then the quality of your article suffers.

Theorem is not a primitive notion. Also, contrary to what you wrote, you defined a logic as a set of formulas without mentioning any "closure properties" (quote: "A modal logic (i.e., a set of formulas) L"). Although you defined the concept of Thm(C) (quote: "We define Thm(C) to be the set of all formulas that are valid in C."), it is a function of a class of structures/frames and not of sets of formulas.

And there are many more glitches in your article.

Is the article fixable? Perhaps. But even if so, this is not a good excuse to not "waste" one's time on cleaning it up.

As far as the if in the definitions replacing iff is concerned, up until some time ago, it was believed by some that it is an unambiguous convention. This, however, is not true in certain contexts, where if is used intentionally together with certain, usually implicit, minimality assumption. It has been demonstrated (for instance, in semantics of logic programming) that the replacement of if with iff - a transformation that was proposed in the past of logic programming in order to make the semantics of logic programs precise - would change the definition in question.

It appears that the authors of the Style of Writing you quoted preferred form over contents. They apparently gave themselves an authority that they didn't earn, and the results are, sometimes, detrimental to precision and correctness.

But if this does not bother you and you have decided to follow the Guide, here is a quotation from it:

"The articles should be accessible, as much as possible, to readers not already familiar with the subject matter."

Have a nice day.

Frame conditions

Text for the second table mentions "the logics are complete with respect to the frame classes given in the table, but they may correspond to a larger class of frames". Is it possible to add a column to show which logics actually correspond to the listed classes of frames? I would also be interested in a few more examples, maybe here or a reference if available. — Preceding unsigned comment added by 173.74.57.70 (talk) 15:38, 12 April 2014 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Kripke semantics. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20041020014707/http://www.princeton.edu/~jburgess/Kripke1.doc to http://www.princeton.edu/~jburgess/Kripke1.doc

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 20:18, 12 December 2017 (UTC)

Satisfaction relation symbol

Is the use of $\Vdash$ (\Vdash) rather than $\models$ (\models) for the satisfaction relation merely a glyph variation (like $\phi$ versus $\varphi$), or is there some technical nuance that this choice seeks to express? I'm not suggesting changing the article, just seeking clarification of whether this means anything. One reason this puzzles me is that

Huth, Michael; Ryan, Mark (2004). Logic in Computer Science – Modelling and Reasoning about Systems. Cambridge University Press. ISBN 978-0-521-54310-1.

is using $\models$ throughout, except in the chapter about modal logic, where instead the definition of Kripke model uses $\Vdash$ for the satisfaction relation; this becomes doubly odd considering that the definitions op. cit. of satisfaction are essentially the same in temporal logic as in modal logic, but the authors are using different symbols. (Of course, it could be that one author wrote one chapter whereas the second wrote the other, and no editor enforced notational consistency.) Here in Wikipedia, articles Kripke semantics and Modal logic use different commands for the satisfaction relation. 95.195.195.123 (talk) 12:42, 10 November 2019 (UTC)

@ sign

According to the article at sign, "a 'designated' world in a Kripke model may be labelled '@'", but I see nothing in this article to support that claim. Is it true? If so, does anyone have a citation? --John Maynard Friedman (talk) 00:01, 25 March 2021 (UTC)