jcreed blog > Towards a Judgmental Reconstruction of Dynamic Logic

Towards a Judgmental Reconstruction of Dynamic Logic

Chris Martens posed a question the other day of what kind of nice constructive/judgmental sense can be made of Dynamic Logic, and I thought I'd write down my thoughts on at least how I think the low-hanging-fruit part of it ought to go. Naturally, I'll use my favorite everything-looks-like-nails hammer, which is taking advantage of focusing to turn semantic clauses — as long as you guess the correct "constructive semantics" clauses — more or less automatically into inference rules.

Refresher on Dynamic/Epistemic Logic

Dynamic logic is a modal logic that I'd heard a little bit about in the past, but I was never really intimately familiar with it. Possibly this is because I hadn't encountered a presentation of it in the style below, so it just seemed like one of those "oh, it's kind of an interesting logic but it seems like a big bag of classical axioms, so I don't really know what sense it makes" kinds of things. The reference I'm using for some of its features is the paper chris referred me to, A Logic for Suspicious Players: Epistemic Actions and Belief-Updates in Games. I can divide the logical features going on in this paper into three rough groups:

So the point of dynamic logic is that you have some type of actions $\alpha$, for which you can talk about the proposition of $[\alpha]\phi$, thought of as meaning "$\phi$ is true after action $\alpha$ is completed". More specifically, it means that for any way of completing $\alpha$, the proposition $\phi$ will be true afterwards.

Right away we can start by defining some trivial actions, \[\alpha ::= 0 \celse 1 \celse \cdots \] with the intended meaning that $0$ is the action that's impossible to complete, and $1$ is the action that has exactly one way to complete, and has no side-effects on the world at all. This would mean that always \[ \prov [0]\phi \] (for, indeed, for all ways of completing the action $0$, of which there are none, it's vacuously true that $\phi$) and \[ [1]\phi \prequiv \phi\] We can also introduce a nondeterministic action \[\alpha ::= \cdots \celse \alpha \cup \beta \celse \cdots \] and we'd expect that \[ [\alpha \cup \beta] \phi \prequiv [\alpha]\phi \land [\beta]\phi \] In other words: for $\phi$ to be guaranteed to be true after a process that might do $\alpha$, and might do $\beta$, is the same as a guarantee that it's true in the event that $\alpha$ actually happens, and a guarantee that it's true after $\beta$.

There's also a notion of sequencing of actions: \[\alpha ::= \cdots \celse \alpha \cdot \beta \celse \cdots \] The intended meaning of $\alpha \cdot \beta$ is "do $\alpha$, and then do $\beta$". We'd expect the equivalence \[[\alpha \cdot \beta]\phi\prequiv [\beta ][ \alpha]\phi \]

Finally, we want to introduce a way for actions to interact with truth of propositions. There is a test action \[\alpha ::= \cdots \celse ? \phi \] with the intended semantics that the action $? \phi$ can complete (and has no side effects) only if $\phi$ is currently true.

Semantics

The complete syntax of propositions and actions might then look like \[\phi ::= \top \celse \bot \celse \phi \lor \phi \celse \phi \land \phi \celse \phi \imp \phi \celse [\alpha]\phi \celse p \] \[\alpha ::= 1 \celse 0 \celse \alpha \cup \alpha \celse \alpha \cdot \alpha \celse ? \phi \celse \pi \] where we include some atomic propositions $p$ and atomic actions $\pi$ to go at the leaves of the expression trees. We want to define a translation of this source language into a more low-level ambient metalogic that we can think of a focused proof-theory, and derive some judgmental-looking inference rules for $[\alpha]\phi$.

This translation will be essentially a Kripke-style possible-world semantics. We have a notion of worlds $u, v, w$, and the translation takes in a proposition $\phi$ and a world $u$, and spits out a metalanguage proposition. I'm going to write the metalanguage propositional connectives as $\forall, \exists, \lor,\land,\imp,$ etc. and hope that no confusion arises from this overloading.

I'll write this translation as $\phi \wat u$. Let's jump right in and give a translation of $[\alpha]\phi$; we say that the meaning of it is given by \[ ([\alpha]\phi) \wat u = \forall v . R_\alpha(u, v) \imp (\phi \wat v) \] to make sense of this, we have to define $R_\alpha$, takes an action $\alpha$, and two worlds $u$ and $v$, and spits out a metalanguage proposition. We define it recursively on $\alpha$, as follows: \[R_\pi(u, v) = \pi(u, v)\] \[R_{\alpha \cdot \beta}(u, v) = \exists w . R_\alpha(u, w) \land R_\beta(w, v)\] \[R_{\alpha \cup \beta}(u, v) = R_\alpha(u, v) \lor R_\beta(u, v)\] \[R_{1}(u, v) = u = v\] \[R_{0}(u, v) = \bot\] \[R_{? \phi}(u, v) = \phi \land (u = v)\] where we postulate that every atomic action $\pi$ comes equipped with some metalanguage binary relation $\pi(u, v)$ on worlds. The interpretation of every other proposition besides $[\alpha]\phi$ (even implication! the Kripke semantics is not here to reify the possible worlds of constructivism itself, but another layer on top of a logic already assumed constructive) is just a boring homomorphism: \[ \top \wat u = \top \qquad \bot \wat u = \bot\] \[ (\phi \land \psi) \wat u = \phi \wat u \land \psi \wat u\] \[ (\phi \lor \psi) \wat u = \phi \wat u \lor \psi \wat u\] \[ (\phi \imp \psi) \wat u = \phi \wat u \imp \psi \wat u\] \[ p \wat u = p(u)\] We do assume that every atomic proposition $p$ comes equipped with a metalanguage unary proposition $p(u)$ on worlds.

Dreaming Up Syntax

So, having written down a "syntactic semantics", we imagine what range of phenomena can possibly occur if we start with a proposition $\phi$, compute $\phi \wat u$, and try to do proof search on the result. Well, if $\phi$ is of the form $[\alpha_1 \cdot \alpha_2 \cdots \alpha_n]\phi$, then we find \[ ([\alpha_1 \cdot \alpha_2 \cdots \alpha_n]\phi) \wat u \equiv (\exists w_1\cdots w_n. R_{\alpha_1}(u, w_1) \land \cdots \land R_{\alpha_n}(w_{n-1}, w_n)) \imp \phi \wat w_n\] Or, up to logical equivalence, we could have also written \[ ([\alpha_1 \cdot \alpha_2 \cdots \alpha_n]\phi) \wat u \equiv \forall w_1\cdots w_n. R_{\alpha_1}(u, w_1) \imp \cdots \land R_{\alpha_n}(w_{n-1}, w_n) \imp \phi \wat w_n\] This means that when we have a proposition like $[\alpha_1 \cdot \alpha_2 \cdots \alpha_n]\phi$ on the right of a sequent, we will need to asynchronously unpack it into a whole sequence of information about possible worlds and actions that transition between them. We therefore might guess that the general form of the sequent of the source language is \[\Gamma; \Omega \prov \phi \] for $\Gamma$ being as usual a context of hypothesized propositions, and $\Omega$ being an ordered list of actions. Semantically, we would say that the meaning of such a judgment is given by \[(\Gamma; \alpha_1, \ldots, \alpha_n \prov \phi)= \] \[\forall u . \forall w_1\cdots w_n. R_{\alpha_1}(u, w_1) \imp \cdots \land R_{\alpha_n}(w_{n-1}, w_n) \imp \Gamma \wat u \imp \phi \wat w_n \] Since $\Gamma$ consists of hypotheses of the form $\phi\ \mathsf{true}$, then $\Gamma \wat u$ would be the conjunction of $\phi \wat u$.

Inference Rules

We can make some progress by trying to start writing down inference rules that decompose non-atomic actions in the context $\Omega$. If we say \[ \Gamma; \Omega, \alpha, \beta, \Omega' \prov \phi \over \Gamma; \Omega, \alpha \cdot \beta, \Omega' \prov \phi \] \[ { \Gamma; \Omega, \Omega' \prov \phi \over \Gamma; \Omega, 1, \Omega' \prov \phi} \qquad { \over \Gamma; \Omega, 0, \Omega' \prov \phi} \] \[ \Gamma; \Omega, \alpha, \Omega' \prov \phi \qquad \Gamma; \Omega, \beta, \Omega' \prov \phi \over \Gamma; \Omega, \alpha \cup \beta, \Omega' \prov \phi \] \[ \Gamma; \Omega, \alpha, \Omega' \prov \phi \qquad \Gamma; \Omega, \beta, \Omega' \prov \phi \over \Gamma; \Omega, \alpha \cup \beta, \Omega' \prov \phi \] then we observe that the interpretation of all these rules are justified by left-inversion rules in the metalanguage. Indeed, by focusing discipline, we can require that these rules are applied eagerly in the source language, until the entire context $\Omega$ consists of nothing but atomic actions and tests.

But now we think about how to write rules for a test $? \phi$ and it seems somewhat unclear with this syntax! Since $?\phi = \phi \land (u = v)$ is a positive proposition, it should invert in this position, but our judgmental apparatus so far isn't general enough to talk about hypothesizing the truth of propositions in the middle of a sequence of world-transitions.

Introducing Mixed Contexts

We want to allow for a mixture of truth-assumptions and action-transitions, so the left side of our sequents should look like \[\Delta ::= \cdot \celse \Delta, \phi\rtrue \celse \Delta, \alpha \ract\] We mean to impose the following structural-rule discipline on such contexts: assumptions $\phi \rtrue$ satisfy weakening and contraction, can be permuted amongst themselves, but cannot be permuted with an $\alpha \ract$, nor can $\alpha \ract$ be permuted amongst themselves, or weakened in general, or contracted. (I believe it's sound to do weakening for actions, only on the left end of the context, but it's not particularly obvious that this should be the case at this point in the narrative) We can get away with eliding the judgment tag (the $\rtrue$ or $\ract$) in almost every case because it can be inferred from the type of the syntactic object.

We can think of such a context as if it were an ordered list of (internally unordered) contexts of ordinary assumptions, linked by actions. \[\Gamma_0 \mapsto_{\alpha_1}\cdots \mapsto_{\alpha_n} \Gamma_n\] \[\approx \Gamma_0, \alpha_1 \ract, \ldots, \alpha_n \ract, \Gamma_n \] where here each $\Gamma_i$ here only containing propositions $\phi \rtrue$.

We could give the meaning of a context recursively by saying \[\cdot \wat u = \top\] \[(\Delta, \phi \rtrue) \wat u = \Delta \wat u \land \phi \wat u\] \[(\Delta, \alpha \ract) \wat v = \exists u . R_\alpha(u, v) \land \Delta \wat u\] and that the intended meaning of $\Delta \prov \phi$ is \[\forall u . \Delta \wat u \imp \phi \wat u\] but we will actually want a slightly more general notion. For any worlds $u, v$, we define $\Delta(u, v)$ to be a metalanguage proposition, defined recursively by \[\cdot(u, v) = (u = v) \] \[(\Delta, \phi \rtrue)(u, v) = \Delta(u, v) \land \phi\wat v \] \[(\Delta, \alpha \ract)(u, v) = \exists w . \Delta(u, w) \land R_\alpha(w, v) \] and observe that the previous definition falls out as a special case of this, since \[\Delta \wat u \equiv \exists v . \Delta(v, u)\] This means another way of expressing the semantics of a sequent $\Delta \prov \phi$ is \[\forall u v . \Delta(v, u) \imp \phi \wat u\]

Action Left Rules

Now we can say \[ \Delta, \alpha, \beta, \Delta' \prov \phi \over \Delta, \alpha \cdot \beta, \Delta' \prov \phi \] \[ { \Delta, \Delta' \prov \phi \over \Delta, 1, \Delta' \prov \phi} \qquad { \over \Delta, 0, \Delta' \prov \phi} \] \[ \Delta, \alpha, \Delta' \prov \phi \qquad \Delta, \beta, \Delta' \prov \phi \over \Delta, \alpha \cup \beta, \Delta' \prov \phi \] \[ \Delta, \alpha, \Delta' \prov \phi \qquad \Delta, \beta, \Delta' \prov \phi \over \Delta, \alpha \cup \beta, \Delta' \prov \phi \] and what's new is that we can say \[ \Delta, \phi, \Delta' \prov \psi \over \Delta, ?\phi, \Delta' \prov \psi \]

Rules for the modality

We've set things up so that the right rule for $[\alpha]\phi$ is easy: \[ \Delta, \alpha \prov \phi \over \Delta \prov [\alpha]\phi \] Both the premise and conclusion of this rule have the same semantics, namely \[\forall u v . \Delta \wat u \imp R_\alpha(u, v) \imp \phi \wat v \] Let's look at how the left rule plays out, though; Most likely it will require us to invent a new judgmental form for what happens to actions on the right, namely in right focus. Let's think about a sequent that's shaped like \[\Delta, \alpha, \Gamma, [\beta]\phi, \Gamma', \alpha', \Delta' \prov \psi \] What I've done is assumed that the context has a $[\beta]\psi$ in it somewhere in the middle, and identified the nearest actions $\alpha$ and $\alpha'$ to its left and right, with $\Gamma$ and $\Gamma'$ being the intervening groups of purely $\rtrue$ assumptions. The meaning of this sequent is something of the shape \[\forall \cdots u, v, w \cdots u_\infty. (\cdots \land R_\alpha(u, v) \land (\Gamma \wat v) \land ([\beta]\phi \wat v) \land (\Gamma' \wat v) \land R_{\alpha'}(v, w) \land \cdots) \imp \psi \wat u_\infty \] so when we left-focus on $[\beta]\phi \wat v$, that is, focus on $\forall v' . R_\beta(v, v') \imp \phi \wat v'$. This means we have to make a choice of future world $v'$, and also prove that $v'$ really is $\beta$-accessible from $v$. Let's make up some notation for this by saying that the left rule for $[\alpha]\phi$ is \[ \Delta_1/\Delta_2/\Delta_3\prov \alpha \qquad \Delta_1, \Delta_2 ,\phi, \Delta_3 \prov \psi \over \Delta_1, [\alpha]\phi, \Delta_2, \Delta_3 \prov \psi \] Now we have to define the judgment \[\Delta_1/\Delta_2/\Delta_3 \prov \alpha\] whose informal meaning is that we can transition from the current world of the first slash, to the current world of the second slash, via action $\alpha$. We define the meaning of $\Delta_1/\Delta_2/\Delta_3 \prov \alpha$ to be \[\forall u,v,w,z . \Delta_1(u, v) \land \Delta_2(v, w) \land \Delta_3(w, z) \imp R_\alpha(v, w)\]

An Exchange Law for this Judgment

Armed with that definition, we can tell that we can allow exchange across slashes for propositional hypotheses (although not actions), i.e. the structural rules \[ { \Delta_1, \phi /\Delta_2/\Delta_3 \prov \psi \over \Delta_1 /\phi,\Delta_2/\Delta_3 \prov \psi} \qquad { \Delta_1 /\phi,\Delta_2/\Delta_3 \prov \psi \over \Delta_1, \phi /\Delta_2/\Delta_3 \prov \psi} \] \[ { \Delta_1 /\Delta_2, \phi/\Delta_3 \prov \psi \over \Delta_1 /\Delta_2/\phi,\Delta_3 \prov \psi} \qquad { \Delta_1 /\Delta_2/\phi,\Delta_3 \prov \psi \over \Delta_1 /\Delta_2, \phi/\Delta_3 \prov \psi} \] because we can prove as a lemma that \[(\phi \rtrue, \Delta)(u, v) = \phi \wat u \land \Delta(u, v)\] and therefore the semantics of both the premise and conclusion of these four rules are respectively equivalent to one of \[\forall u,v,w,z .\Delta_1(u, v) \land \phi(v) \land \Delta_2(v, w) \land \Delta_3(w, z) \imp R_\alpha(v, w) \] \[ \forall u,v,w,z . \Delta_1(u, v) \land \Delta_2(v, w) \land \phi(w) \land \Delta_3(w, z) \imp R_\alpha(v, w)\]

Action Right Rules

Let's now try to write down some rules that decompose $\alpha$. \[ {\over \Delta_1/\cdot /\Delta_3 \prov 1} \qquad \textrm{\textcolor{gray}{(no rule for 0)}} \] \[ \Delta_1/\Delta_2/\Delta_3\Delta_4 \prov \alpha \qquad \Delta_1\Delta_2/\Delta_3/\Delta_4 \prov \beta \over \Delta_1/\Delta_2\Delta_3/\Delta_4 \prov \alpha\cdot\beta \] \[ { \Delta_1/\Delta_2/\Delta_3 \prov \alpha \over \Delta_1/\Delta_2/\Delta_3 \prov \alpha\cup \beta } \qquad { \Delta_1/\Delta_2/\Delta_3 \prov \beta \over \Delta_1/\Delta_2/\Delta_3 \prov \alpha\cup \beta } \] \[ { \Delta_1 \prov \phi \over \Delta_1/\cdot /\Delta_3 \prov ?\phi } \qquad { \over \Delta_1/ \pi /\Delta_3 \prov \pi } \] All of these are admissible with respect to the semantics.

Rules For Ordinary Connectives

We need to settle how regular connectives interact with this judgmental machinery. An easy one to start with is the init rule, which requires that no actions appear to the right of the hypothesis being concluded: \[ \over \Delta, \phi \prov \phi \] Rules for $\land$ and $\lor$ don't do anything surprising: \[{\Delta \prov \phi \qquad \Delta \prov \psi \over \Delta \prov \phi \land \psi} \qquad {\Delta, \phi, \Delta' \prov \theta \over \Delta, \phi \land \psi, \Delta' \prov \theta} \qquad {\Delta, \psi, \Delta' \prov \theta \over \Delta, \phi \land \psi, \Delta' \prov \theta} \] \[{ \Delta, \phi, \Delta' \prov \theta \qquad \Delta, \psi, \Delta' \prov \theta \over \Delta, \phi \lor \psi, \Delta' \prov \theta} \qquad {\Delta \prov \phi \over \Delta \prov \phi \lor \psi} \qquad {\Delta \prov \psi \over \Delta \prov \phi \lor \psi} \] but for $\imp$ we have to truncate the context to the current world in the left rule: \[{\Delta \prov \phi \qquad \Delta, \psi, \Delta' \prov \theta \over \Delta, \phi \imp \psi, \Delta' \prov \theta } \qquad {\Delta, \phi \prov \psi \over \Delta \prov \phi \imp \psi }\] In the semantics, the left rule becomes \[\forall uv.\Delta(u, v) \imp \phi \wat v \qquad \forall uvw . \Delta(u, v), \psi \wat v, \Delta'(v, w) \prov \theta \wat w \over \forall uvw. \Delta(u, v), (\phi \wat v) \imp (\psi \wat v), \Delta'(v, w) \prov \theta \wat w \]

What's Missing

What this handles is actions that can test the truth of propositions at various worlds, but it can't change the truth of them, either actually really changing the value of atomic propositions as in the $\mathsf{flip}$ operation as Baltag has, or changing them in the minds of epistemic agents. It would be very interesting to see how those (or appropriate weakenings of them) might be added in a constructive/judgmental setting, but I don't have any clear ideas right now.