Subformula (Propositional Logic)

Definition

Subformula (Propositional Logic)

The subformulas of a formula $F$ are the formulas out of which $F$ is built, $F$ included; the set $\mathrm{Sub}(F)$ of them is defined recursively over the structure of $F$:

$$\mathrm{Sub}(F)=\{\begin{array}{ll}\{F\}& F\text{ an atom},\\ \{F\}\cup \mathrm{Sub}(G)& F=\neg G,\\ \{F\}\cup {\bigcup }_{i=1}^n\mathrm{Sub}(B_i)& F=B_1\wedge \cdots \wedge B_n\text{ or }{B}_1\vee \cdots \vee B_n,\\ \{F\}\cup \mathrm{Sub}(G)\cup \mathrm{Sub}(H)& F=G\circ H,\circ \in \{\to ,\leftrightarrow \}.\end{array}$$

Each case adds $F$ to the subformulas of its immediate parts; an atom — likewise the constants $\top$, $\perp$ (verum, falsum) — has only itself. Being a subformula is a partial order, whose strict companion is the proper subformula relation. An occurrence of a subformula in $F$ is fixed by a propositional formula position; distinct positions may carry the same formula.

Polarity

Definition

Polarity (Propositional Logic)

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