 Forcing games are also known to descriptive set theorists as Banach-Mazur games; see the references by Kechris or Oxtoby below for more details of the mathematical background. Model theorists use them as a way of building infinite structures with controlled properties. In the simplest case \(\forall\) and \(\exists\) play a so-called Model Existence Game, where \(\exists\) claims that a fixed sentence \(\phi\) has a model while \(\forall\) claims that he can derive a contradiction from \(\phi\). In the beginning a countably infinite set \(C\) of new constant symbols \(a_0, a_1, a_2\) etc is fixed. \(\exists\) defends a disjunction by choosing one disjunct, and an existential statement by choosing a constant from \(C\) as a witness. \(\forall\) can challenge a conjunction by choosing either conjunct, and a universal statement by choosing an arbitrary witness from \(C\). \(\exists\) wins if no contradicting atomic sentences are played. \(\exists\) has a winning strategy (a Consistency Property is one way of describing a winning strategy) if and only if \(\phi\) has a model. On the other hand, if \(\forall\) has a winning strategy, the tree (which can be made finite) of all plays against his winning strategy is related to a Gentzen style proof of the negation of \(\phi\). This method of analysing sentences is closely related to Beth’s method of semantic tableaux and the Dialogical Game (see Section 8).