 The advantage of this type of formalism is that it not only affirms the meaningfulness, the possession of sense, of mathematical utterances; in sharp contrast with traditional game formalism, it holds that such utterances have truth values, where proofs or refutations exist. The problem of the metatheory is met if one can give, after the fashion of Goodman and Quine 1947, a non-mathematical account of concrete proof. Of course, as noted above, severe problems remain. The problem of applicability has to be met, by providing conservative extension proofs for example. And of course the theory is threatened not only by Gödel—type incompleteness and the undecidable—but intuitively truth-valued– sentences it throws up; even more devastating indeterminacy looms in the form of ‘concretely undecidable’ sentences such as Tennant’s primality claim of section 5. 