 Idealisation, then, is essential in metamathematics, including the idealised notions of truth and proof found in metamathematics. If the formalist is entitled to assert there are infinitely many primes, whilst denying abstract objects exist, there seems no reason why she cannot affirm that there are infinitely many formulae or infinitely many proofs, whilst also denying that abstract objects exist. Weir (2016: 38–39) therefore argues that the formalist can answer the problem of concrete undecidables so long as there are concrete proofs (or proof sketches) of results to the effect that formal truth, for a given language or sub-language, coincides with formal provability, and that there is no reason to restrict idealisation for finitary languages. 