Proper Subformula (Propositional Logic)

Definition

Proper Subformula (Propositional Logic)

A subformula $G$ of a formula $F$ is a proper subformula of $F$ if it is not $F$ itself:

$$G\in \mathrm{Sub}(F)\setminus \{F\}.$$

Property

Strict partial order

“Is a proper subformula of” is the strict companion of the subformula partial order: irreflexive, since no formula is a proper subformula of itself, and transitive, since subformulas of a subformula are again subformulas. Every step to a proper subformula removes at least the topmost connective, so chains of proper subformulas are finite.