Defining functions in second-order arithmetic

Question

In ZF, a function is a special kind of set, namely a set of ordered pairs where no two pairs have the same first component but different second components. How are functions defined in SOA? Are functions in SOA special kinds of natural numbers (or maybe special subsets of natural numbers)? I know in SOA you already have some "primitive" functions, namely the successor function and addition/multiplication, but it is not clear to me how to compose them to form other functions. My guess is that the comprehension axiom is used to define more complicated functions. Is this correct?

Answer 1

There are two basic approaches to second-order arithmetic: the "set-based" approach and the "function-based" approach.

In the "set-based" approach, the objects in second-order arithmetic are numbers and sets of numbers. There is a definable pairing function which allows us to code pairs of numbers into single numbers. Using this, we can represent functions as sets of (coded) ordered pairs of numbers, that is, a function is identified with its graph. There are no function variables, and the only function constants are the addition and multiplication operations. There are variables that range over sets of numbers, but no constant set symbols and no term-forming operations for sets.

In this "set-based" setting, to define the function $(\lambda x)(x+2)$, assuming $\langle a,b\rangle $ is the pairing function, we use this comprehension axiom: $$ (\exists X)(\forall n)[n \in X \leftrightarrow (\exists a)(\exists b)(b = a + 1 + 1 \land \langle a,b\rangle = n)]$$ The resulting set $X$ is the graph of the desired function.

In the "function-based" approach, the fundamental objects are numbers and unary functions from numbers to numbers - sets are no longer basic objects, and there are no set variables any more, just function terms and function variables. In this setting, we do have additional term forming operations (combinators), such as $\lambda$ abstraction. We can define $(\lambda x)(x+2)$ as, well, $(\lambda x)(x + 1 + 1)$, which is a formula of second-order arithmetic in this setting.

Each of the set-based and function-based approaches is interpretable in the other, using the axioms for each kind of second-order arithmetic, and so for many purposes it doesn't matter which one is used. However, for various reasons, proof theory and intuitionistic second-order arithmetic often use the function-based approach, while classical Reverse Mathematics usually uses the set-based approach.

It is worth pointing out that "general" second-order logic has quantifiers over not only over sets (unary relations) and over unary functions, but also over $k$-adic relations and $k$-ary functions for all $k \in \omega$. In the context of second-order arithmetic, we generally ignore this generality, because we have a definable pairing function already, which allows us to encode higher arities into unary relations and functions.

Here are some references. The set-based version is described in Stephen G. Simpson's book Subsystems of Second Order Arithmetic. The function-based version is described in Ulrich Kohlenbach's book Applied Proof Theory (and in other proof theory books that are less accessible). Kohlenbach writes something about the interpretation of each into the other in his paper "Higher-Order Reverse Mathematics", but not much, as it's an easy exercise. Stewart Shapiro's book ''Foundations Without Foundationalism'' is about second-order logic more generally, but not particularly about second-order arithmetic. None of these is really accessible below the graduate level; there is no good undergraduate-level reference on second-order arithmetic that I know of, although some logic textbooks have brief descriptions of second-order logic.