Infinite games: are they well defined? It is just my curiosity about this question where we have an infinite game and (according to the answers) winning strategies for both players. I am familiar with terminating games only, and I am pretty sure that nonterminating ones can cause many paradoxes. As this is a community wiki mode, I would be happy to see formal definitions, existence of wining strategies as well as possible collisions.
Thanks in advance for keeping my mind finite!
 A: I'm aware of quite a number of theories of "games" in mathematics. A not-overly-naive preliminary is to ask about what these are, and then what they have in common. 
I think the earliest is probably the Polish (Banach-Mazur) type, which have already been defined. "Game theory'' as in von Neumann-Morgenstern is another, important for economists. Combinatorial Game Theory (CGT) is another, with its distinctive ending rule. And then there is the use of "game semantics" in computer science.
The game-like aspect is certainly to do with quantifiers. What mathematicians would recognise as "uniformity" (there exists ... such that for all ...) is to be iterated. My winning is stated in the form "I have a play such that for all plays you make (I have a play such that for all plays you make (...))". This is the typical game quantifier G, and what matters is what happens to the ... . It happens to be true, for example, that any chess game is decided by the time 10,000-ply has been played, so for chess G is a simple iteration, not some sort of "fixed point" construction. 
Examples from logic I think largely fall into the "Polish" style of game. That is to judge by the Hodges book on model theory. In CGT there is a no particular distinction between finitary and infinitary games. Whichever theory is being spoken about, you need to explain carefully what the winning or ending condition is, and quite what you mean by a "strategy" (recall that G is sort of non-constructive, being existential in nature). 
A: The Axiom of Choice implies that there exist infinite games in which neither player has a winning strategy.  Thus, the Axiom of Choice is incompatible with the Axiom of Determinacy.  An example of a game where neither player has a winning strategy is the following (caveat: I'm not a set-theorist).
The game is a subset $G \subset [0,1]$ of real numbers.  At stage 1, player 1 chooses a bit which is either 0 or 1.  At stage 2, player 2 (knowing player 1's choices so far) chooses another bit.  The players then repeat.  After $\omega$ steps, they have constructed a real number $g \in [0,1]$ where the odd bits of $g$ (in binary) are given by player 1's choices and the even bits of $g$ are given by player 2's choices.  Player 1 wins if $g \in G$, and player 2 wins if $g \notin G$.  
Regarding the question that inspired the question, I've had a look at the paper (it's available on Springerlink).  I'm convinced that $L$ does have a winning strategy.  So, that particular game is determined.  
A: In recent years, a relatively abstract and general formulation of extensive form games has been developed by Carlos Alos-Ferrer and Klaus Ritzberger. The formulation is general enough to discuss when some useful properties hold- and when they fail. In particular, in Trees and Extensive Forms (WP version can be found here here), they give necessary and sufficient conditions for when every pure strategy in an extensive game induces an outcome and when this outcome is unique.  
A: A relatively general definition of an infinite, discrete "Gale–Stewart game" is the one used in Martin's proof of Borel determinacy [1]. More information about this type of game can be found in Kechris's Classical Descriptive Set Theory and in Jech's Set Theory. 
Definition. We define a game $G(X,P)$ based on a nonempty set $X$ and a set $P \subseteq X^\omega$. The elements of $X$ are the moves of the game. A play of the game is a sequence $r = (r_0, r_1, r_2, \ldots)$. If $r \in P$ then we say that player I wins, otherwise we say that player II wins. Hence every play of the game has a winner. The informal interpretation of this game is as follows: player I chooses $r_0$, then player II chooses $r_1$, then player I chooses $r_2$, etc. 
The way that the game is played is formally specified by the definition of a winning strategy. In the game $G(X,P)$, a strategy is just a function $s \colon \left ( \bigcup_{i \in \omega}X^i \right )  \to X$. Intuitively, the value of $s(\tau)$ is the move that should be played if the other player's moves up this this point are listed in the sequence $\tau$. 
A winning strategy for player I is a function $f \colon \left ( \bigcup_{i\in\omega} X^{i} \right )  \to X$ such that player I wins any play of the form 
$$
f(\langle \rangle),\: r_1, f(\langle r_1\rangle),\: r_3, f(\langle r_1, r_3\rangle), \ldots
$$
A winning strategy for player II is a function $g \colon \left ( \bigcup_{i\in\omega} X^{i+1} \right )  \to X$ such that player II wins any play of the form 
$$
r_0, \: g(\langle r_0\rangle),\: r_2,\: g(\langle r_0, r_2\rangle),\: r_4, g(\langle r_0, r_2, r_4 \rangle),\ldots
$$

This set of definitions leads to a well-defined, non-paradoxical collection of games. It is impossible for both players to have a winning strategy for the same game, because the strategies can be played against each other.  However, it is possible for neither player to have a winning strategy, and in fact ZFC proves that in the specific case $X = \{0,1\}$ there is a set $P \subseteq \{0,1\}^\omega$ for which neither player has a winning strategy. 
Donald Martin proved the Borel determinacy theorem in 1975: if $X$ is any nonempty set whatsoever and $P$ is a Borel subset of $X^\omega$ then one of the players has a winning strategy for $G(X,P)$. Here $X$ has the discrete topology and $X^\omega$ has the product topology. 
The axiom of determinacy states that if $P$ is any subset of $\{ 0,1 \}^\omega$ then one of the players has a winning strategy in $G(\{0,1\}, P)$. This is inconsistent with ZFC but is consistent with ZF plus dependent choice. 
The paper that Andres Caicedo  gave above [2] studies an entirely different type of game, which is continuous rather than discrete. 
1: http://en.wikipedia.org/wiki/Borel_determinacy_theorem
2: http://arxiv.org/abs/0909.2524
