 It’s puzzling that we have here two theories of when a sentence is true, and the theories are not equivalent if the axiom of choice fails. In fact the reason is not very deep. The axiom of choice is needed not because the Hintikka definition uses games, but because it assumes that strategies are deterministic, i.e. that they are single-valued functions giving the user no choice of options. A more natural way of translating the Tarski definition into game terms is to use nondeterministic strategies, sometimes called quasistrategies (see Kolaitis 1985 for details). (However, Hintikka 1996 insists that the correct explication of ‘true’ is the one using deterministic strategies, and that this fact vindicates the axiom of choice.)