Explanation of states, models and worlds in Kripke semantics?

Can someone explain to me how the concepts of states, models and worlds work together in Kripke semantics?

I've been trying to piece together how the parts work are linked together but cannot figure it out.

From what I understand, a model $M$ consists of worlds. Now as far as I can gather from that, states would be the same as worlds. However, I cannot find this confirmed anywhere.

Could someone explain to me how these concepts work? Obviously, I've googled them, but most texts are quite complicated to grasp with little experience on the subject. Even textbooks remain quite vague.

• You can understand a state as a world and a set of states as a set of worlds. The different terms are used by different communities. If you are interested in logical and meta-logical characterisations, then the notion of a world may suffice. If you want to analyse a single model and that model is generated by a program, the structure of the state becomes important. – Vijay D Aug 8 '13 at 0:33

Here is a sketch (massively simplifying for reasons of pedagogy):

Setting the scence. You can think of logic as a tool, an API in computing parlance, to reason about things, where reasoning means deriving true statements from true assumptions. The things that we reason about using logic is called a model. What makes logic useful is that this API, in particular its dominant strain called first-order logic (of course there are other logics), is completely generic, meaning we can use it to reason about teddy bears, cars, bridges over rivers, stars, computation, whatever you want. Because logic is so generic, we can build up a generic reasoning infrastructure that can be reused in many domains. Example include interactive theorem provers, SAT solvers, textbooks, social conventions such as learned journals, career structures in the sciences, conventions about when we deem to have lost/won an argument etc. So logic is a great labour saving device, because we don't have to reinvent these core tools again and again for everything that we want to reason about.

Is logic all we need to reason? Naturally not. Because logic is generic, we have to inject domain specific assumptions, usually called axioms, to cater for domain specific knowledge (e.g. ZFC or Peano arithmetic to found mathematics, deontic axioms for reasoning about ethics etc).

What has all of this to do with Kripke semantics? Often we want to reason about things that change over time (e.g. traffic at a traffic light, concurrent processes using shared memory communication, knowledge of observers). We can do this by injecting suitable axioms into first-order logic for each domain separately. However, just as with first-order logic, it turns out that a lot of the axioms that we need to reason about change are similar regardless of what changes over time. So why not 'factor out' this similarity and create an API for reasoning about change, just as we did with first-order logic as an API for general reasoning? Let this new logic/API be called modal logic.

Now we come back to the notion of model, because models are what we reason about.

What is this API called modal logic about? Well, things that change. Let's call them worlds. Now , the worlds change into each other over time. Would a description of this change not be a binary relation on the set of world? The set of worlds together with the relation is the model.

Voila, Kripke semantics.

Warning: the description above is simplistic, and terminology is not uniform. Moreover, for most modal logics the model must also account for variables. In more neutral terminology (and still simplifying), a model is a triple $( W, R, \sigma )$ where

• $W$ is a non-empty set (elements of W are called nodes or worlds or points).

• $R$ is a binary relation on $W$, and is known as the accessibility relation which regulates how 'time' flows.

• $\sigma$ is a map from variables (in the ambient logic) to the powerset of W. The idea behind $\sigma$ is that $\sigma$ controls at what points/worlds the variables are true.

If you want to know even more, maybe check the Wikipedia entries on Kripe semantics or modal logic or any good book on the subject such as Modal Logic, by Blackburn, de Rijke and Venema.

• Added note on the existence of more than one kind of logic. – Karl Damgaard Asmussen Aug 8 '13 at 13:25
• @KarlDamgaardAsmussen that's right, there are many logics. First-order logic is somewhat canonical though (e.g. the meta-theory of most logics is developed in FOL), and it might be helpful at for the original poster not to worry too much about other logics. – Martin Berger Aug 8 '13 at 13:45
• I am not talking about First-Order/Second-Order, I mean Intuitionistic/Classical and weaker systems. – Karl Damgaard Asmussen Aug 8 '13 at 15:24
• @MartinBerger, thank you, but as D.W. says this contradicts with the notion that states are equal to worlds. In particular, this seems to say that a collection of states is the world, which looks to me like the world is the same as the model. Could you clarify in the last part how models fit in to the story? Thanks for the explanation so far though :-) – Mythio Aug 9 '13 at 19:39
• @D.W. You are right. I'm sorry, the terminology is not uniform (partly because there are so many different modal logics), and confusingly I have made terminological choices that are unusual. I added some explanation. I hope it's more clear now. – Martin Berger Aug 15 '13 at 12:00