Even before we do the fancy stuff to define the ‘reals’ in ACA0, we twice over have to use pair-codings (i.e. use natural numbers as codes for pairs of naturals) to construct first the integers and then a rational field. Is that bad news? Does that make even those initial constructions unacceptably artificial?
Well, on reflection, it is not easy to see how anyone who is happy with more standard set-theoretic constructions of number systems can really press this complaint. For they are equally committed to essentially parallel artificial coding tricks.
Recall, for a start, the way ordered pairs are usually handled in a set theoretic framework. Sets with the same members are identical — that is arguably analytic of the very notion of a set. But two ordered pairs with the same members in the opposite order are not identical, so ordered pairs aren’t sets, and that is analytic of the very notion of an ordered pair. So it is plain that we shouldn’t, strictly speaking, identify an ordered pair with its Kuratowski reduction, for that set is never ordered and indeed is often not a pair either. But — of course! — the Kuratowski reduction has the property of real ordered pairs that that matters. So we’ve all learnt to use Kuratowski unordered sets as proxies for ordered sets. And this trick works so smoothly that we soon fall into the habit of saying that ordered pairs are sets of sets, keeping more cautious talk of proxies (or representations, or codes) for when we are on our Sunday best behaviour.
Likewise, we standardly learn to say that rationals, for example, are equivalence classes of ordered pairs of equivalence classes of ordered pairs of natural numbers, keeping proxy talk for Sundays. But it is no more and no less true that rationals are sets of sets of sets of sets of sets of sets of numbers than that they are numbers coding for pairs of pair-codes. Either both claims should be rejected; or both claims should be endorsed, each relative to its proprietary modeling scheme for representing the rationals (and then we will no doubt be tempted to go structuralist about ‘the rationals themselves’ — it’s in some sense what is shared by the various schemes that matters). What wouldn’t seem defensible is any suggestion that the standard set-theoretic coding of the rationals gets it fundamentally right (whatever ‘it’ precisely might be) while the arithmetic coding available in Peano Arithmetic and hence ACA0 gets it wrong.
‘Still,’ it might be protested, ‘surely the familiar set-based construction is compelling in a way that using number-codes isn’t. Surely, for example, rationals are ratios of pairs of numbers, and it is much more natural to have the relevant pairs of numbers there, in some sense in the construction, rather than just being pointed to by some essentially arbitrary coding device.’
However, this line of thought is definitely resistable. For a start, thinking of elements as being present in the sets of which they are members is highly misleading. Some might be tempted, perhaps, to think of the numbers 1, 2 as being ‘in’ the set {1,2} in something like the sense in which the numerals ‘1’, ‘2’ do indeed feature in the name of the set ‘{1,2}’ — as if, metaphysically, all we have to do is remove from around the members the lasso which pulls them into a set, to be left with the naked members themselves. But that is a quite hopeless picture, confusing parthood with set-membership. Much better to think of sets in more category-theoretical terms, as being entities that come equipped with a bunch of special ‘arrows’ out, with the arrows mapping the set to its several members. And what makes the entities in question just sets is that this is all there is to be said about them — they are abstract entities whose only feature is to have those ‘arrows’ out, their only role is to thereby enable us to treat many objects together as one.
Looked at that way, the difference between a set-theoretic construction and a coding-by-numbers construction comes down to this. In the first case, we are introducing new entities whose sole role is to enable us to point to two or more numbers taken together; while in the second case, we are making use of what we already have, i.e. numbers, to enable us to point to pairs of numbers taken together. But now remember again that, in the standard set-theoretic construction of ordered pairs, we do put a considerable premium on using what we have around already, namely unordered sets, rather than introducing ordered pairs as new primitives governed by their own laws (as Russell and Whitehead did). Analogously, when constructing the integers and rationals, why shouldn’t we put a premium on using what we already have around while we can, and so use numbers to point to pairs of numbers rather than introduce new entities to do the job?
There more to be said about set-theoretic constructions. But at least initially, we can insist that, while the set-construction of the integers and the rationals may win over the number-code construction in ACA0 on grounds of sheer familiarity, there is no very obvious sense in which it is intrinsically preferable.