Abstract

By , we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. is defined to be plus weak König's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. In this paper, we first show that for any countable model M of , there exists a countable model M′ of whose first-order part is the same as that of M, and whose second-order part consists of the M-recursive sets and sets not in the second-order part of M. By combining this fact with a certain forcing argument over universal trees, we obtain the following result : if proves X!Y with arithmetical, so does . We also discuss several improvements of this results