We give a variant of the Gödel-Gentzen-negative translation, and a syntactic characterization which entails conservativity result for formulas.

We systematically study several principles and give a principle which is weaker than disjunctive Markov’s principle. We also show that the principle is underivable and strictly weaker than MP∨ in certain extensions of the system EL of elementary analysis.