History

Please fill in your query. A complete syntax description you will find on the General Help page.
Intuitionistic choice and restricted classical logic. (English)
Math. Log. Q. 47, No.4, 455-460 (2001).
Summary: Recently, {\it T. Coquand} and {\it E. Palmgren} [Arch. Math. Logic 39, 53-74 (2000; Zbl 0947.03078)] 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. S. Feferman subsequently observed that the proof-theoretic strength of such systems can be determined by functional interpretation based on a nonconstructive $μ$-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 [the author, J. Symb. Log. 57, 1239-1273 (1992; Zbl 0781.03051)].