Games with 1-backtracking (Q636360)

The authors define 1-backtracking for games, allowing either player to correct any previous move a finite number of times. This corresponds to simple backtracking in earlier work of \textit{T. Coquand} [``A semantics of evidence for classical arithmetic'', J. Symb. Log. 60, No. 1, 325--337 (1995; Zbl 0829.03037)]. Given a game \(G\), bck\((G)\) denotes an associated game allowing 1-backtracking. The central results of the paper show that a player \(p\) has a winning strategy for \(G\) computable from \(\mathbf 0^\prime\) if and only if \(p\) has a computable winning strategy for bck\((G)\). Games of the form bck\((G)\) are a sound and complete semantics for Limit Computable Mathematics as formulated by \textit{S. Hayashi} [``Can proofs be animated by games?'', Fundam. Inform. 77, No. 4, 331--343 (2007; Zbl 1182.03067)]. Thus, this form of backtracking is useful for studying the constructive content of certain classical theorems.