Suppose that 5-in-a-row is played on an infinite board, and after an infinite number of moves, if no one won yet and there is an empty square, the game just continues. At limit steps, it is the first player's turn.
Question: What is the complexity of the set of finite winning positions?
I suspect that the complexity is extraordinarily high, with the set of finite winning positions outside of the minimal iterable inner model with an inaccessible limit of Woodin cardinals.
If five in a row Os did not count as a win for the second player, then (even for infinite positions) the complexity is $Σ^0_1$, with the transfinite extension redundant for perfect play (see below for proof).
However, as both players can win, I suspect we can simulate an arbitrary game of the following type:
Transfinite generalized X and O: Players alternate placing 'X' and 'O' respectively on empty squares; at limit steps the first player moves. Game result (Win, Loss, Draw, Incomplete) is determined by an arbitrary arithmetic formula, with the game ending once the result is not Incomplete. ('Incomplete' is only used when there is an empty square.)
Alternative question: Under large cardinal axioms, what is the complexity of this class of games?
Notes:
* To complement the alternative question, one can ask (and is in scope here) about which natural games, extended transfinitely, are complete for this class. Candidates include 5-in-a-row, 5-in-a-row where overlines do not win, Connect6, perhaps some variations of Hex, etc.
* The transfinite extension creates an asymmetry between player 1 and player 2.
* The complexity class seems robust. For example, the complexity remains the same if we allow all second order arithmetic formulas here. Access to the ordering of the moves also does not change the complexity.
Intuition for why 5-in-a-row should simulate this: The complexity of typical 5-in-a-row gameplay suggests that one can implement arbitrary computation. Using it, in the first $ω$ (or more) steps, the players create a suitable grid for the remainder, with $ω$ logical cells (though starting from such a grid may simplify gadgets). Then at each move before the endgame, X plays into one of the logical cells, and O replies in the same cell ($O(1)$ choices for O suffice by using multiple moves to encode an integer). At any point, either player can claim a win/draw (a $Σ^1_1$ statement), and supply an infinite string to support the claim. Then the other player picks a number, and the original player has to verify that the relevant computation halts.
Note: This should work even for $O(1)$ board height. At the end, one player gives a claimed computation (for each step, print tape contents and other data), and the other may claim an error. Then the error check will need to verify that certain two segments in the error claim have equal length, which can be done by alternatively filling cells in the two segments (eg. XOXOX in cell 1 of segment 1, then OXOXO in cell 1 of segment 2; and repeat with cell 2, 3, ...), with an extraneous move detectable (if flagged) through a parity mismatch in filled cell numbers.
Complexity of transfinite generalized X and O, and beyond
Note: This section assumes familiarity with Woodin cardinals and determinacy.
For every countable ordinal $α$ encoded by the position, we can simulate a game on integers (or reals) of length $α$, so the complexity is outside the minimal iterable inner model with $α$ Woodin ordinals. On the other hand, the game must end after a countable number of steps (dependent on the play), and these are games with continuously coded length, so a strong past a Woodin cardinal suffices for their determinacy and winning strategies.
My intuition is that the complexity (both for the first player winning, and the first player not losing) is complete for $(Σ^2_1)^{\text{uB}}$ of the minimal iterable inner model with a proper class of Woodin cardinals. $ω$ moves correspond to a Woodin cardinal (or a high enough Turing degree), and the ability to choose the placement of X at limit steps corresponds to being unbounded. However, the second player (not being able to move at limit steps) cannot independently prevent the game from ending too soon, and instead the first player certifies existence of enough Woodin cardinals (in a resulting model) through a $(Σ^2_1)^{uB}$ fact.
We can (presumably) go further by, at each limit step, permitting the first player skip the first move in exchange for a reasonable compensation (example: in Connect6, moves place two stones, except that the opening move of the player moving first places one stone).
A higher complexity, beyond even games with continuously coded length, is obtained by alternating infinite time Turing machines. A potential example is the game of Go, where capturing a location cofinally often makes it empty, and the objective is modified to, for example, controlling a given area.
Other infinite games
Chess
In infinite chess, every win occurs after a finite number of moves, but because the opponent (Black) can have an infinite number of choices where to move, the game tree for a forced win can be infinite (but well-founded). For positions with infinitely many pieces (with positions encoded by real numbers or subsets of $ω$), existence of a forced win is $Π^1_1$-complete. See the Checkmate in ω moves question and its Matthew Bolan's answer. I expect that existence of a forced win is $Π^1_1$-complete (as a set of integers) even for positions (on the infinite board) with $O(1)$ pieces.
However, if Black has only short-range pieces (perhaps infinitely many) and can skip moves (i.e. has a null move), then existence of a White win is $Σ^0_1$, and the win can be accomplished in a bounded number of moves. The reason is that, by induction on $n$, for every mate in $n$, there is a finite subset of the board that certifies the win. After making a move, White need only consider the null response and the responses that change the pieces on the subset of the board that certifies that the null response is a loss; and by the same argument, mate in $ω$ moves is some mate in $n$.
Games with compound moves: In some games, a move consists of a potentially unbounded number of submoves, which can be infinite in infinite positions. For example, in checkers a move can have an arbitrarily long chain of captures, and for an infinite chain, we can specify that the capturing piece is removed as well. For such games, even with all wins having a finite number of moves, the game tree for a forced win may need an uncountable ordinal rank. The complexity can now go beyond second order arithmetic, but the set of winning positions is still $Σ_1^{(L_δ(ℝ), ∈, ℝ)}$, where $δ$ is the least ordinal admissible to the reals.
5-in-a-row without O wins / Maker-Breaker games: In 5-in-a-row, all marks are permanent, so we can naturally speak of the position after an infinite number of moves. However, if five-in-a-row Os do not count as a win for the second player, then it is a Maker-Breaker game with finitely sized sets to make. In such games, all Maker wins (allowing transfinite wins) can be made finite, and certified by a finite subset of the board. By induction on finite $n$, a win in $n$ moves is certified by a finite set. Next, existence of a win in a finite number moves implies a win in a bounded number of moves (one need only consider responses in a region that certifies that skipping the turn would be a loss). Finally, if at a limit ordinal time, a finite region $S$ certifies a win in $n$, then since the position on $S$ was unchanged from an earlier time, the first player missed an earlier win. (Also, for a win in $n$ moves ($2n$ plies), $S$ need only have $< 2^{2^n}$ unfilled points, and in a metric where the sets to make have diameter $O(1)$, it only needs $O(2^n)$ diameter.)
Non-transfinite 5-in-a-row: Existence of a win should be $Π^1_1$-complete for infinite positions, and plausibly $Π^1_1$-complete for finite positions as well. A possible construction for finite positions is that at certain points O is forced to play far from the main 'computer' (as its only potentially saving threat), and X is forced to play near the O, and then the distance to the O X is measured, and the numbers from the measurements are used to test whether the chosen relation is well-founded.
