Propositional dynamic logic with local assignments (Q1062972)

An extension of propositional dynamic logic is proposed which allows a new kind of program terms - local assignments \(p:=v\) of truth-values v to propositional variables p. In this logic many notions, like equivalence of programs, looping and finitely branching, as well as the truth in the (standard model of) first order arithmetic are expressible. In fact it is equivalent in expressive power to first-order logic with transitive closure and its validity problem is \(\Pi^ 1_ 1\)-complete.