Second-order Arithmetic - Coding Mathematics in Second-order Arithmetic

Coding Mathematics in Second-order Arithmetic

Second-order arithmetic allows us to speak directly (without coding) of natural numbers and sets of natural numbers. Pairs of natural numbers can be coded in the usual way as natural numbers, so arbitrary integers or rational numbers are first-class citizens in the same manner as natural numbers. Functions between these sets can be encoded as sets of pairs, and hence as subsets of the natural numbers, without difficulty. Real numbers can be defined as Cauchy sequences of rational numbers, but for technical reasons not discussed here, it is preferable (in the weak axiom systems above) to constrain the convergence rate (say by requiring that the distance between the n-th and (n+1)-th term be less than 2−n). These systems cannot speak of real functions, or subsets of the reals. Nevertheless, continuous real functions are legitimate objects of study, since they are defined by their values on the rationals. Moreover, a related trick makes it possible to speak of open subsets of the reals. Even Borel sets of reals can be coded in the language of second-order arithmetic, although doing so is a bit tricky.