Polarity (Propositional Logic)

logic

Definition

Polarity (Propositional Logic)

Let be a propositional formula. The polarity of an occurrence of a subformula in is defined recursively from the root of .

We write for the polarity of the occurrence at position in :

An occurrence is called positive, negative, or neutral according as its polarity is , , or .

Behaviour

Let be a formula and let occur in .

• The connectives and preserve polarity.
• The connective flips polarity.
• In an implication , the first argument flips polarity and the second preserves it.
• In an equivalence , both arguments are neutral.

Neutral Subtrees

Once a position is neutral, every subformula in its subtree is also neutral, since:

Odd Node

A position is negative () if it has an odd number of negating (flipping) edges above it.

Even Node

A position is positive () if it has an even number of negating (flipping) edges above it.

Motivation

Monotonicity

Let the truth values be ordered by

A connective is monotonic in an argument if increasing that argument’s truth value (from to ) never decreases the truth value of the whole formula. It is anti-monotonic in an argument if increasing that argument’s truth value never increases the truth value of the whole formula.

The three polarity values correspond exactly to these three possibilities:

• polarity means the connective is monotonic in that argument;
• polarity means the connective is anti-monotonic in that argument;
• polarity means the connective is neither monotonic nor anti-monotonic in that argument.

For the standard connectives this yields:

• monotonic: , , and the second argument of ;
• anti-monotonic: and the first argument of ;
• neither: both arguments of .

Intuition

Forget the formal definition and start with a simpler question:

If we want the whole formula to be true, in which direction should a given occurrence help?

At the root there is no choice. The root is the whole formula itself, so if we want to be true, then the root should help by being true. That is why the root gets polarity .

Now move down the parse tree. For each child, ask the same question again: does making this child truer help the original goal, does making it falser help, or is there no uniform helpful direction?

This leads to three cases:

• positive means that moving this occurrence towards helps the whole formula;
• negative means that moving this occurrence towards helps the whole formula;
• neutral means that there is no uniform helpful direction.

From here the connectives determine everything:

• for and , the helpful direction is inherited by every child;
• for , the helpful direction is reversed;
• for , the left child reverses and the right child keeps the direction;
• for , the direction is lost, because both and make the equivalence true.

So polarity is not a guessed sign. It is the record of how the single goal

make the whole formula true

propagates through the tree.

Simplification

Polarity tells us which truth value can be substituted safely for an occurrence of a subformula without destroying satisfiability.

Let occur in at a position with polarity .

• If (positive), then .
• If (negative), then .

In other words, a positively occurring subformula may be replaced by and a negatively occurring subformula by , and the resulting formula is a logical consequence of the original.

This justifies the pure literal rule used in the DPLL algorithm: if an atom occurs only positively, it may be set to ; if only negatively, to .

Computation

Tree Traversal

Polarity is computed from the structure of the formula, usually by traversing its parse tree.

A practical rule is:

• start with polarity at the root
• pass through or the left side of to flip polarity
• pass through , , or the right side of to keep polarity
• set polarity to below any occurrence of

Colouring Algorithm

Edge colouring

The recursive definition can be read off from the parse tree by colouring its edges.

1. Colour in blue every edge below an equivalence.
2. Colour in red every uncoloured edge leaving a negation and every uncoloured edge going to the left child of an implication.
3. Leave all remaining edges uncoloured.

Then the polarity of a position is determined by the path from the root to that position:

• if there is at least one blue edge on the path, then the polarity is ;
• otherwise, if the number of red edges on the path is odd, then the polarity is ;
• otherwise, the polarity is .

This works because blue is absorbing below an equivalence, while each red edge contributes exactly one sign flip.

Colouring a tree

Let

The outer negation contributes one red edge, the left child of the large implication contributes another red edge, and the whole subtree below is blue. Hence the two rightmost leaves are immediately neutral, while the left branch is determined by the parity of the red edges above it.

Examples

Let . We start with polarity at the root.

The outer connective is , so both arguments preserve polarity. Hence:

• has polarity ;
• has polarity .

Inside , the connective also preserves polarity. Therefore:

• has polarity ;
• has polarity .

Thus every atom in occurs positively.

Let . We start with polarity at the root.

First, the outer negation flips polarity, so the subformula has polarity .

Next, we analyse the implication under polarity :

• the antecedent flips polarity once more, so has polarity ;
• the consequent preserves polarity, so has polarity .

Therefore, in , the occurrence of is positive and the occurrence of is negative.

Let .

We compute the polarity of the occurring subformulas step by step.

The outermost implication starts with polarity . Hence:

• the left side gets polarity ;
• the right side gets polarity .

We first analyse the left side. The connective preserves polarity, so both conjuncts still have polarity .

For the first conjunct under polarity :

• the antecedent flips polarity, so has polarity ;
• the consequent preserves polarity, so has polarity .

For the second conjunct under polarity , the negation flips polarity, so has polarity .

We now analyse the right side . Since it is an equivalence, both arguments become neutral. Therefore:

• has polarity ;
• has polarity .

Altogether, the atoms in have the following polarities: