Every symbol in a formula has a polarity, which can be determined by a set of rules:
- The initial polarity is .
- A subformula which is a negation or the left hand side of an implication has the polarity of its parent multiplied by .
- Any subformula which is within (even indirectly) a bi-implication has a polarity of .
- All other operators do not affect polarity.
A subformula with a polarity of is said to occur positively. If its polarity is then it occurs negatively, and a polarity of indicates a neutral occurence.