Weir’s formalist account of arithmetic in headline form comes to this: the arithmetical claim P is correct just in case that there is (or in practice could be) a concrete proof of P. (We’ll stick to considering the arithmetical case.)
Weir needs proofs to be concrete: treating proofs as abstract objects wouldn’t at all chime with his naturalist worries about abstracta. He needs to allow the practical possibility of a concrete proof to suffice for truth, or else — for all he knows — there could be random gaps even among the simple computable truths about small numbers because no one has yet bothered to write down a computation. But the modality had better be not be an extravagant one (“in some possible world, however remote, where our counterparts can e.g. handle proofs with more steps than particles in the actual world, …”), or again we could be taking on modal commitments that are inimicable to Weir’s strong naturalism: so as we said, we need some notion of practical possibility here.
Are these concrete proofs particular tokens? If so, you and I always give different proofs. That wouldn’t tally with our ordinary ways of talking of proofs (when we talk of Euclid’s proof of the infinitude of primes, we don’t mean just some ancient token; when we say there is only one known proof of P we don’t mean that it has only been written down once). But Weir wants to avoid proof-types (or he is back with the unwanted abstracta); so he makes play with with a notion of a proof-tipe, where a tipe is a mereological sum of equiform tokens. Thus understood, a proof tipe is a scattered concrete thing, and you and I giving the same proof — to speak with the vulgar — is a matter of you and I producing tokens that are part of the same proof tipe. (Weir thinks that for his purposes he can get away with a lightweight mereological theory that doesn’t get tangled with issue about e.g. absolutely restricted principles of composition. Let’s give him that assumption. It will be the least of our worries.)
Now, concrete numerals and concrete proofs are few (even counting in practically possible ones as well). The obvious challenge to Weir’s position is that his formalism will therefore lead to some kind of finitist revisionism rather than conserving the arithmetic we know and love.
To press the point, take a concretely statable claim P that some very large number n is prime. Then it could well be that there is no practically possible concrete proof of either P or not-P in your favourite formal system S (the system whose concrete proofs, according to Weir, make for the correctness of arithmetical claims on your lips). Yet it is an elementary arithmetical claim that either P or not-P, a truth now seemingly without a formalist-approved truth-maker (given that Weir endorses a standard truth-functional account of the connectives). What to do?
Well at this point I struggle. The idea seems to be this. Here is our practice of producing concrete formal proofs in the system S. Like other bits of the world, we can theorize about this, doing some applied mathematics M which — like other bits of applied mathematics — purports to talk about some idealized mathematical model, in this case a model of the real-world practice of proving things in S. And now, we do have a concrete M-proof that, in the idealized model, the model’s representative for the concrete claim that either P or not-P. So,
the EXISTENCE [remember: small caps indicate talk-in-the-metaphysics room] of concrete indeterminables [like P] should not inhibit reasoners from applying excluded middle to them so long as THERE IS a concrete proof that, in a legimitate idealization, the image of the indeterminable is decidable in the formal sense. (TTP, p. 205)
But hold on! Setting aside worries about ‘legitimate’, what makes an arithmetical claim correct, on your lips, is by hypothesis the practical availability of a concrete proof in a formal game S [maybe different speakers are working in different games with appropriate mappings between them, but let’s not worry about that now]. So by hypothesis, a concrete proof in a different bit of mathematics M — a bit of applied mathematics about an idealized model of our arithmetical practice — just isn’t the sort of thing that can make an arithmetical claim correct. If we allow moves external to S to make-true arithmetical claims, then S isn’t after all the formal system proofs within which proofs provide correctness conditions for arithmetic.
So on the face of it, it looks as if Weir has simply cheated here by changing the rules of the formalist game midstream! And I’m evidently not alone in thinking this: John Burgess in his Philosophia Mathematica review finds himself baffled by the same passage. Weir himself recognizes that his readers might find the move here sticky. In one of his comments in the thread following my last blog post on his book, he writes
If we want to know whether a particular area is bivalent … we don’t ask whether for every token there is a token proof or disproof, we ask if there is a concrete proof of a formal negation-completeness result for the idealised theory. If so, we are allowed to lay down all instances of LEM for that sub-language as axioms … even if that means that some concretely provable theorems — t is prime or t is not prime say — have disjuncts which are neither concretely provable nor refutable. I suspect this get out of jail manoeuvre will prove one of the biggest sticking points in the reception of the book, but I’m still confident about its legitimacy!
Like Burgess, I can’t share Weir’s confidence.