Polarity of Propositional Subformulas

logic

Definition

Polarity of Propositional Subformulas

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

We write $\mathrm{pol}(A,\pi )$ for the polarity of the occurrence at position $\pi$ in $A$:

$$\mathrm{pol}(A,\pi )=\{\begin{array}{ll}1& \text{if }\pi =\epsilon ,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\wedge \cdots \wedge B_n\text{ and }\pi ={\pi }^{\prime }.i,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\vee \cdots \vee B_n\text{ and }\pi ={\pi }^{\prime }.i,\\ -\mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=\neg B_1\text{ and }\pi ={\pi }^{\prime }.1,\\ -\mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\to B_2\text{ and }\pi ={\pi }^{\prime }.1,\\ \mathrm{pol}(A,{\pi }^{\prime })& \text{if }A{|}_{{\pi }^{\prime }}=B_1\to B_2\text{ and }\pi ={\pi }^{\prime }.2,\\ 0& \text{if }A{|}_{{\pi }^{\prime }}=B_1\leftrightarrow B_2\text{ and }\pi ={\pi }^{\prime }.i.\end{array}$$

An occurrence is called positive, negative, or neutral according as its polarity is $1$, $-1$, or $0$.

Behaviour

Let $A$ be a formula and let $B$ occur in $A$.

• The connectives $\wedge$ and $\vee$ preserve polarity.
• The connective $\neg$ flips polarity.
• In an implication $B_1\to B_2$, the first argument flips polarity and the second preserves it.
• In an equivalence $B_1\leftrightarrow B_2$, both arguments are neutral.

Neutral Subtrees

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

$$0=-0=+0$$

Odd Node

A position is negative ($\rho =-1$) if it has an odd number of negating (flipping) edges above it.

Even Node

A position is positive ($\rho =1$) if it has an even number of negating (flipping) edges above it.

Motivation

Monotonicity

Let the truth values be ordered by

$$0<1.$$

A connective is monotonic in an argument if increasing that argument’s truth value (from $0$ to $1$) 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 $1$ means the connective is monotonic in that argument;
• polarity $-1$ means the connective is anti-monotonic in that argument;
• polarity $0$ means the connective is neither monotonic nor anti-monotonic in that argument.

For the standard connectives this yields:

• monotonic: $\wedge$, $\vee$, and the second argument of $\to$;
• anti-monotonic: $\neg$ and the first argument of $\to$;
• neither: both arguments of $\leftrightarrow$.

Intuition

Forget the formal definition and start with a simpler question:

If we want the whole formula $A$ 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 $A$ to be true, then the root should help by being true. That is why the root gets polarity $1$.

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 $(1)$ means that moving this occurrence towards $1$ helps the whole formula;
• negative $(-1)$ means that moving this occurrence towards $0$ helps the whole formula;
• neutral $(0)$ means that there is no uniform helpful direction.

From here the connectives determine everything:

• for $B_1\wedge \cdots \wedge B_n$ and $B_1\vee \cdots \vee B_n$, the helpful direction is inherited by every child;
• for $\neg B$, the helpful direction is reversed;
• for $B_1\to B_2$, the left child reverses and the right child keeps the direction;
• for $B_1\leftrightarrow B_2$, the direction is lost, because both $(1,1)$ and $(0,0)$ 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 $B$ occur in $A$ at a position with polarity $\rho$.

• If $\rho =1$ (positive), then $A\models A[\top /B]$.
• If $\rho =-1$ (negative), then $A\models A[\perp /B]$.

In other words, a positively occurring subformula may be replaced by $\top$ and a negatively occurring subformula by $\perp$, 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 $1$; if only negatively, to $0$.

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 $1$ at the root
• pass through $\neg$ or the left side of $\to$ to flip polarity
• pass through $\wedge$, $\vee$, or the right side of $\to$ to keep polarity
• set polarity to $0$ below any occurrence of $\leftrightarrow$

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 $0$;
• otherwise, if the number of red edges on the path is odd, then the polarity is $-1$;
• otherwise, the polarity is $1$.

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

Colouring a tree

Let

$$A=\neg (((p\to q)\wedge ((p\wedge q)\to r))\to (p\leftrightarrow (r\to q))).$$

The outer negation contributes one red edge, the left child of the large implication contributes another red edge, and the whole subtree below $\leftrightarrow$ 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

$p\wedge (q\vee r)$

Let $A=p\wedge (q\vee r)$. We start with polarity $1$ at the root.

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

• $p$ has polarity $1$;
• $(q\vee r)$ has polarity $1$.

Inside $(q\vee r)$, the connective $\vee$ also preserves polarity. Therefore:

• $q$ has polarity $1$;
• $r$ has polarity $1$.

Thus every atom in $A$ occurs positively.

$\neg (p\to q)$

Let $A=\neg (p\to q)$. We start with polarity $1$ at the root.

First, the outer negation flips polarity, so the subformula $(p\to q)$ has polarity $-1$.

Next, we analyse the implication under polarity $-1$:

• the antecedent $p$ flips polarity once more, so $p$ has polarity $1$;
• the consequent $q$ preserves polarity, so $q$ has polarity $-1$.

Therefore, in $\neg (p\to q)$, the occurrence of $p$ is positive and the occurrence of $q$ is negative.

$((p\to q)\wedge \neg r)\to (s\leftrightarrow t)$

Let $A=((p\to q)\wedge \neg r)\to (s\leftrightarrow t)$.

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

The outermost implication starts with polarity $1$. Hence:

• the left side $((p\to q)\wedge \neg r)$ gets polarity $-1$;
• the right side $(s\leftrightarrow t)$ gets polarity $1$.

We first analyse the left side. The connective $\wedge$ preserves polarity, so both conjuncts still have polarity $-1$.

For the first conjunct $(p\to q)$ under polarity $-1$:

• the antecedent $p$ flips polarity, so $p$ has polarity $1$;
• the consequent $q$ preserves polarity, so $q$ has polarity $-1$.

For the second conjunct $\neg r$ under polarity $-1$, the negation flips polarity, so $r$ has polarity $1$.

We now analyse the right side $(s\leftrightarrow t)$. Since it is an equivalence, both arguments become neutral. Therefore:

• $s$ has polarity $0$;
• $t$ has polarity $0$.

Altogether, the atoms in $A$ have the following polarities:

$$p:1,q:-1,r:1,s:0,t:0.$$