Games in non-standard models Has anyone studied Combinatorial game theory in non-standard models?
In particular, we can work in either non-standard models of set theory, or we can work in non-standard models of arithmetic, where $l$ and $r$ are binary predicates representing Left and Rights moves.
In particular, I think that studying Sylver coinage in non-standard models of PA would be interesting.
 A: There are Paris-Kirby games, there is the Hydra game, there is a theory of ordinal semi-invariants in combinatorial game theory, there are Diophantine games by Jones which behave differently in different models of arithmetic, Hales-Jewett (provable, but metamathematically relevant) was first formulated as generalized noughts and crosses, there are Clote games in models of arithmetic, there are Ramsey, Schur and van-der-Waerden games, the games paradigm is dominant throughout the subject.
Now the Axiom of Determinacy and its fragments, all behaving differently in various models of second-order arithmetic or set theory.
There are games throughout Descriptive Set Theory (see Kechris's monumental monograph), there are games for indiscernibles and games for sharps, games to build an ultrafilter (which will give a model). 
Most classical recursion theory can be cast in the language of games, since Lachlan and Rabin. (See also Kummer.)
Often, to build a nonstandard model you have a game between two players: one tries to build a branch in a tree, the other one tries to block all possible branches by some obstacles: minors or indiscernibles.
See also Hodges "Building models by games".
Recursive saturation and simply Completeness Theorem can be cast as games and it depends on formal Consistency held or not held in your ground model -- which player will have a winning strategy.
There are games to avoid arithmetical progressions (but these have not yet been connected to models of arithmetic, possibly for some Erdos-Turan reasons).
About simpler games, like in Conway's book -- check out Thomas Forster's ordinal-analysis of Nim.
There is a lot of literature about finite perfect-information games without an algorithm of a winning strategy. (See J. Jones).
I have some examples of games without a PA- or a PRA- provably winning strategy (so they will behave differently in different models of arithmetic). Also I have a curious example of a game without a PA-provably winning strategy for either player, but ANY (of the infinitely-many possibilities) move of the First Player puts him in a losing position.
Nash-Williams theory can be cast in terms of games, and it builds a model of ATR_0.
Speaking of ATR_0, there are games of length: who can build a longer well-ordering.
There are Ehrenfeucht-Fraissé games and back-and-forth games.
Many forcing constructions are games.
This is just a fraction of things, what just crossed my mind now.
Sylver Coinage as it is may disappoint you, but it is ready for interesting modifications that can become very metamathematically-sensitive.
