Counterexamples in applicative theories with choice
Gerard R. Renardel de Lavalette · Logic Group preprint series · 1990
TAPP is a total applicative theory, conservative over intuitionistic arithmetic. In this paper, we compare a number of choice principles and establish their incompatibility with several other axiom schemes. The counterexamples involved are obtained in a uniform way and translate to similar results for related systems of intuitionistic arithmetic and analysis.