# Interpretation of implication symbol in modal logic

Suppose we have two propositions p and q, and an implication of this form:

p → □q

I can think of two potential interpretations of the meaning of this in terms of possible worlds:

1. If p is true in this world, q must be true in all possible worlds.

2. In any world where p is true, it necessarily follows q is true in that possible world as well. But this should not be taken to rule out that there may be worlds where neither is true. For example, it is necessarily true that if Steve is a bachelor than Steve does not have a living spouse, but there can still be worlds where Steve is not a bachelor and does have a living spouse.

Which of these, if either, is the generally accepted meaning? If anyone can point to a reference by a professional that spells this out that'd be ideal, but if not I'll accept an answer based on personal expertise if there seems to be agreement among those answering.

• What do you mean by "generally accepted meaning"? Modal logic is based on axioms so any proposition has only one "meaning"? Jun 13, 2015 at 14:36
• @Atamari - Correct me if I'm wrong, but I thought the axioms of basic modal logic don't deal explicitly with sets of "possible worlds" (the axioms here don't, for example) but conceptual and philosophical discussions of modal logic often make use of this concept. In general I believe the symbols in any formal axiomatic system are understood not to have any inherent meaning, any interpretation of their meaning requires a "model" of the system in the sense of model theory. Jun 13, 2015 at 15:02
• Your 2) would be [] (p->q), so I am leaning toward 1) But I am having trouble imagining an application that does not involve p -> [] p first. If p is necessarily either true or false by nature of its content, then p -> [] p. if in addition [] (p->q) then p -> [] q.
– user9166
Jun 13, 2015 at 15:27
• @jobemark - Thanks, your first point seems like a good one in favor of 1)--the only thing I would want to confirm is that □(p → q) and p → □q are wholly independent in the sense that neither one can be derived from the other. Jun 13, 2015 at 15:51
• In this sense, if you are asking for an interpretation of a formula, you should give the model first. The truth value of many formulae depends on the accessibility relation. Jun 13, 2015 at 17:12

A Kripke frame is a pair (W,R), where W is a (possibly 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.

We read w ⊩ A as “w satisfies A”, “A is satisfied in w”, or “w forces A”.

The relation is called the satisfaction relation, evaluation, or forcing relation. The satisfaction relation is uniquely determined by its value on propositional variables.

According to these semantical specifications, the truth-value of p → □q must be computed as :

w ⊩ p → □q, i.e. “p → □q is satisfied in w

as follows :

either p is not satisfied (i.e. is false) in w, or q is satisfied in every u such that wRu (i.e. in all worlds accessible from w).

In simpler words : if p is true in a world, q must be true in all worlds accessible from it.