The error concerns the relationship between modal axioms and frame properties. The current SEP entry provides a table

that indicates axioms, their names, and the corresponding conditions on the accessibility relation

R,

but the entailment only holds in one direction, from a specified frame property to that line’s modal schema. The implication **does not hold** in the other direction, for it is false that a specified modal schema must have that line’s frame property. To illustrate, consider the schema (**M**), which the author uses as an example. According to his table, the models in which (**M**) is valid are all based on reflexive frames. But here is a model that isn’t reflexive.

Let N=(W, R, V) be a Kripke model such that W contains two worlds, 1 and 2, R = { (1,2), (2,1) }, and our only proposition variable, p, is true under the valuation function V at 1 and at 2. It follows that

$$! \Vdash^{N} \Box p \rightarrow p, $$

since the formula is satisfied on all worlds in the model N. But the frame that N is based on is **not** reflexive. (It is symmetric.)

There appears to be real confusion in the article rather than a slip in writing, for there is a remark later about bisimulations that is supposed to explain the (false) correspondence between axiom (**M**) and reflexive frames. But bisimulations are a device for identifying *semantically equivalent* models that have *different* frames. The whole point behind bisimulation is to ignore the particular structural properties of the frames behind a set of models, but clump them together so long as they all agree on what is valid. You can then go back to these equivalent models (under bisimulation) to see whether some of them have attractive properties. But that is a separate issue.

Greg, I think you’re right. The problem in section 12 of the article seems to be that one can’t simply substitute Rxy for Ay in the way that’s proposed.

To see this, compare (y)(Rxy->Ay) with (y)(Rxy->Rxy). The author clearly intends these to have parallel translations into modal formulas, but this isn’t the case.

The former, (y)(Rxy->Ay), gets translated as LAx (using L as the necessity operator). The universally quantified variable y gets eliminated in the translation and is replaced by x. But if one does this in a parallel fashion when translating (y)(Rxy->Rxy) the result is LRxx, which says that it’s necessary that x is accessible to itself. Since (y)(Rxy->Rxy) is a tautology and LRxx isn’t, something clearly has gone wrong. Moreover, as a tautology, (y)(Rxy->Rxy) is going to be true in models in which the accessibility relation isn’t reflexive.

I think the entry is assuming that we’re looking at frames without valuations — so a frame satisfies a formula iff it satisfies that formula for *all* valuations. In that case, the chart works fine. (In your example, the frame fails to satisfy the formula at a valuation which makes P true only at world 2).

Nice comments, Steve & Tim.

Tim- I agree that assuming that if we restrict ourselves to validity with respect to a class of frames, rather than to a class of models, then we get the schema-to-property implication. That is to say, we agree that this is the result that should motivate the table.

At first I thought I was just unhappy about the way this was expressed. That would be the slip in writing thesis I mentioned.

But then I read the section on bisimulation, which is supposed to explain the correspondence (which we agree holds for validity w.r.t. classes of frames, not w.r.t. models) and my charity drained away.

Bisimilarity is a technique for identifying invariant models, and it does so precisely by

ignoringframe properties, not by identifying frame properties. If two models are bisimilar, then we know that worlds in one model are related to worlds in the other such that the atomic propositions at the so-related worlds agree, are identical in fact, and the transition possibilities from each pair of worlds are the same. So, for example, in symmetric models (assuming agreement on atomic propositions), you have to move to another world in the course of satisfying (M), whereas in reflexive models you can stay put.The details needed to explain the schema-to-property implication are precisely those that are excluded from bisimilar models.

This is why I opted for the less charitable reading.