This calculus is very expressive. Still it enjoys normalisation, actually strong normalisation, and many functions are definable in this calculus. Actually all functions provably total in second order arithmetic, which is a very large class of functions. It is so powerful that even connectives are definable in this calculus starting from just implication and quantification. For instance, we may define the logical conjunction in this way.

---