Intuitionistic Choice and Restricted Classical Logic

Recently, Coquand and Palmgren considered systems of intuitionistic arithmeticin all finite types together with various forms of the axiom of choice anda numerical omniscience schema (NOS) which implies classical logic for arithmeticalformulas. Feferman subsequently observed that the proof theoreticstrength of such systems can be determined by functional interpretation basedon a non-constructive mu-operator and his well-known results on the strengthof this operator from the 70's.In this note we consider a weaker form LNOS (lesser numerical omniscienceschema) of NOS which suffices to derive the strong form of binary K¨onig'slemma studied by Coquand/Palmgren and gives rise to a new and mathematicallystrong semi-classical system which, nevertheless, can proof theoreticallybe reduced to primitive recursive arithmetic PRA. The proof of this fact relieson functional interpretation and a majorization technique developed in aprevious paper