Mathematical Descriptions that are Mathematical Objects

We can measure how strong a mathematical theory is by asking whether it can distinguish computer programs which run for a very long time from those which never halt. Measuring stronger theories requires new techniques for describing computer programs which are guaranteed to eventually stop, but where this can only be proven in very strong theories. The goal of this project is to complete a recent breakthrough in this area which introduced the use of self-modifying computer programs. This made it possible to analyze the theory known as full second order arithmetic in this way. This project will use this new characterization of this very abstract theory to develop new ways to translate this abstract strength into concrete, computational information. This project involves graduate and undergraduate students. The starting point of this project will be writing down a complete ordinal notation for the theory of second order arithmetic and then using this to examine the strength of this theory from several perspectives. The project will develop combinatorial results, in the style of Goodstein sequences or hydra games, whose termination is so hard to prove that it cannot be shown in second order arithmetic. The project will also develop new forms of inductive definitions which exhaust the strength of second order arithmetic. This project will also develop this new approach to cut-elimination as a general method applicable to other logics besides variants of second order arithmetic. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.