0

I was reading about dynamic logic over at wikipedia as a possible lead on a previous question. However, its not making a lot of sense to me. In particular, wikipedia says that

The constant action $0$ ... does nothing and does not terminate, whereas the constant action $1$ ... does nothing but does terminate.

That's fine, although its slightly odd that they refer to both $0$ and $1$ as "the constant action." I feel like only $0$ should be referred to as the constant action, since $1$ does something fairly drastic, in particular it terminates the program. Anyway, we then come to the following axiom

$$(A1) \;\;[0]p$$

which apparently reads, "it is necessary that if we enact the constant action that does nothing, then $p$ will hold," which seems like nonsense. We also have the following corollary

$$(T1) \neg \langle 0 \rangle p$$

which seems to be saying, "it's not possible that after performing the constant action that does nothing, we will observe that $p$ holds," which also sounds like nonsense.

So, I'm guessing that there's some mistakes on the wikipedia page. What are the correct conventions?

Community
  • 1
goblin GONE
  • 67,744

2 Answers2

1

I have no prior knowledge of dynamic logic, but what you quote seems to fit together nicely.

"0" and "1" are "constant actions" in the sense that each is the name of one particular action which is the same action each time you mention the name. In other words, they are constants of type "action". That does not refer to what the actions they name actually do. (And the wording is arguably confusing, yes).

The axiom $[0]p$ effectively defines that 0 is an action that it is always impossible to take. What the axiom says that if you take it anyway, then anything will be true -- which is vacuously valid because you can't take it.

This is perhaps even clearer in the form $\neg\langle0\rangle p$, which directly says that "it is not possible to perform 0 and then have $p$ be true". If we let $p$ be the logical constant $\top$ (true), $\neg\langle0\rangle \top$ says neither more nor less than "it is not possible to perform 0".

hmakholm left over Monica
  • 286,031
  • Okay, but the quote says that: "0 ... does nothing and does not terminate." If it does nothing, why is it impossible to take? – goblin GONE Oct 13 '13 at 23:07
  • @user18921: That quote seems to be an attempt to convey intuition, and evidently not doing it very well in your case. The formal definition of what $0$ does is the axioms it satisfies, not how someone thought he could popularize it. --What is meant by "does nothing" must be that it doesn't say anything in particular about how the world before doing $0$ relates to the world after doing $0$, because there is no world after doing $0$. – hmakholm left over Monica Oct 13 '13 at 23:11
  • ... or perhaps better, $0$ "does nothing" in the sense that it doesn't lead to a world that differs from the world before you do $0$ -- but in contrast to $1$ (which does nothing because it always leads to the same world you started from), $0$ does nothing because it doesn't lead to any world. – hmakholm left over Monica Oct 13 '13 at 23:15
  • I certainly think you make a good point about $0$ being a "constant" action, in the same way that $e$ is a constant in the equational language of groups. However, I still think there is a mistake, either in the axioms or in the "intuition" part. Lets wait and see if someone with some experience in the field will post and clarify. – goblin GONE Oct 13 '13 at 23:20
  • Oh wait. I think I get it now. $0$ is the action that "runs forever" and never gets around to terminating. So you were right, there is no mistake on the wikipedia page. – goblin GONE Oct 15 '13 at 16:33
0

I think I finally get it. When the page says "it does not terminate," the intended meaning is that the process $0$ never gets around to finishing. Thus, the statement $$[0]p$$

basically reads: "After the process that never gets around to finishing has finished, it is necessary that $p$ holds." This sounds completely reasonable.

So, the Wikipedia page is fine.

goblin GONE
  • 67,744