((λa.(λb.(λc.D) C) B) A)Consider program D that requires A, B & C which them selves stand alone:

((λabc.D) A B C)Recall that functions i, d, z, H and K are primordial.

Here we do some arithmetic Church’s way:

((λYS.(λrpamP. (p(P(r6)(r3))); Client on this line ) (Y(λrn.zn(λd.H)(λD.S(r(dn)))i)) ; r (read; native integers to Church) (λn.ni0) ; p (write; Church integers to native) (λxy.xSy) ; a, add (λxyz.x(yz)) ; m, multiply (λxy.yx) ; P, power ) (λf.(λx.f(λy.xxy))(λx.f(λy.xxy))) ; Y combinator (λnfx.f(nfx)) ; S (Church number successor) )The above expression yields 6

(p(a(r6)(r3))) ; -> 6+3 = 9

(p(m(r6)(r3))) ; -> 6*3 = 18

(p(P(r6)(r3))) ; -> 6

(p(P(r0)(r0))) ; -> 0

All of this development of arithmetic is within the bald language with Church’s abbreviations; the native arithmetic is relegated solely to input/output. It is notable that each of the three functions add, multiply and power stand alone as short expressions with no infrastructure beyond S, the successor function. Recursion is normally used in defining arithmetic but here is is only for the definition of r which converts to Church numbers.

To get this far starting with set theory takes many pages of ideas solely in support of arithmetic. Further I know no how-to (computational) version of arithmetic based on set theory, but I suspect that such is possible.