 Gödel defines a book-keeping device, a well-ordering of all tuples of variables arising from a need to satisfy φ as dictated by (Q). For example, if (Q)φ is ∀x0∃x1ψ(x0, x1), we list the quantifier-free formulas ψ(xn, xn+1). (Or more precisely, finite conjunctions of these in increasing length. See below.) Then in any domain consisting of the values of the different xn, in which each ψ(xn, xn+1) is true, the sentence (Q)φ is clearly true. A crucial lemma claims the provability, for each k, of the formula (Q)φ → (Qk)φk, where the quantifier free formula φk asserts the truth of ψ for all tuples up to the kth tuple of variables arising from (Q), and (Qk)φk is the existential closure of φk. (See the example below where the definition of the φk′s is given.) This lemma is the main step missing from the various earlier attempts at the proof due to Löwenheim and Skolem, and, in the context of the completeness theorem for first order logic, renders the connection between syntax and semantics completely explicit.