Henkin-style second-order expressibility conjecture for NDL

Let $NDL$ be the generalized dynamic logic discussed in the paper, and let Henkin-style second-order logic (HSOL) be the corresponding Henkin semantics for second-order logic. A program property is a property of programs expressible in the relevant logic. Henkin-style second-order expressibility conjecture. Every program property expressible in HSOL can also be expressed in $NDL$.

This conjecture is motivated by the observed correspondence between $NDL$ and HSOL: $NDL$ admits a natural translation into HSOL, while program properties expressible in HSOL had, according to the paper's stated experience, also been found expressible in $NDL$.