 The method we have described revolves almost entirely around removing existential quantifiers from the beginnings of formulas; so it is known as the method of quantifier elimination. It is not as far as you might think from the two standard definitions. In all cases Tarski assigns to each formula, by induction on the complexity of formulas, a description of the class of assignments that satisfy the formula. In the two previous truth definitions this class is described directly; in the quantifier elimination case it is described in terms of a boolean combination of formulas of a simple kind.