Hajime Ishihara's Guide to Constructive Reverse Mathematics 📚

The lecture was held within the framework of the Hausdorff Trimester Program: Types, Sets and Constructions.

Abstract:
This talk presents an introduction to constructive reverse mathematics (CRM) with some recent results. The aim of CRM is to classify various theorems in intuitionistic, constructive recursive and classical mathematics by logical principles, function existence axioms and their combinations. We review some results in classical reverse mathematics (Friedman-Simpson program), and axioms of intuitionistic and constructive recursive mathematics with their consequences to motivate CRM. Then we present some results of CRM with and without countable choice, and recent results in CRM without countable choice.