Well structured program equivalence is highly undecidable

TL;DR

This paper proves that determining program equivalence in well-structured programs within certain logical frameworks is highly undecidable, with implications for logic, verification, and computational theory.

Contribution

It introduces the construction of program equivalence and demonstrates its high undecidability and non-axiomatizability in propositional dynamic logic variants.

Findings

Program equivalence is $ ext{T}$ iff programs are equivalent on halting computations.

Validity problem is $oldsymbol{ ext{Pi}}_1^1$-hard for certain logics.

Finite model validity set is not recursively enumerable.

Abstract

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 $\mathsf{T}$ precisely when two given programs are equivalent on halting computations. We show that virtually any variant of propositional dynamic logic has $\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.