 More technically, the elements of the structure \(A\) are fixed in advance, say as \(a_0, a_1, a_2\) etc., but the properties of these elements have to be settled by the play. Each player moves by throwing in a set of atomic or negated atomic statements about the elements, subject only to the condition that the set consisting of all the statements thrown in so far must be consistent with a fixed set of axioms written down before the game. (So throwing in a negated atomic sentence \(\neg \phi\) has the effect of preventing any player from adding \(\phi\) at a later stage.) At the end of the joint play, the set of atomic sentences thrown in has a canonical model, and this is the structure \(A\); there are ways of ensuring that it is a model of the fixed set of axioms. A possible property P of \(A\) is said to be enforceable if a builder who is given the task of making P true of \(A\) has a winning strategy. A central point (due essentially to Ehrenfeucht) is that the conjunction of a countably infinite set of enforceable properties is again enforceable.