 Kripke has shown that KS implies the existence of nonrecursive functions, a result not published by him but by Kreisel (1970). Clearly, this implies that the theory CS also implies the existence of a nonrecursive function. A possible argument for CS runs as follows. Suppose \(X\) is a noncomputable but computably enumerable set and define the function \(f\) as follows: