 The problem this raises for the formalist is this: the metatheory is itself a substantial piece of mathematics, ostensibly committed to an infinite realm of objects which are not, on the face of it, concrete. Tokens of the expressions of the object language game calculus may be finite—ink marks and the like; but since there are infinitely many expressions, theorems and proofs, these themselves must be taken to be abstract types. At best, the formalist can achieve no more than a reduction in commitment from the transfinite realms of some mathematical theories, such as set theory, to the countably infinite, but still presumably abstract, realm of arithmetic, wherein the syntax and proof theory of standard countable languages such as those of standard set theory, can, as Gödel showed, be modelled.