We investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector's consistency proof of ACA0 and from the negative translation of RCA0, as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.
- fragments of classical logic
- intuitionistic arithmetic and analysis
- Phrasesdouble negation shift
ASJC Scopus subject areas