Abstract

It was conjectured by Halpern and Kapron that frame satisfiability of propositional modal formulas is incomparable in expressive power to both $\Sigma^1_1$ and $\Sigma^1_1$. We prove this conjecture. Our results imply that $\Sigma^1_1$ and $\Sigma^1_1$ are incomparable in expressive power, already on finite graphs. Moreover, we show that on ordered finite graphs, i.e., finite graphs with a successor, $\Sigma^1_1$ is strictly more expressive than $\Sigma^1_1$.