Higher Order Reverse Mathematics

Abstract

In this paper we argue for an extension of the second order frame-work currently used in the program of reverse mathematics to finite types. In particular we propose a conservative finite type extension RCA^omega_0 of the second order base system RCA_0. By this conservation nothing is lost for second order statements if we reason in RCA^omega_0 in stead of RCA_0. However, the presence of finite types allows to treat various analytical notions in a rather direct way, compared to the encodings needed in RCA_0 which are not always provably faithful in RCA_0. Moreover, the language of finite types allows to treat many more principles and gives rise to interesting extensions of the existing scheme of reverse mathematics. We indicate this by showing that the class of principles equivalent (over RCA^omega_0 ) to Feferman's nonconstructive mu-operator forms a mathematically rich and very robust class. This is closely related to a phenomenon in higher type recursion theory known as Grilliot's trick.