CODEWITHSUNDEEP
logicdependent-typetype-theory
geguze
geguze

Reputation: 203

Intuitionistic Propositional Logic

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?

Upvotes: 1

Views: 116

Answers (1)

Alexey Romanov
Alexey Romanov

Reputation: 170735

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

Upvotes: 1

Related Questions