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:
“If photography is allowed to stand in for art in some of its functions it will soon supplant or corrupt it completely thanks to the natural support it will find in the stupidity of the multitude. It must return to its real task, which is to be the servant of the sciences and the arts, but the very humble servant, like printing and shorthand which have neither created nor supplanted literature.”
—Charles Baudelaire (1821–1867)
“‘Tis no extravagant arithmetic to say, that for every ten jokes,—thou hast got an hundred enemies; and till thou hast gone on, and raised a swarm of wasps about thine ears, and art half stung to death by them, thou wilt never be convinced it is so.”
—Laurence Sterne (1713–1768)