 We now recall the power set axiom of classical set theory: if \(X\) is a set, then so is its power set  \[ \textrm{sb}(X)≡ \{S: S \subset X\}. \]  Since this definition is impredicative, most constructive mathematicians hesitate to regard \(\textrm{sb}(X)\) as a set. What they normally use, and we shall adopt, as the constructive replacement for the power set axiom is the axiom of exponentiation : If \(A\) and \(B\) are sets, then so is the set of all mappings from \(A\) into \(B\). In particular, the class \(2^{\bN}\) of all binary sequences is a set. 