Exact Complexity of the Satisfiability Problem for Strategy Logic

Abstract

We show that the satisfiability problem for Strategy Logic introduced by Mogavero, Murano, and Vardi is ${\Pi }_{\infty }^1$-complete, and, more strongly, computably isomorphic to true second-order arithmetic. The lower bound is established for the next-time Boolean-goal fragment of Strategy Logic. Consequently, Strategy Logic is not recursively axiomatizable, even with effectively defined $\omega$-rules.