In Krister Segerberg’s modal logic seminar here in Calgary, we were talking about propositional dynamic logic last week. PDL was originally introduced (by Vaughn Pratt in the early 70’s) to reason about programs. In the language, you have propositional variables but then also variables for (indeterministic) programs. Moreover, you have complex terms for programs, e.g., if α and β are programs then α ∪ β is “either do α or do β”, α;β is “first do α then do β”, α* is “do α 0 or more times. If α is a program term and φ is a formula, then [α]φ means “after every execution of α, φ is true”.
The semantics for PDL is your regular Kripke semantics where W is a set of states, V maps propositional variables into ℘(W), and R maps program variables into ℘(W2). The idea is that V(φ) is the set of states where φ holds, and v R(α) w if α takes you from state w to state v (α may be nondeterministic, so it’s a relation, not a function). The definition of ||- is as you’d expect, with w ||- [α]φ if v ||- φ for all v so that w R(α) v. You can put in program constants, e.g., the program 0 that just freezes (R(0) = ∅), the program 1 that does nothing and immediately halts (R(1) = ΔW), and the completely indeterministic program that can take you to any state from any state (R(U) = W2).
Most of the people in the seminar are philosophers, not computer scientists, so we were talking a fair amount of time about how to interpret this semantics not in terms of programs. One way to think of the α’s is as actions types: α is an action type, [α]φ means “φ is true after every action of type α”, and w R(α) v if some action of type α can take you from w to v. For instance, think of W as the set of chess configurations (together with whether it’s black’s or white’s move). Then α might be “move the king”. But this is still pretty close to the programs-changing-state interpretation.
I was thinking of a completely different interpretation, and was wondering if anyone has thought about this interpretation and if it might have any use: In the “intended” interpretation, R(α) tells you which states you can get to from a given state by doing α. But R(α) may be seen as an ordinary modal accessibility relation on W. On this interpretation, PDL turns into a parametrized multi-modal logic with operations on modalities: α is an accessibility relation (e.g., U is the total relation–every world is accessible from every world), [α]φ means “φ is α-necessary), and the operations on programs turn into operations on accessibility relations, e.g., 1 ∪ α is the reflexive closure of α and α* is the transitive closure of α. My hunch is that, maybe by adding some additional operations on the α’s, this could make PDL into a logic of modalities in general.
Hi Richard — I think you are right that the move from ordinary modal logic towards PDL is a move towards greater generality. I am not sure, though, that you have things right side up: it’s not that state transitions are a special kind of modality, I would rather say that modalities are a special kind of state transitions. Thus if (in ordinary modal logic) aRb, this represents a transition from a state a to a state b which is possible relative to a. For a while it was common place that the move from a mono-modal framework to a poly-modal one was trivial (I think van Benthem said so somewhere), but that is a view that is losing traction (and was never right to begin with). Going poly-modal (and PDL is radically so) leads to much greater generality, and things can happen with multiple modalities that can’t happen with just one. This is a view that I tried to press in my talk at the 2007 Logic Colloquium — where you there? — slides for which can be found here.
Thanks for the link! I wasn’t there unfortunately.Re state transitions as special modalities. I guess what I would say is that [α] is a kind of modality (in the same sense in which an S5 ☐ is a modality), and yes, ☐ is then a special kind of [α] (viz., [U]).
Richard — besides the rhetorical point whether modalities are a kind of transitions or vice-versa, the interesting part you mention is the question of what is needed to turn PDL into a general theory of modalities. Speaking of which: what would be needed to qualify as a general theory of modalities? Perhaps something along the following lines: consider a FOL L with only binary predicate symbols and perhaps identity: can each sentence of L be represented by means of operations on modalities?
Wouldn’t rather a theory in whose language you also have variables representing programs/accessibility relations and quantifiers binding them deserve the name of a general theory of modalities? (btw, I don’t know, has anyone worked on such stuff?)
This is an interesting discussion. Thanks. Aldo: you say <>Small Question: what do you mean by “modalities” in this? (I’m sorry if I’m being thick here!) (On another, unrelated point: we want our “general theory of modalities” to cover not only the normal modal frameworks, but also the non-normal. Of course, nothing Aldo or Richard has said rules this out.)Jc
Hi JC,By modalities I mean binary relations over worlds — the idea being that the 2-place predicate symbols in L can be thought of as modalities on which one can then perform the operations from PDL.On reflection, it’s obvious that in some respects PDL outstrips FOL — transitive closure is not definable in FOL but it’s a primitive in PDL. Is the converse also true? How do you represent quantification in PDL? I am not sure.
Hi.In the last semester we had a seminar on dynamic logic, where our first task was to find a different interpretation of this “Pratt” logic. Your idea is very surprising, no one proposed anything like this. We had an another idea in mind, namely to interpret normal propositional formulas as constitutive utterances and programs as performative utterances (in the sense Austin used these terms). It’s still close to the states-and-changes picture, but it may be more interesting, than chess. :)We haven’t spent much time with this interpretation, but you may find this interesting.