 The foundational discussion concerning extended “constructive” viewpoints is taken up in  section 4.  There, and throughout our paper the concepts of “proof-theoretic reducibility” and “proof-theoretic equivalence” will play a central role. The connection between PA and HA is paradigmatic and leads to the notion of proof-theoretic reduction. Before we can furnish a precise definition, we should perhaps stress that many concepts can be expressed in the language of PRA (as well as PA) via coding, also known as Gödel numbering. Any finite object such as a string of symbols or an array of symbols can be coded via a single natural number in such a way that the string or array can be retrieved from the number when we know how the coding is done. Typical finite objects include formulae in a given language and also proofs in a theory. Talk about formulae or proofs can then be replaced by talking about predicates of numbers that single out the codes of formulae and proofs, respectively. We then say that the concepts of formula and proof have been arithmetized and thereby rendered expressible in the language of PRA.