Well Structured Program Equivalence is Highly Undecidable
Marcel Jackson and Robert Goldblatt
We show that strict deterministic propositional dynamic logic with intersection is highly undecidable,
solving a problem in the Stanford Encyclopedia of Philosophy. In fact we show something quite a bit
stronger. We introduce the construction of program equivalence, which returns the value $\top$
precisely when two given programs are equivalent on halting computations. We show that virtually any
variant of propositional dynamic logic has a $\Pi_1^1$-hard validity problem if it can express even
just the equivalence of well-structured programs with the empty program \texttt{skip}.
We also show, in these cases, that the set of propositional statements valid over finite models
is not recursively enumerable, so there is not even an axiomatisation for finitely valid propositions.