Intuitionistic Choice and Restricted Classical Logic

Ulrich Kohlenbach

May 2000


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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.