- March 2016
Constructive reverse mathematics: an introduction and recent results
We review some results in Friedman-Simpson program, classical reverse mathematics, and axioms and their consequences in varieties of constructive mathematics: intuitionistic mathematics, constructive recursive mathematics and Bishop’s constructive mathematics. Then we propose constructive reverse mathematics with countable choice to classify theorems in the varieties of constructive mathematics by logical principles etc., and we refine it without assuming countable choice to compare some results in constructive reverse mathematics with results in classical reverse mathematics. Finally, we present some recent results on the binary expansion and the intermediate value theorem.