Intuitionistic Propositional Logic

Question

I have been looking into intuitionistic logic and what is called "negative fragment" of intuitionistic propositional logic. However, I was not able to find any resource that explains the reason why it is called "negative fragment".

Any references/suggestions?

Answer 1

According to Negative translations not intuitionistically equivalent to the usual ones,

The image of the usual negative translations is (essentially) the negative fragment NF, that is the set of all formulas without ∨ and ∃ and whose atomic formulas are all negated

If you look at the rules given at page 3 (or here), it should be unsurprising that the translation is called negative. The fragment as defined by Harper removes the requirement that

atomic formulas are all negated