Extensionality and choice in constructive mathematics
Michael J. Beeson · Pacific Journal of Mathematics · 1980
ion. Suppose A is a set, with S(A, A'). Then {{xeA:φ(xf y)}:yeA} , for a z/o-formula φ, can be formed by elementary comprehension, as Q = {{xe A: φ'(x, y, Y', A, A')}: ye A}, where φ' is the formula constructed in verifying the separation axiom, and Y' = { , b) e W & (x, c) e W -*h(x, b) = h(x, c))}. This also can be done with elementary comprehension. Now we claim that X is the set of functions from A to B. First, if / e l , then / is (the graph of) a function from A to B, by the second clause in the definition of X Secondly, if F is a function from A to B, fix W as in CAC', then F arises as H(h), where h is the choice function given by CAC. (More precisely, a function with the same values as F arises as H(h)> which is good enough.) Thus the set of functions from A to B is a classification; but it is easy to define its transitive closure in terms of the transitive closures of A and B. Hence it is a set. Finally, we need to say something about the assertion that φ° is equivalent to for arithmetic. In B, sentences are built up from a constant for zero, a constant for successor, but no symbols for plus and times; while in FQ, there are application terms for plus, times, and successor. We have left implicit that in defining φ zero should be interpreted as zero, and the successor should be interpreted as the graph of the successor function in Fo. We then prove in Fo that the graphs of plus and times satisfy the interpretations of the defining formulae for plus and times in set theory (which say that plus and times satisfy certain recursion relations). We also prove that if any classification satisfies these defining formulae, then it is the graph of plus (or times, as the case may be). This takes care of the basis case of an easy induction on the complexity of arithmetic formulae φ. This completes the proof of