The abstract type of the real numbers (Q2238151)

The author provides an axiomatization for finite type arithmetic appending an abstract type for the real numbers. Typically, finite type arithmetic encodes reals with rapidly converging Cauchy sequences of rationals. The introduction of the abstract type sidesteps this translation. The principles associated with the added type facilitate applications of the bounded functional interpretation as described in the appendix. For more detail on abstract types within the bounded functional interpretation see the work of [\textit{P. Engrácia} and \textit{F. Ferreira}, Landsc. Log. 1, 87--112 (2020; Zbl 1505.03126)].