Now Under Construction: Intuitionistic Reverse Analysis

Each variety of reverse analysis attempts to determine a minimal axiomatic basis for proving a particular mathematical theorem. Classical reverse analysis asks which set existence axioms are needed to prove particular theorems of classical second-order number theory. Informal constructive reverse analysis asks which constructive principles are needed to prove particular theorems of Bishop’s constructive analysis, and which nonconstructive principles are equivalent over Bishop’s constructive analysis to classical theorems. Intuitionistic reverse analysis asks which intuitionistically accepted properties of numbers and functions suffice to prove particular theorems of intuitionistic analysis using intuitionistic logic, and may also consider the relative strength of classical principles consistent with intuitionistic analysis. This lecture sketches the current state of intuitionistic reverse analysis, in relation to its classical counterpart