Is there a game semantical countermodel to Markov's Principle?

112 Views Asked by At

For specificity, let's fix Markov's Principle as $$\forall P : \mathbb N \to 2. \neg(\forall n : \mathbb N. P(n) = 0) \to \exists m : \mathbb N. P(m) = 1.$$ I've seen an informal argument that this should be invalid for an interpretation of $P$ as ranging over choice sequences in an environment where the sequence is being chosen maliciously; framed game-semantically, Opponent could continually extend the sequence with $0$s to an arbitrary length, preventing verification of the $\exists$, but immediately insert a $1$ should Player try to refute the $\neg\forall$ premise. (Of course, this would hinge on Player not being able to subsequently go back and win by verifying the conclusion with the newly-inserted $1$, which does seem problematic since I guess it would suggest an additive interpretation of the $\to$ in the body?)

Is there some formal construction which captures this concept?