 Evaluation games There are well-known two-player games for evaluating a first-order formula \(\varphi\) within a given logical model. These games are played between Verifier and Falsifier, who can both test atomic assertions, and specify the value of variables from a given domain (Hintikka 1973). The schedule of the game is determined from the syntactic structure of the formula \(\varphi\). Disjunctions and existential quantifiers require choices of the Verifier, conjunctions and universal quantifiers of the Falsifier, and negations trigger a role switch between the two players. The result is the following match between winning strategies and the ordinary semantic notion of truth: