策略逻辑可满足性问题的精确复杂度
Exact Complexity of the Satisfiability Problem for Strategy Logic
AI总结：
本文证明策略逻辑的可满足性问题是$\Pi^1_\infty$-完全的且与二阶算术计算同构，即使使用$\omega$-规则也不可递归公理化。
AI中文摘要：
我们证明了由Mogavero、Murano和Vardi提出的策略逻辑的可满足性问题是$\Pi^1_\infty$-完全的，并且更强地，它与真正的二阶算术计算同构。下界是针对策略逻辑的next-time布尔目标片段建立的。因此，策略逻辑不是递归可公理化的，即使使用有效定义的$\omega$-规则也是如此。
英文摘要：
We show that the satisfiability problem for Strategy Logic introduced by Mogavero, Murano, and Vardi is $Π^1_\infty$-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 $ω$-rules.
