27/01/2015 Danko Ilik ERRATA for version 2 of "An interpretation of the Sigma-2 fragment of classical Analysis in System", http://arxiv.org/abs/1301.5089v2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ There are two typos: - (p. 10) Computationally irrelevant formulas do not include disjunction. There is no disjunction as such in the system, only an existential quantifier. If there were disjunction, it would have to be a part of the \Sigma_2 formulas. - (p.14) \tau in MP should be replaced by \mathbb{N} ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 22/01/2014 Danko Ilik ERRATA for version 1 ("Double-negation shift as a constructive principle", http://arxiv.org/abs/1301.5089) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * DNS^0 does not imply \neg\neg LPO, as suggested in the Abstract and on page 4, but only every instance of it, which is not the same thing, since a universal quantification of type 0->0 is avoided. I thank Martin Escardo for pointing this out. (DNS^0 still implies \neg\neg HP and DNS^1 does imply \neg\neg LPO) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~