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.
|Number of pages||22|
|Journal||Journal of Symbolic Logic|
|Publication status||Published - 2018 Sept 1|
- fragments of classical logic
- intuitionistic arithmetic and analysis
- Phrasesdouble negation shift
ASJC Scopus subject areas