文章基本信息

标题：Intuitionistic Choice and Restricted Classical Logic
本地全文：下载
作者：Ulrich Kohlenbach
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2000
卷号：7
期号：12
出版社：Aarhus University
摘要：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¨onig'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.