Does the dynamic logic page at wikipedia have some mistakes?

Question

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?

Answer 1

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.

Answer 2

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".