Definable Functions of Second-order Arithmetic
The first-order functions that are provably total in second-order arithmetic are precisely the same as those representable in system F (Girard et al., 1987, pp. 122–123). Almost equivalently, system F is the theory of functionals corresponding to second-order arithmetic in a manner parallel to how Gödel's system T corresponds to first-order arithmetic in the Dialectica interpretation.
Read more about this topic: Second-order Arithmetic
Famous quotes containing the words functions and/or arithmetic:
“Let us stop being afraid. Of our own thoughts, our own minds. Of madness, our own or others’. Stop being afraid of the mind itself, its astonishing functions and fandangos, its complications and simplifications, the wonderful operation of its machinery—more wonderful because it is not machinery at all or predictable.”
—Kate Millett (b. 1934)
“O! O! another stroke! that makes the third.
He stabs me to the heart against my wish.
If that be so, thy state of health is poor;
But thine arithmetic is quite correct.”
—A.E. (Alfred Edward)