Intuitionistic Choice and Restricted Classical Logic

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic<br />in all finite types together with various forms of the axiom of choice and<br />a numerical omniscience schema (NOS) which implies classical logic for arithmetical<br />formulas. Feferman subsequently observed that the proof theoretic<br />strength of such systems can be determined by functional interpretation based<br />on a non-constructive mu-operator and his well-known results on the strength<br />of this operator from the 70's.<br />In this note we consider a weaker form LNOS (lesser numerical omniscience<br />schema) of NOS which suffices to derive the strong form of binary K¨onig's<br />lemma studied by Coquand/Palmgren and gives rise to a new and mathematically<br />strong semi-classical system which, nevertheless, can proof theoretically<br />be reduced to primitive recursive arithmetic PRA. The proof of this fact relies<br />on functional interpretation and a majorization technique developed in a<br />previous paper.