Second-order Arithmetic - Definable Functions of Second-order Arithmetic

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:

    Those things which now most engage the attention of men, as politics and the daily routine, are, it is true, vital functions of human society, but should be unconsciously performed, like the corresponding functions of the physical body.
    Henry David Thoreau (1817–1862)

    Your discovery of the contradiction caused me the greatest surprise and, I would almost say, consternation, since it has shaken the basis on which I intended to build my arithmetic.... It is all the more serious since, with the loss of my rule V, not only the foundations of my arithmetic, but also the sole possible foundations of arithmetic seem to vanish.
    Gottlob Frege (1848–1925)