Higher Order Reverse Mathematics

Ulrich Kohlenbach

December 2000

Abstract:

In this paper we argue for an extension of the second order framework 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$ instead 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 non-constructive $\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

Available as PostScript, PDF, DVI.

Last modified: 2003-06-08 by webmaster.