{"id":"arxiv/2609.16173","url":"https://arxiv.org/abs/2609.16173","tags":["math.LO"],"score":0,"title":"Exact Complexity of the Satisfiability Problem for Strategy Logic","domain":"math.LO","source":"arxiv","authors":["Tikhon Pshenitsyn"],"reviews":0,"subject":"math.LO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-14","reactions":{}}