Searching for the ideal framework
Michael Rathjen1
1 University of Leeds
The best known program for calibrating the strength of theorems from ordinary mathematics is reverse mathematics (RM). RM’s scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. However, its language is not expressive enough to be able to talk about higher order objects, such as function spaces, directly.
Richer formal systems in which higher order mathematical objects can be directly accounted for have been suggested. The price for maintaining conservativity over elementary theories, however, is that one has to use different logics for different ontological realms, allowing classical logic to reign at the level of numbers but higher type mathematical objects only governed by intuitionistic logic. In the talk, I’d like to present some of these semi-intuitionistic systems, give a feel for carrying out mathematics within them, and relate them to systems considered in RM.