Propositional Subformula

propositional-logic

Definition

Propositional Subformula

A propositional subformula is a propositional formula contained in another propositional formula.

More precisely, a propositional formula $G$ is a subformula of a propositional formula $F$ if $G=F$ or if $G$ occurs as a proper part of $F$ when $F$ is analysed according to its formation rules.

A fixed occurrence of a propositional subformula can be specified formally by a propositional formula position.

Polarity

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$.

Link to original

Examples

$P\wedge Q$

In

$$P\wedge Q,$$

the subformulas are $P$, $Q$, and $P\wedge Q$.

$\neg (P\to Q)$

In

$$\neg (P\to Q),$$

the subformulas are $P$, $Q$, $P\to Q$, and $\neg (P\to Q)$.