Counterexamples in applicative theories with choice

Abstract

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.