# How is Kripke-style modal logic distinct from classical propositional logic with additional axioms?

I've been considering the possible-worlds semantics for simple forms of modal logic, such as Kripke modal logic. This reading of modal logic seems to be a reduction to restricted truth-tables, where each row of the truth-table corresponds to the truth-assignment to propositions in (one or more) conceivable worlds; and the worlds which we deem possible are some subset of these rows.

Consider a proposition A, and some selection W of possible worlds which corresponds to some particular rows of a truth-table. We also introduce a (trivial) modal notion of a conceivable world, which is more general than a "possible" world in that all rows of the truth table are considered to correspond to conceivable worlds; and let U correspond to the set of all concievable worlds, containing the actually possible worlds as a subset. The usual notion of the truth of A in some world w ∈ W (or w ∈ U) is then written v(A,w). In this reading of modal logic, □A means that in all admissible rows, A holds, i.e.

∀w∈W: v(A,w)=T  ;

and ◊A means that in some one or more admissible rows, A holds, i.e.

∃w∈W: v(A,w)=T  .

This makes immediately clear why A⇒□A is valid in Kripke modal logic, while □A⇒A is not; if A is a theorem (and our logical system is sound), this means that

∀w∈U: v(A,w)=T  ,

that is A holds in all conceivable worlds, without restriction merely to the possible worlds, so that it clearly implies that `∀w∈W: v(A,w)=T`. Thus clearly A⇒□A; is valid. On the other hand, □A⇒A is not valid, as the truth of A in all conceivable worlds (all worlds in U) is not implied by its truth in only the possible worlds (all worlds in W ⊆ U).

Question. How is the restriction to possible worlds, in this case, not simply equivalent to adopting a supplementary propositional premise which is true in precisely the set of possible worlds, so that □A is synonymous with W⇒A where W is true in all possible worlds and only the possible worlds?

• I think I understand the question, but some of the post is not clear to me. (1) Could you explain to me what this says: 'A means that the proposition A holds in all conceivable worlds, without restriction to the "possible" worlds selected for consideration'. I feel like there should be something else instead of the first 'A'. Also, suppose we call that wider notion of necessity 'N' instead of '□'. Question (2): which of your boxes are 'N's and which '□'s? Nov 3, 2013 at 4:51
• @HunanRostomyan: the "wider sort of necessity" to which you refer is simple validity (possibly subject to some set of axioms). I have attempted to clarify what I mean. I really do mean for a 'concievable' world to be a trivial notion truth-functionally: A is true in all 'concievable' worlds if and only if A is valid. Nov 3, 2013 at 12:54
• Just to point out for people who haven't read the SEP link, the implication `A⇒□A` obtains in K when A is a theorem - not in generality. Nov 4, 2013 at 0:19
• @PaulRoss: I suppose that's a distinction which I read, but missed. Would you go further to say that Γ⊨A⇒□A is valid, if and only if Γ⊨A is valid for the subset of the possible worlds? Nov 4, 2013 at 11:18
• @NieldeBeaudrap, there might be a counterexample if `Γ⊨¬A` was valid, because then `Γ⊨A⇒P` (for any P, including □A) would just fall out from the way the conditional is defined. Nov 4, 2013 at 19:25

First up, we need to correct a big difficulty, you seem to be conflating truth and provability. A does not imply □A.

There's plenty of scope for contingent truth in system K- that is: there is plenty of scope for dealing with true propositions A which are true but not necessarily so- which just, as it were, happen to be the case. That Nixon was elected president, for example, is true in the actual world, but that does not entail that he was elected president in all possible worlds.

Now we have that under our belt, why is modal logic significantly different from classical logic?

Firstly, the modal operators are at least potentially very much world dependent (provided we do not include additional axioms such as S4- mentioned in the SEP article you linked). That is to say: from worlds which are possible from our point of view, we may be able to see other worlds as possible which were not possible from our original point of view. This fact (kept track of in the access relations between the worlds) means that we must do some extra work in evaluating modal propositions, chasing around a potential web of possibility.

Secondly, things get screwy when we introduce quantifiers. Since necessity and possibility are quantifiers of a sort themselves, we might assume they commute, that is:

◊∃x.A(x) => ∃W∃x.v(A(x),W)=T => ∃x.◊A(x)

But this is not necessarily the case- the above argument schema would say (roughly) for example that "There is possibly a man in my closet" implied "There is a man who is possibly in my closet", which are very different things (the latter seems to imply that you know of a particular guy, which seems somewhat stronger).

This (I would say metaphysically shaky) argument schema is a corollary of the Barcan formula, and has stirred up some controversy. If we introduce it as an axiom, though, that makes for some logical gymnastics that properly transcend those of simple in-world deduction.

The above considerations point to the nub of the difference between modal and classical logics. In short: deductions occur not just in worlds, but between them, and that means weird stuff goes down...

• "you seem to be conflating truth and provability" ... but your example of "Nixon was elected" is not valid; it happens to have been true, but only if you grant enough data about the past (that we might grant as axioms) that it is derivable from it. These axioms select for the actual world; by which, of course, we mean the unknown one of the possible worlds compatible with this data which we inhabit (in which it is possible that Nixon ate a ham sandwich on October 17, 1962). Under what circumstances is it a theorem that Nixon was the president, and is it not necessary under those axioms? Nov 3, 2013 at 19:43
• Moving on... you go on to describe a misconception that I might have, but given that I didn't really bring up anything to do with quantifiers and commuting them past one another, I'm not sure where you got that from. Of course, one should be careful about literal translation between idiomatic language (e.g. everyday English) and formal logic. Just because I don't have in mind someone specific who might be in my closet (something like a constructive proof that there exists someone who is possibly in my closet), doesn't mean that there might not be someone who could possibly be in my closet. Nov 3, 2013 at 19:55
• Perhaps the one pertinent thing in your answer which gets at the point of my question is "deductions occur not just in worlds, but between them". This implies that a classical logical deduction occurs within a world. Well... could you actually present an example of that, and how it affects attempts to interpret it using subsets of the rows of truth-tables? I can see how ◊A⇒B is an interaction (a boot-strapping inference from one world into all), but how would one derive this except by axioms which would also imply A⇒B? Nov 3, 2013 at 20:01
• I would like to emphasize that it is not at all clear how ∃◊ formally differs from ◊∃ in terms of validity. Let `Cx` be "x is in my closet". Then `◊∃xCx` means that there is a world in which `Cp` for some p, so that `◊Cp` and so `∃x◊Cx`. Conversely if `∃x◊Cx` then `◊Cp` for some p, so that in some world `Cp`; then in some world `∃xCx` so that `◊∃xCx`. It would seem that the two are equivalent, unless one has more strict rules for existential (and possibilistic) generalization, as constructivists do. How does your word of warning, then, relate to the possible world semantics as in the SEP? Nov 6, 2013 at 15:15

Referring to the Wikipedia page on Kripke semantics (with minor reivisons of notation):

A Kripke frame or modal frame is a pair (W,R), where W is a non-empty set, and R is a binary relation on W. Elements of W are called nodes or worlds, and R is known as the accessibility relation.

A Kripke model is a triple (W,R,|⊢), where (W,R) is a Kripke frame, and |⊢ is a relation between nodes of W and modal formulas, such that:

• w |⊢ ¬A if and only if ¬(w |⊢ A);
• w |⊢ A ⇒ B if and only if ¬(w |⊢ A) or (w |⊢ B);
• w |⊢ □A if and only if (u |⊢ A) for all u such that wRu.

A formula A is valid [in a] model (W,R,|⊢), if w |⊢ A for all w ∈ W [...] .

So the notion of a world may in principle differ from a single row of a truth-table, or a set of rows of a truth-table. The first axiom would certainly apply for a single row of a truth table, but does not make very much sense for multiple rows of a truth-table; conversely, the fact that necessity is defined in terms of further worlds accessible from a single world mean that it does not make sense to treat a world in terms of a single row of a truth-table unless one is happy to see either the notion of 'necessity' or the notion of 'accessibility' trivialise.

The Wikipedia page goes on to note various possible properties that the accessibility relation can have, including:

A ⇒ □A   [which is equivalent to]   wRv ⇒ w=v

which is to say that if A ⇒ □A is valid for all A (and not just e.g. when A is a theorem or other valid proposition), then the accessibility relation does trivialise, so that w |⊢ □A if and only if w |⊢ A. Then rows of truth tables can provide a Kripke model, and any set W of possible worlds which can be expressed in a finite number of symbols can by that fact be encapsulated by a proposition W which is true precisely in the set of all possible worlds, so that ⊨ □A if and only if W ⊨ A.

In short, contrary to what one may be led to believe by the SEP section on possible world semantics, there are a wider variety of models for Kripke modal logic than rows of truth-tables directly allows; and that in those models where worlds do amount to rows of truth tables, the semantics of □A is very boring if one is concerned with validity relative to a set of premisses. (On the other hand, these pessimistic remarks do not hold so clearly for ¬□A, which is to say for propositions of the form ◊B, as it does not correspond to any proposition holding in all such rows of the truth table.)

• Incidentally, I would be happy for someone to provide a better answer than this, which could really exhibit a richer and more interesting construction of a Kripke model, to illustrate the limitations of either the semantics section of the SEP article or of my understanding of that section. Nov 5, 2013 at 0:33
• Part of my problem is that I am interested in logic as a tool not merely for describing truth, but inferring it. I cannot easily find any references which are intermediate between "It is true that Nixon was the president, but not necessarily true" (in which no breath is gasped regarding which premisses are granted, nor what the space of possible worlds is), and total abstraction on the level of describing different possible properties of the accessibility relation. I am writing my own answer only because I wish someone would write a better exposition, but will do so if no-one else does. Nov 6, 2013 at 0:41
• @ThomasKlimpel: I have revised the answer essentially to reduce the most contentious paragraph to a sentence at the coda of the conclusion. Of course, you might feel that I'm still getting a grasp on modal logic more generally, and you would be right. If you have any recommendations as to how to improve the answer for someone whose priorities tend towards inference of validity/possibility/necessity (e.g. rather than merely attempting to represent conventional informal meanings by transliteration of English words to boxes and diamonds), I again ask you to improve the answer or to write another. Nov 6, 2013 at 15:05

Modal logic is useful for me, because it allows me to better separate the dynamic aspects from the static aspects of mathematical models.

Let me try to illustrate this in the context of universal algebra. Here, we basically start with a collection of operations over some set, and are interested in equations using these operations. (For my purpose here, universal algebra may be regarded as a very limited subset of predicate logic). The equations contain variables, and we might want to distinguish the validity of an equation for specific values of the variables from the validity of an equation for every possible assignment of values to the variables. An equation A is necessarily valid, if it is valid for every possible assignment of values, which we would denote □A in modal logic. This has to be distinguished from the validity of the equation for a specific assignment of values.

In the example above, the operator □ satisfies the axioms of the modal logic system S5. The description of the possible-world semantics given in the question is the one for S5, but this may be part of the confusion (as the question never mentions S5 explicitly, contrary to the SEP article). The question mentions Kripke modal logic, which could be interpreted as a reference to system K. To illustrate the difference between different modal system, I will now modify the example above such that the operator □ no longer belongs to system S5, but only to system S4.

We might want to consider parameters in addition to variables. We can turn any variable into a parameter, by just stating that we want to treat it like a parameter instead of like a variable. So let's add the information which variables should be considered as parameters to our assignment of values to the variables. The meaning of □A is now restricted such that the parameters are kept fixed. In order to define the meaning of □□A and □¬□A, we allow that a variable may be "converted" to a parameter, but a parameter cannot be turned back into a variable.

Universal algebra commonly doesn't use modal logic, so how does it work around this? How is this related to what I called "static and dynamic aspects of mathematical models"? One way to treat parameters is to add an additional constant symbol (0-ary function) to the non-logical language for each parameter. The drawback is that this modifies the system we want to investigate, but me might prefer to keep our model "static". We could add a sufficiently large numbers of constant symbols to our non-logical language, so that we always have a spare symbol when we need an additional parameter. So yes, in practice you can probably find workarounds to avoid modal logic, but it depends a bit on the questions you want to investigate whether this is a good idea or not.