Hajime Ishihara- Constructive Reverse Mathematics- An Introduction and Recent Results

Explore constructive reverse mathematics (CRM) in this comprehensive lecture by Hajime Ishihara. Delve into the classification of theorems in intuitionistic, constructive recursive, and classical mathematics using logical principles and function existence axioms. Begin with an overview of classical reverse mathematics, including the Friedman-Simpson program, before examining axioms of intuitionistic and constructive recursive mathematics. Investigate CRM results with and without countable choice, and discover recent developments in the field. Learn about key concepts such as omniscience principles, Markov's principle, and the relationship among various mathematical principles. Gain insights into the multi-dimensional nature of CRM and its implications for mathematical foundations.

Intro
Classical reverse mathematics
Classical (higher order) reverse mathematics
Bishop's constructive mathematics
Notations
Axioms of intuitionism
Consequences of the axioms
Omniscience principles
Principles weaker than Markov's principle
Relationship among principles
Constructive reverse mathematics with countable choice
Constructive reverse mathematics (CRM)
WKL for restricted trees
Conditions for DC
CRM is a multi-dimensional reverse mathematics