 Game-theoretical vs. Tarskian semantics of FO. The set of formulas of \(\mathbf{FO}\) is a proper subset of the set of \(\mathbf{IFL}\) formulas. The standard semantics of \(\mathbf{FO}\) is not the one provided by GTS, but the Tarskian semantics specifying recursively the satisfaction relation \(M, g \vDash \phi\). If the Axiom of Choice is  assumed,[34]  the two semantics of \(\mathbf{FO}\) coincide: