 The proof we will outline is sensitive to the particular concept we use for the length of a proof. Another possibility, and the one that Gödel has in mind, is the number of formulas in the proof. Buss (see below) proves the theorem in either case, so both cases are resolved.