MARKOV’S PRINCIPLE AND SUBSYSTEMS OF INTUITIONISTIC ANALYSIS
Joan Rand Moschovakis · Journal of Symbolic Logic · 2019
Abstract Using a technique developed by Coquand and Hofmann [3] we verify that adding the analytical form MP 1 : $\forall \alpha ( eg eg \exists {\rm{x}}\alpha ({\rm{x}}) = 0 \to \exists {\rm{x}}\alpha ({\rm{x}}) = 0)$ of Markov’s Principle does not increase the class of ${\rm{\Pi }}_2^0$ formulas provable in Kleene and Vesley’s formal system for intuitionistic analysis, or in subsystems obtained by omitting or restricting various axiom schemas in specified ways.