 However Frege lays down very stiff challenges even for a rigorous game formalist fully equipped with the techniques and results of metamathematics. Such a theorist gives us a characterisation of a language, for example by setting out what the basic elements are—primitive symbols, and strings thereof—and then gives a recursive specification of which strings count as well-formed. Similarly we will be given a rigorous specification of which arrangements of well-formed formulae count as proofs in a given system, and of what theorem they prove in each case. If strings such as ‘\(3+1=0\)’ or ‘\(3 \gt 2\)’ come out as provable in the system (arithmetic modulo 4, say) then that is enough to count them as correct utterances of the system. No further issue of truth need arise; nor do we need to assume that there is only one system for a given set of symbols. Nor, furthermore, need we assume that each such system is complete (though Frege took Thomae to task for the incompleteness, massive though readily rectifiable, of his arithmetic calculus). We need make no assumption that the numerals in these strings refer to anything outside the system, indeed we need not assume they refer to anything at all. (This game formalist, then, is not subject to the objection that ‘3 \(\gt  2\)’ should come out as false, on any legitimate formalist reading of ‘\(\gt\)’; no need to think of the numerals as referring to concrete marks and ‘\(\gt\)’ meaning physically greater in size.)