INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES

Abstract

Abstract We investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector’s consistency proof of ACA 0 and from the negative translation of RCA 0 , as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.