Combinatorial game theory plays a role in logic and computer science as in, for example, the Ehrenfeucht-fraïssé game, which is a logic game played on model-theoretic structures. At each turn, the first player chooses an element from one of the two structures, and the second has to chose an element from the other, trying to maintain a local isomorphisms between the elements chosen up to that point.

The main theorem regarding this game roughly says that if Player 2 has a winning strategy in a game over two structures, then there does not exist a first-order logic formula that differentiate the two structures.

This result is used in a large number of expressibility results for first order logic and for other logics as well (there's notably an extension of the theorem to monadic second-order logic).

These expressiveness results in turn have strong applications in computer science, e.g. to formal verification, database theory, etc...

Combinatorial game theory plays a role in logic and computer science as in, for example, the Ehrenfeucht-fraïssé game, which is a logic game played on model-theoretic structures. At each turn, the first player chooses an element from one of the two structures, and the second has to chose an element from the other, trying to maintain a local isomorphisms between the elements chosen up to that point.

The main theorem regarding this game roughly says that if Player 2 has a winning strategy in a game over two structures, then there does not exist a first-order logic formula that differentiate the two structures.

This result is used in a large number of expressibility results for first order logic and for other logics as well (there's notably an extension of the theorem to monadic second-order logic).

These expressiveness results in turn have strong applications in computer science, e.g. to formal verification, database theory, etc...